:: POLYNOM8 semantic presentation begin theorem :: POLYNOM8:1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "x")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: POLYNOM8:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k8_group_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k11_algstr_0 :::"""::: ) ")" ))))) ; theorem :: POLYNOM8:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z")))))) ; theorem :: POLYNOM8:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k5_binom :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" )))))) ; theorem :: POLYNOM8:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k2_binom :::"|^"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "q")) ($#k2_binom :::"|^"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s")) ")" ) ")" ) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" )))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"emb"::: "(" "m" "," "L" ")" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: POLYNOM8:def 1 (Set "m" ($#k5_binom :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) "L" ")" )); end; :: deftheorem defines :::"emb"::: POLYNOM8:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_polynom8 :::"emb"::: ) "(" (Set (Var "m")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k5_binom :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ))))); theorem :: POLYNOM8:6 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_polynom8 :::"emb"::: ) "(" (Set (Var "m")) "," (Set (Var "L")) ")" ")" ) ($#k6_matrix_3 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_polynom8 :::"emb"::: ) "(" (Set (Var "m")) "," (Set (Var "L")) ")" ")" ) ($#k6_matrix_3 :::"*"::: ) (Set "(" (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2")) ")" ))))))) ; theorem :: POLYNOM8:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: POLYNOM8:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "s")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM8:9 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ))))) ; theorem :: POLYNOM8:10 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "k")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "l")) ($#k3_polynom5 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "l")) ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "seq"))))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "m1", "m2" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "L")); func "m1" :::"*"::: "m2" -> ($#m1_subset_1 :::"sequence":::) "of" "L" means :: POLYNOM8:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "m1" ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "m2" ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"*"::: POLYNOM8:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "m1")) ($#k2_polynom8 :::"*"::: ) (Set (Var "m2")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m1")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "m2")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "m1", "m2" be ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Const "L")); cluster (Set "m1" ($#k2_polynom8 :::"*"::: ) "m2") -> ($#v1_algseq_1 :::"finite-Support"::: ) ; end; theorem :: POLYNOM8:11 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "m1")) ($#k2_polynom8 :::"*"::: ) (Set (Var "m2")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "m1")) ")" ) "," (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "m2")) ")" ) ")" )))) ; theorem :: POLYNOM8:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "m2"))))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "m1")) ($#k2_polynom8 :::"*"::: ) (Set (Var "m2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "m1")))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "i" be ($#m1_hidden :::"Integer":::); func :::"pow"::: "(" "a" "," "i" ")" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: POLYNOM8:def 3 (Set (Set "(" ($#k4_group_1 :::"power"::: ) "L" ")" ) ($#k1_binop_1 :::"."::: ) "(" "a" "," "i" ")" ) if (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) "i") otherwise (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) "L" ")" ) ($#k2_binop_1 :::"."::: ) "(" "a" "," (Set "(" ($#k1_int_2 :::"abs"::: ) "i" ")" ) ")" ")" ) ($#k11_algstr_0 :::"""::: ) ); end; :: deftheorem defines :::"pow"::: POLYNOM8:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "implies" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "i")) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))))) "implies" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "i")) ")" ) ")" ")" ) ($#k11_algstr_0 :::"""::: ) )) ")" ")" )))); theorem :: POLYNOM8:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM8:14 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: POLYNOM8:15 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) )))) ; theorem :: POLYNOM8:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM8:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "x")))) & (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ")" ))) ")" )))) ; theorem :: POLYNOM8:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ")" ))))) ; theorem :: POLYNOM8:19 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "j")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Num 1) ")" ")" )))))) ; theorem :: POLYNOM8:20 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "j")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" )))))) ; theorem :: POLYNOM8:21 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ")" ))))) ; theorem :: POLYNOM8:22 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "k")) ")" ) ")" ))))) ; theorem :: POLYNOM8:23 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ))))) ; theorem :: POLYNOM8:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "m")) ")" ))))) ; theorem :: POLYNOM8:25 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k11_algstr_0 :::"""::: ) ))))) ; theorem :: POLYNOM8:26 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set "(" ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "j")) ")" ))))) ; theorem :: POLYNOM8:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set "(" (Set (Var "x")) ($#k2_binom :::"|^"::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ))))) ; begin definitionlet "m" be ($#m1_hidden :::"Nat":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Const "L")); func :::"mConv"::: "(" "p" "," "m" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "m" "," (Num 1) "," "L" means :: POLYNOM8:def 4 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "m")) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"mConv"::: POLYNOM8:def 4 : (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Num 1) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_polynom8 :::"mConv"::: ) "(" (Set (Var "p")) "," (Set (Var "m")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )))) ")" ))))); theorem :: POLYNOM8:28 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_polynom8 :::"mConv"::: ) "(" (Set (Var "p")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k4_polynom8 :::"mConv"::: ) "(" (Set (Var "p")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" ($#k4_polynom8 :::"mConv"::: ) "(" (Set (Var "p")) "," (Set (Var "m")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )))) ; theorem :: POLYNOM8:29 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Num 1) "," (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set ($#k4_polynom8 :::"mConv"::: ) "(" (Set (Var "a")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "M"))))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "L")); func :::"aConv"::: "M" -> ($#m1_subset_1 :::"AlgSequence":::) "of" "L" means :: POLYNOM8:def 5 (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M"))) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M"))) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "L")) ")" ) ")" ); end; :: deftheorem defines :::"aConv"::: POLYNOM8:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_polynom8 :::"aConv"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" ) ")" )))); begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "x" :::"is_primitive_root_of_degree"::: "n" means :: POLYNOM8:def 6 (Bool "(" (Bool "n" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "x" ($#k2_binom :::"|^"::: ) "n") ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "L")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) "n")) "holds" (Bool (Set "x" ($#k2_binom :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k5_struct_0 :::"1."::: ) "L")) ")" ) ")" ); end; :: deftheorem defines :::"is_primitive_root_of_degree"::: POLYNOM8:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Var "n"))) "iff" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "x")) ($#k2_binom :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))) ")" ) ")" ) ")" )))); theorem :: POLYNOM8:30 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Bool "not" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Var "n")))))) ; theorem :: POLYNOM8:31 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Var "m")))))) ; theorem :: POLYNOM8:32 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))))))) ; definitionlet "m" be ($#m1_hidden :::"Nat":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"DFT"::: "(" "p" "," "x" "," "m" ")" -> ($#m1_subset_1 :::"AlgSequence":::) "of" "L" means :: POLYNOM8:def 7 (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) "m")) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" "p" "," (Set "(" "x" ($#k2_binom :::"|^"::: ) (Set (Var "i")) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) "m")) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "L")) ")" ) ")" ); end; :: deftheorem defines :::"DFT"::: POLYNOM8:def 7 : (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_polynom8 :::"DFT"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "m")) ")" )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "x")) ($#k2_binom :::"|^"::: ) (Set (Var "i")) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" ) ")" )))))); theorem :: POLYNOM8:33 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_polynom8 :::"DFT"::: ) "(" (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) "," (Set (Var "x")) "," (Set (Var "m")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))))) ; theorem :: POLYNOM8:34 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k6_polynom8 :::"DFT"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "m")) ")" ")" ) ($#k2_polynom8 :::"*"::: ) (Set "(" ($#k6_polynom8 :::"DFT"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) "," (Set (Var "m")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_polynom8 :::"DFT"::: ) "(" (Set "(" (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) "," (Set (Var "m")) ")" )))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "m" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"Vandermonde"::: "(" "x" "," "m" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "m" "," "L" means :: POLYNOM8:def 8 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "m") & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) "m")) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" "x" "," (Set "(" (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ))); end; :: deftheorem defines :::"Vandermonde"::: POLYNOM8:def 8 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_polynom8 :::"Vandermonde"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" )) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ))) ")" ))))); notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "m" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); synonym :::"VM"::: "(" "x" "," "m" ")" for :::"Vandermonde"::: "(" "x" "," "m" ")" ; end; theorem :: POLYNOM8:35 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "L")) "," (Set (Var "m")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Var "M")))))) ; theorem :: POLYNOM8:36 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_polynom8 :::"emb"::: ) "(" (Set (Var "m")) "," (Set (Var "L")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "u1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))) ")" )) "holds" (Bool (Set (Set (Var "u")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_polynom8 :::"emb"::: ) "(" (Set (Var "m")) "," (Set (Var "L")) ")" ")" ) ($#k6_matrix_3 :::"*"::: ) (Set (Var "u1"))))))) ; theorem :: POLYNOM8:37 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Var "m"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom8 :::"pow"::: ) "(" (Set (Var "x")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "s")))))))) ; theorem :: POLYNOM8:38 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "m")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "x")) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))))) ; theorem :: POLYNOM8:39 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_polynom8 :::"emb"::: ) "(" (Set (Var "m")) "," (Set (Var "L")) ")" ")" ) ($#k6_matrix_3 :::"*"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "L")) "," (Set (Var "m")) ")" ")" )))))) ; theorem :: POLYNOM8:40 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x")) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) "," (Set (Var "m")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" ")" )))))) ; begin theorem :: POLYNOM8:41 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" ($#k6_polynom8 :::"DFT"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "m")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k4_polynom8 :::"mConv"::: ) "(" (Set (Var "p")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ))))))) ; theorem :: POLYNOM8:42 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_polynom8 :::"DFT"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "m")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k5_polynom8 :::"aConv"::: ) (Set "(" (Set "(" ($#k7_polynom8 :::"VM"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k4_polynom8 :::"mConv"::: ) "(" (Set (Var "p")) "," (Set (Var "m")) ")" ")" ) ")" ))))))) ; theorem :: POLYNOM8:43 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k6_polynom8 :::"DFT"::: ) "(" (Set "(" ($#k6_polynom8 :::"DFT"::: ) "(" (Set "(" (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) "," (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ")" ")" ) "," (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) "," (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_polynom8 :::"emb"::: ) "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) "," (Set (Var "L")) ")" ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ))))))) ; theorem :: POLYNOM8:44 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_polynom8 :::"is_primitive_root_of_degree"::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")))) & (Bool (Set ($#k1_polynom8 :::"emb"::: ) "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_polynom8 :::"emb"::: ) "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) "," (Set (Var "L")) ")" ")" ) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" ($#k6_polynom8 :::"DFT"::: ) "(" (Set "(" (Set "(" ($#k6_polynom8 :::"DFT"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) "," (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ")" ")" ) ($#k2_polynom8 :::"*"::: ) (Set "(" ($#k6_polynom8 :::"DFT"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) "," (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ")" ")" ) ")" ) "," (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) "," (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")))))))) ;