:: UNIROOTS semantic presentation begin scheme :: UNIROOTS:sch 1 CompIndNE{ P1[ ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::)] } : (Bool "for" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool P1[(Set (Var "k"))])) provided (Bool "for" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool P1[(Set (Var "n"))]) ")" )) "holds" (Bool P1[(Set (Var "k"))])) proof end; theorem :: UNIROOTS:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: UNIROOTS:2 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "f")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "g")))))) ; theorem :: UNIROOTS:3 (Bool "for" (Set (Var "s")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "s")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "r")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_uproots :::"canFS"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "r")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ")" )) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" "(" (Set (Var "s")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ")" ) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "r"))))))) ; theorem :: UNIROOTS:4 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_int_1 :::"integer"::: ) ) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "f"))) "is" ($#v1_int_1 :::"integer"::: ) )) ; theorem :: UNIROOTS:5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Set (Var "r1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k8_group_1 :::"*"::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")))) ")" ))) ; theorem :: UNIROOTS:6 (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "r")) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) ))) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set ($#k1_hahnban1 :::"[**"::: ) (Set (Var "q")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "r")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "q")) ($#k10_binop_2 :::"-"::: ) (Num 1))))) ; theorem :: UNIROOTS:7 (Bool "for" (Set (Var "ps")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "ps"))))) "holds" (Bool (Set (Set (Var "ps")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "x"))) ")" )) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "ps"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "x"))))) ; theorem :: UNIROOTS:8 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) "," (Set (Var "n")) ")" ))) ; theorem :: UNIROOTS:9 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "i")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ))) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "i")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ))) ")" )) ; theorem :: UNIROOTS:10 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "i")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "i")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ))) ; theorem :: UNIROOTS:11 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "i")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "i")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ) ($#k8_group_1 :::"*"::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "j")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "j")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k23_binop_2 :::"+"::: ) (Set (Var "j")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k23_binop_2 :::"+"::: ) (Set (Var "j")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ))) ; theorem :: UNIROOTS:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "n")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "m")) ")" ))))) ; theorem :: UNIROOTS:13 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Integer":::))) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) "is" ($#m1_hidden :::"Integer":::)))) ; theorem :: UNIROOTS:14 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_hidden :::"Integer":::)) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) "is" ($#m1_hidden :::"Integer":::))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) bbbadV5_VECTSP_1() ($#v6_vectsp_1 :::"left_unital"::: ) bbbadV2_RLVECT_1() bbbadV3_RLVECT_1() bbbadV4_RLVECT_1() ($#v1_vectsp_2 :::"domRing-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) bbbadV5_VECTSP_1() ($#v6_vectsp_1 :::"left_unital"::: ) bbbadV2_RLVECT_1() bbbadV3_RLVECT_1() bbbadV4_RLVECT_1() for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; begin definitionlet "R" be ($#l6_algstr_0 :::"Skew-Field":::); func :::"MultGroup"::: "R" -> ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) means :: UNIROOTS:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) "R")) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "R") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" ); end; :: deftheorem defines :::"MultGroup"::: UNIROOTS:def 1 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "b2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_uniroots :::"MultGroup"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "R")))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "R"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) ")" ) ")" ))); theorem :: UNIROOTS:15 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Skew-Field":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set (Var "R")) ")" )) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: UNIROOTS:16 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "c")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))))))) ; theorem :: UNIROOTS:17 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Skew-Field":::) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set (Var "R")) ")" )))) ; registrationlet "R" be ($#v8_struct_0 :::"finite"::: ) ($#l6_algstr_0 :::"Skew-Field":::); cluster (Set ($#k1_uniroots :::"MultGroup"::: ) "R") -> ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ; end; theorem :: UNIROOTS:18 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l6_algstr_0 :::"Skew-Field":::) "holds" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_group_1 :::"card"::: ) (Set (Var "R")) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1)))) ; theorem :: UNIROOTS:19 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set (Var "R")) ")" )))) "holds" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))))) ; theorem :: UNIROOTS:20 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Skew-Field":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))))) ; begin definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "n" :::"-roots_of_1"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) equals :: UNIROOTS:def 2 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) : (Bool (Set (Var "x")) "is" ($#m1_comptrig :::"CRoot"::: ) "of" "n" "," (Set ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) "}" ; end; :: deftheorem defines :::"-roots_of_1"::: UNIROOTS:def 2 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) : (Bool (Set (Var "x")) "is" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) "}" )); theorem :: UNIROOTS:21 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) )) "iff" (Bool (Set (Var "x")) "is" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) ")" ))) ; theorem :: UNIROOTS:22 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ))) ; theorem :: UNIROOTS:23 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ))) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: UNIROOTS:24 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) )) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ))) ")" ))) ; theorem :: UNIROOTS:25 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k5_binop_2 :::"*"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) )))) ; theorem :: UNIROOTS:26 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) "}" )) ; theorem :: UNIROOTS:27 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "n" ($#k2_uniroots :::"-roots_of_1"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set "n" ($#k2_uniroots :::"-roots_of_1"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: UNIROOTS:28 (Bool "for" (Set (Var "n")) "," (Set (Var "ni")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "ni")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "ni")) ($#k2_uniroots :::"-roots_of_1"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ))) ; theorem :: UNIROOTS:29 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set (Var "R")) ")" ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "k")) ")" )))))) ; theorem :: UNIROOTS:30 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "x")) "is" ($#v4_group_1 :::"being_of_order_0"::: ) )))) ; theorem :: UNIROOTS:31 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ))) "holds" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_nat_d :::"div"::: ) (Set "(" (Set (Var "k")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n")) ")" )))))) ; theorem :: UNIROOTS:32 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" )))) ; theorem :: UNIROOTS:33 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) "st" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: UNIROOTS:34 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "x"))) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) )) ")" ))) ; theorem :: UNIROOTS:35 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) : (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "x"))) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) "}" )) ; theorem :: UNIROOTS:36 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) )) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "y"))) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) ")" )) ")" ))) ; definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "n" :::"-th_roots_of_1"::: -> ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) means :: UNIROOTS:def 3 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "n" ($#k2_uniroots :::"-roots_of_1"::: ) )) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set ($#k1_complfld :::"F_Complex"::: ) )) ($#k1_realset1 :::"||"::: ) (Set "(" "n" ($#k2_uniroots :::"-roots_of_1"::: ) ")" ))) ")" ); end; :: deftheorem defines :::"-th_roots_of_1"::: UNIROOTS:def 3 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_uniroots :::"-th_roots_of_1"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) )) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set ($#k1_complfld :::"F_Complex"::: ) )) ($#k1_realset1 :::"||"::: ) (Set "(" (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ")" ))) ")" ) ")" ))); theorem :: UNIROOTS:37 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k3_uniroots :::"-th_roots_of_1"::: ) ) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) ; begin definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; func :::"unital_poly"::: "(" "L" "," "n" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" equals :: UNIROOTS:def 4 (Set (Set "(" (Set "(" ($#k9_polynom3 :::"0_."::: ) "L" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) "L" ")" ) ")" ) ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" "n" "," (Set "(" ($#k1_group_1 :::"1_"::: ) "L" ")" ) ")" ); end; :: deftheorem defines :::"unital_poly"::: UNIROOTS:def 4 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k4_uniroots :::"unital_poly"::: ) "(" (Set (Var "L")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ) ")" ) ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set (Var "n")) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ) ")" )))); theorem :: UNIROOTS:38 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set (Var "L")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ))) & (Bool (Set (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set (Var "L")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "L")))) ")" ))) ; theorem :: UNIROOTS:39 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set (Var "L")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))))) ; theorem :: UNIROOTS:40 (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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set (Var "L")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k4_uniroots :::"unital_poly"::: ) "(" "L" "," "n" ")" ) -> ($#v1_uproots :::"non-zero"::: ) ; end; theorem :: UNIROOTS:41 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ")" ) ($#k4_binop_2 :::"-"::: ) (Num 1))))) ; theorem :: UNIROOTS:42 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_polynom5 :::"Roots"::: ) (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ))) ; theorem :: UNIROOTS:43 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")))) ")" )))) ; theorem :: UNIROOTS:44 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1))) ")" )))) ; theorem :: UNIROOTS:45 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k8_uproots :::"BRoots"::: ) (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ")" ) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ))) ; theorem :: UNIROOTS:46 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" "(" (Set "(" (Set (Var "n")) ($#k2_uniroots :::"-roots_of_1"::: ) ")" ) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ")" )))) ; theorem :: UNIROOTS:47 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "i")) "is" ($#m1_hidden :::"Integer":::))) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" ) "is" ($#m1_hidden :::"Integer":::)))) ; begin definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); func :::"cyclotomic_poly"::: "d" -> ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) means :: UNIROOTS:def 5 (Bool "ex" (Set (Var "s")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) : (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) "d") "}" ) & (Bool it ($#r2_funct_2 :::"="::: ) (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" "(" (Set (Var "s")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ")" ))) ")" )); end; :: deftheorem defines :::"cyclotomic_poly"::: UNIROOTS:def 5 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "d")))) "iff" (Bool "ex" (Set (Var "s")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) : (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) "}" ) & (Bool (Set (Var "b2")) ($#r2_funct_2 :::"="::: ) (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" "(" (Set (Var "s")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ")" ))) ")" )) ")" ))); theorem :: UNIROOTS:48 (Bool (Set ($#k5_uniroots :::"cyclotomic_poly"::: ) (Num 1)) ($#r2_funct_2 :::"="::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ")" ) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k4_polynom5 :::"%>"::: ) )) ; theorem :: UNIROOTS:49 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" )) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "i")))) ")" ")" ) ")" )) "holds" (Bool (Set ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f")))))) ; theorem :: UNIROOTS:50 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ))(Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "i")))) ")" ")" ) ")" ) & (Bool (Set ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "n")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "p")))) ")" )))) ; theorem :: UNIROOTS:51 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "d")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "d")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k19_binop_2 :::"-"::: ) (Num 1))) ")" ) & (Bool (Set (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "d")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) "is" ($#v1_int_1 :::"integer"::: ) ) ")" ))) ; theorem :: UNIROOTS:52 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) "is" ($#m1_hidden :::"Integer":::))) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "d")) ")" ) "," (Set (Var "z")) ")" ) "is" ($#m1_hidden :::"Integer":::)))) ; theorem :: UNIROOTS:53 (Bool "for" (Set (Var "n")) "," (Set (Var "ni")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" )) (Bool "for" (Set (Var "s")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) : (Bool "(" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "y"))) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) & (Bool (Bool "not" (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "y"))) ($#r1_nat_d :::"divides"::: ) (Set (Var "ni")))) & (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Var "n"))) ")" ) "}" ) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) "or" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "ni"))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) & (Bool (Bool "not" (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "ni")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "i")))) ")" ")" ) ")" )) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" "(" (Set (Var "s")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ")" )))))) ; theorem :: UNIROOTS:54 (Bool "for" (Set (Var "n")) "," (Set (Var "ni")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "ni")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "ni")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ))(Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "(" "(" (Bool (Bool "(" "not" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) "or" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "ni"))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) & (Bool (Bool "not" (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "ni")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "i")))) ")" ")" ) ")" ) & (Bool (Set ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "ni")) ")" ")" ) ($#k13_polynom3 :::"*'"::: ) (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "n")) ")" ) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "p")))) ")" )))) ; theorem :: UNIROOTS:55 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" )) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) "or" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) "or" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "i")))) ")" ) ")" )) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "c")) ")" ) "is" ($#v1_int_1 :::"integer"::: ) ))))) ; theorem :: UNIROOTS:56 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "q")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "qc")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "qc")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "n")) ")" ) "," (Set (Var "qc")) ")" )) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "qc")) ")" ))) "holds" (Bool (Set (Var "j")) ($#r1_int_1 :::"divides"::: ) (Set (Var "k")))))) ; theorem :: UNIROOTS:57 (Bool "for" (Set (Var "n")) "," (Set (Var "ni")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "ni")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "ni")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "qc")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "qc")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "n")) ")" ) "," (Set (Var "qc")) ")" )) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "qc")) ")" )) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k4_uniroots :::"unital_poly"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "ni")) ")" ")" ) "," (Set (Var "qc")) ")" ))) "holds" (Bool (Set (Var "j")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "k")) ($#k5_int_1 :::"div"::: ) (Set (Var "l")))))))) ; theorem :: UNIROOTS:58 (Bool "for" (Set (Var "n")) "," (Set (Var "q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "qc")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "qc")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "n")) ")" ) "," (Set (Var "qc")) ")" ))) "holds" (Bool (Set (Var "j")) ($#r1_int_1 :::"divides"::: ) (Set (Set "(" (Set (Var "q")) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1)))))) ; theorem :: UNIROOTS:59 (Bool "for" (Set (Var "n")) "," (Set (Var "ni")) "," (Set (Var "q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "ni")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "ni")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "qc")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "qc")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "n")) ")" ) "," (Set (Var "qc")) ")" ))) "holds" (Bool (Set (Var "j")) ($#r1_int_1 :::"divides"::: ) (Set (Set "(" (Set "(" (Set (Var "q")) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k13_newton :::"|^"::: ) (Set (Var "ni")) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1) ")" )))))) ; theorem :: UNIROOTS:60 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "q")))) "holds" (Bool "for" (Set (Var "qc")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "qc")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uniroots :::"cyclotomic_poly"::: ) (Set (Var "n")) ")" ) "," (Set (Var "qc")) ")" ))) "holds" (Bool (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "q")) ($#k21_binop_2 :::"-"::: ) (Num 1))))))) ;