:: MATRIX10 semantic presentation begin definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); attr "M" is :::"Positive"::: means :: MATRIX10:def 1 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))); attr "M" is :::"Negative"::: means :: MATRIX10:def 2 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))); attr "M" is :::"Nonpositive"::: means :: MATRIX10:def 3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))); attr "M" is :::"Nonnegative"::: means :: MATRIX10:def 4 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))); end; :: deftheorem defines :::"Positive"::: MATRIX10:def 1 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix10 :::"Positive"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); :: deftheorem defines :::"Negative"::: MATRIX10:def 2 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v2_matrix10 :::"Negative"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); :: deftheorem defines :::"Nonpositive"::: MATRIX10:def 3 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); :: deftheorem defines :::"Nonnegative"::: MATRIX10:def 4 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); definitionlet "M1", "M2" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); pred "M1" :::"is_less_than"::: "M2" means :: MATRIX10:def 5 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M1"))) "holds" (Bool (Set "M1" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set "M2" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))); pred "M1" :::"is_less_or_equal_with"::: "M2" means :: MATRIX10:def 6 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M1"))) "holds" (Bool (Set "M1" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set "M2" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))); end; :: deftheorem defines :::"is_less_than"::: MATRIX10:def 5 : (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M1"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "M2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) ")" )); :: deftheorem defines :::"is_less_or_equal_with"::: MATRIX10:def 6 : (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M1"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "M2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) ")" )); definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"|:":::"M":::":|"::: -> ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: MATRIX10:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"|:"::: MATRIX10:def 7 : (Bool "for" (Set (Var "M")) "," (Set (Var "b2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M")) ($#k1_matrix10 :::":|"::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ) ")" )); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"-"::: redefine func :::"-"::: "M" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "M1", "M2" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"+"::: redefine func "M1" :::"+"::: "M2" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "M1", "M2" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"-"::: redefine func "M1" :::"-"::: "M2" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"*"::: redefine func "a" :::"*"::: "M" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registration cluster (Set "(" (Num 1) "," (Num 1) ")" ($#k1_matrix_2 :::"-->"::: ) (Num 1)) -> ($#v1_matrix10 :::"Positive"::: ) for ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "(" (Num 1) "," (Num 1) ")" ($#k1_matrix_2 :::"-->"::: ) (Num 1)) -> ($#v4_matrix10 :::"Nonnegative"::: ) for ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "(" (Num 1) "," (Num 1) ")" ($#k1_matrix_2 :::"-->"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) -> ($#v2_matrix10 :::"Negative"::: ) for ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "(" (Num 1) "," (Num 1) ")" ($#k1_matrix_2 :::"-->"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) -> ($#v3_matrix10 :::"Nonpositive"::: ) for ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; registration cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set bbbadK3_FINSEQ_2((Set ($#k1_numbers :::"REAL"::: ) )))) bbbadV1_FUNCT_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_matrix_1 :::"tabular"::: ) ($#v1_matrix10 :::"Positive"::: ) ($#v4_matrix10 :::"Nonnegative"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set bbbadK3_FINSEQ_2((Set ($#k1_numbers :::"REAL"::: ) ))); cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set bbbadK3_FINSEQ_2((Set ($#k1_numbers :::"REAL"::: ) )))) bbbadV1_FUNCT_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_matrix_1 :::"tabular"::: ) ($#v2_matrix10 :::"Negative"::: ) ($#v3_matrix10 :::"Nonpositive"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set bbbadK3_FINSEQ_2((Set ($#k1_numbers :::"REAL"::: ) ))); end; registrationlet "M" be ($#v1_matrix10 :::"Positive"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "M" ($#k4_matrix_1 :::"@"::: ) ) -> ($#v1_matrix10 :::"Positive"::: ) ; end; registrationlet "M" be ($#v2_matrix10 :::"Negative"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "M" ($#k4_matrix_1 :::"@"::: ) ) -> ($#v2_matrix10 :::"Negative"::: ) ; end; registrationlet "M" be ($#v3_matrix10 :::"Nonpositive"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "M" ($#k4_matrix_1 :::"@"::: ) ) -> ($#v3_matrix10 :::"Nonpositive"::: ) ; end; registrationlet "M" be ($#v4_matrix10 :::"Nonnegative"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "M" ($#k4_matrix_1 :::"@"::: ) ) -> ($#v4_matrix10 :::"Nonnegative"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set "(" "n" "," "n" ")" ($#k1_matrix_2 :::"-->"::: ) (Num 1)) -> ($#v1_matrix10 :::"Positive"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "(" "n" "," "n" ")" ($#k1_matrix_2 :::"-->"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) -> ($#v2_matrix10 :::"Negative"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "(" "n" "," "n" ")" ($#k1_matrix_2 :::"-->"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) -> ($#v3_matrix10 :::"Nonpositive"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "(" "n" "," "n" ")" ($#k1_matrix_2 :::"-->"::: ) (Num 1)) -> ($#v4_matrix10 :::"Nonnegative"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set bbbadK3_FINSEQ_2((Set ($#k1_numbers :::"REAL"::: ) )))) bbbadV1_FUNCT_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_matrix_1 :::"tabular"::: ) ($#v1_matrix10 :::"Positive"::: ) ($#v4_matrix10 :::"Nonnegative"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set bbbadK3_FINSEQ_2((Set ($#k1_numbers :::"REAL"::: ) )))) bbbadV1_FUNCT_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_matrix_1 :::"tabular"::: ) ($#v2_matrix10 :::"Negative"::: ) ($#v3_matrix10 :::"Nonpositive"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: MATRIX10:1 (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_vectsp_1 :::"F_Real"::: ) ) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set (Var "x2")))))) ; theorem :: MATRIX10:2 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set "(" ($#k4_matrixr1 :::"-"::: ) (Set (Var "M")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: MATRIX10:3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M2")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M1"))))) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k5_matrixr1 :::"-"::: ) (Set (Var "M2")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "M2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: MATRIX10:4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_matrixr1 :::"*"::: ) (Set (Var "M")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" )))))) ; theorem :: MATRIX10:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M")) ($#k1_matrix10 :::":|"::: ) ))))) ; theorem :: MATRIX10:6 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_matrix10 :::"|:"::: ) (Set "(" (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M")) ")" ) ($#k1_matrix10 :::":|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k7_matrixr1 :::"*"::: ) (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M")) ($#k1_matrix10 :::":|"::: ) )))))) ; theorem :: MATRIX10:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M"))) "is" ($#v1_matrix10 :::"Positive"::: ) ))) ; theorem :: MATRIX10:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v1_matrix10 :::"Positive"::: ) ))) ; theorem :: MATRIX10:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M2")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M1")))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v1_matrix10 :::"Positive"::: ) ))) ; theorem :: MATRIX10:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v1_matrix10 :::"Positive"::: ) ))) ; theorem :: MATRIX10:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix10 :::"Negative"::: ) ) & (Bool (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M2")) ($#k1_matrix10 :::":|"::: ) ) ($#r1_matrix10 :::"is_less_than"::: ) (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M1")) ($#k1_matrix10 :::":|"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v1_matrix10 :::"Positive"::: ) ))) ; theorem :: MATRIX10:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) "is" ($#v1_matrix10 :::"Positive"::: ) ))) ; theorem :: MATRIX10:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M2")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M1")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) "is" ($#v1_matrix10 :::"Positive"::: ) ))) ; theorem :: MATRIX10:14 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v1_matrix10 :::"Positive"::: ) )))) ; theorem :: MATRIX10:15 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v1_matrix10 :::"Positive"::: ) )))) ; theorem :: MATRIX10:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M"))) "is" ($#v2_matrix10 :::"Negative"::: ) ))) ; theorem :: MATRIX10:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix10 :::"Negative"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v2_matrix10 :::"Negative"::: ) ))) ; theorem :: MATRIX10:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M2"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v2_matrix10 :::"Negative"::: ) ))) ; theorem :: MATRIX10:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix10 :::"Negative"::: ) ) & (Bool (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M1")) ($#k1_matrix10 :::":|"::: ) ) ($#r1_matrix10 :::"is_less_than"::: ) (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M2")) ($#k1_matrix10 :::":|"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v2_matrix10 :::"Negative"::: ) ))) ; theorem :: MATRIX10:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) "is" ($#v2_matrix10 :::"Negative"::: ) ))) ; theorem :: MATRIX10:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1"))) "is" ($#v2_matrix10 :::"Negative"::: ) ))) ; theorem :: MATRIX10:22 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v2_matrix10 :::"Negative"::: ) )))) ; theorem :: MATRIX10:23 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v2_matrix10 :::"Negative"::: ) )))) ; theorem :: MATRIX10:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )) "holds" (Bool (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M"))) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ))) ; theorem :: MATRIX10:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ))) ; theorem :: MATRIX10:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ))) ; theorem :: MATRIX10:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M2"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ))) ; theorem :: MATRIX10:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ))) ; theorem :: MATRIX10:29 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )))) ; theorem :: MATRIX10:30 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )))) ; theorem :: MATRIX10:31 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )))) ; theorem :: MATRIX10:32 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )))) ; theorem :: MATRIX10:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M")) ($#k1_matrix10 :::":|"::: ) ) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ))) ; theorem :: MATRIX10:34 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ))) ; theorem :: MATRIX10:35 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )) "holds" (Bool (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M"))) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ))) ; theorem :: MATRIX10:36 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ))) ; theorem :: MATRIX10:37 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M1"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ))) ; theorem :: MATRIX10:38 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M2")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M1")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ))) ; theorem :: MATRIX10:39 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )))) ; theorem :: MATRIX10:40 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )))) ; theorem :: MATRIX10:41 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )))) ; theorem :: MATRIX10:42 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M"))) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )))) ; theorem :: MATRIX10:43 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k3_matrix10 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2")) ")" )) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )))) ; begin theorem :: MATRIX10:44 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:45 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M3"))))) ; theorem :: MATRIX10:46 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M3")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M4")))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M3"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M2")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M4")))))) ; theorem :: MATRIX10:47 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M3"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M2")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M3")))))) ; theorem :: MATRIX10:48 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:49 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_matrix10 :::"|:"::: ) (Set "(" (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k1_matrix10 :::":|"::: ) ) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M1")) ($#k1_matrix10 :::":|"::: ) ) ($#k3_matrixr1 :::"+"::: ) (Set ($#k1_matrix10 :::"|:"::: ) (Set (Var "M2")) ($#k1_matrix10 :::":|"::: ) ))))) ; theorem :: MATRIX10:50 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3")))))) ; theorem :: MATRIX10:51 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M3")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3"))))) "holds" (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:52 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3"))))) "holds" (Bool (Set (Var "M3")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:53 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:54 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M3")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M4")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M4"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3")))))) ; theorem :: MATRIX10:55 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M3")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M4")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M4"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3")))))) ; theorem :: MATRIX10:56 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M4"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M4")))))) ; theorem :: MATRIX10:57 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M4"))))) "holds" (Bool (Set (Set (Var "M4")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:58 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M4"))))) "holds" (Bool (Set (Set (Var "M4")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:59 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX10:60 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M4"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M3"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M4")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX10:61 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M4"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M4"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX10:62 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M4"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M4"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX10:63 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:64 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M2"))))) "holds" (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:65 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M2")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M1")))) "holds" (Bool (Set ($#k2_matrix10 :::"-"::: ) (Set (Var "M1"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:66 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M2")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:67 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:68 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )) "holds" (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX10:69 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:70 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M3")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ) & (Bool (Set (Var "M3")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M3")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M1"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:71 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M3")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ) & (Bool (Set (Var "M3")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M3")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M1"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:72 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M3")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix10 :::"Negative"::: ) ) & (Bool (Set (Var "M3")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M3")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M1"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:73 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ) & (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M3")))))) ; theorem :: MATRIX10:74 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) ) & (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M3")))))) ; theorem :: MATRIX10:75 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ) & (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M1")) ($#k3_matrix10 :::"+"::: ) (Set (Var "M3")))))) ; theorem :: MATRIX10:76 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) )) "holds" (Bool (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:77 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) )) "holds" (Bool (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))))) ; theorem :: MATRIX10:78 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) )) "holds" (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:79 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix10 :::"Negative"::: ) )) "holds" (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:80 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1"))) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ))) ; theorem :: MATRIX10:81 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ) & (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Set (Var "M2")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M3"))))) ; theorem :: MATRIX10:82 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ) & (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:83 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ) & (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:84 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix10 :::"Negative"::: ) ) & (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "M3")) ($#k4_matrix10 :::"-"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX10:85 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX10:86 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX10:87 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))))))) ; theorem :: MATRIX10:88 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))))))) ; theorem :: MATRIX10:89 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX10:90 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))))))) ; theorem :: MATRIX10:91 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ) & (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "b")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX10:92 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "M1")) "is" ($#v3_matrix10 :::"Nonpositive"::: ) ) & (Bool (Set (Var "M2")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M1")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Set (Var "b")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX10:93 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "M1")) "is" ($#v2_matrix10 :::"Negative"::: ) ) & (Bool (Set (Var "M2")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M1")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "b")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX10:94 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "M1")) "is" ($#v4_matrix10 :::"Nonnegative"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "b")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX10:95 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) ) & (Bool (Set (Var "M1")) ($#r2_matrix10 :::"is_less_or_equal_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "b")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX10:96 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "M1")) "is" ($#v1_matrix10 :::"Positive"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M1"))) ($#r1_matrix10 :::"is_less_than"::: ) (Set (Set (Var "b")) ($#k5_matrix10 :::"*"::: ) (Set (Var "M2"))))))) ;