:: INT_7 semantic presentation begin theorem :: INT_7:1 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: INT_7:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "q")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "q")) ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k11_pre_poly :::"+"::: ) (Set (Var "q"))) ($#r6_pboole :::"="::: ) (Set (Var "r"))))) ; theorem :: INT_7:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "q")) ")" )))) "holds" (Bool (Set (Var "p")) ($#r6_pboole :::"="::: ) (Set (Var "q"))))) ; theorem :: INT_7:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r6_pboole :::"="::: ) (Set (Var "q"))))) ; definitionlet "p" be ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ); attr "p" is :::"prime-factorization-like"::: means :: INT_7:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Prime":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_polynom2 :::"support"::: ) "p"))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set "p" ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Set (Var "n")))) ")" ))); end; :: deftheorem defines :::"prime-factorization-like"::: INT_7:def 1 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Prime":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "p")) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Set (Var "n")))) ")" ))) ")" )); registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k13_nat_3 :::"prime_factorization"::: ) "n") -> ($#v1_int_7 :::"prime-factorization-like"::: ) ; end; theorem :: INT_7:5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "m")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))))) ; theorem :: INT_7:6 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Prime":::) "st" (Bool (Bool (Set (Var "b")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) ) & (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "b"))) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "b")))) & (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_wsierp_1 :::"Product"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "b")) ")" ) ")" )))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "b"))))))) ; theorem :: INT_7:7 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) "st" (Bool (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "p"))) ($#r1_int_1 :::"divides"::: ) (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "q"))))) ; theorem :: INT_7:8 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Prime":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_int_1 :::"divides"::: ) (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "p")))) ")" ))) ; theorem :: INT_7:9 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "m")) ")" ) ")" )))) ; theorem :: INT_7:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k5_nat_3 :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "b1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "b2")) ")" ))))) ; theorem :: INT_7:11 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "n")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "m")) ")" ) ")" )))) ; theorem :: INT_7:12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) ) & (Bool (Set (Var "q")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) ) & (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "p"))) "," (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "q"))) ($#r1_int_2 :::"are_relative_prime"::: ) )) ; theorem :: INT_7:13 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) )) "holds" (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: INT_7:14 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) )) "holds" (Bool "(" (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: INT_7:15 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) ) & (Bool (Set (Var "q")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) ) & (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "p")) ($#r8_pboole :::"="::: ) (Set (Var "q")))) ; theorem :: INT_7:16 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_7 :::"prime-factorization-like"::: ) ) & (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k8_nat_3 :::"Product"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k13_nat_3 :::"ppf"::: ) (Set (Var "n"))) ($#r8_pboole :::"="::: ) (Set (Var "p"))))) ; theorem :: INT_7:17 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "ex" (Set (Var "m0")) "," (Set (Var "n0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "n")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n0")) ($#k4_nat_1 :::"*"::: ) (Set (Var "m0")))) & (Bool (Set (Set (Var "n0")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m0"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "n0")) ($#r1_int_1 :::"divides"::: ) (Set (Var "n"))) & (Bool (Set (Var "m0")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))) & (Bool (Set (Var "n0")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m0")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); assume (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Const "n"))) ; func :::"Segm0"::: "n" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: INT_7:def 2 (Set (Set "(" ($#k7_card_1 :::"Segm"::: ) "n" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"Segm0"::: INT_7:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k1_int_7 :::"Segm0"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_card_1 :::"Segm"::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )))); theorem :: INT_7:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_int_7 :::"Segm0"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) ; definitionlet "n" be ($#m1_hidden :::"Prime":::); func :::"multint0"::: "n" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_int_7 :::"Segm0"::: ) "n" ")" ) equals :: INT_7:def 3 (Set (Set "(" ($#k7_int_3 :::"multint"::: ) "n" ")" ) ($#k1_realset1 :::"||"::: ) (Set "(" ($#k1_int_7 :::"Segm0"::: ) "n" ")" )); end; :: deftheorem defines :::"multint0"::: INT_7:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set ($#k2_int_7 :::"multint0"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_int_3 :::"multint"::: ) (Set (Var "n")) ")" ) ($#k1_realset1 :::"||"::: ) (Set "(" ($#k1_int_7 :::"Segm0"::: ) (Set (Var "n")) ")" )))); theorem :: INT_7:19 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool "(" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" ($#k1_int_7 :::"Segm0"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k2_int_7 :::"multint0"::: ) (Set (Var "p")) ")" ) "#)" ) "is" ($#v3_group_1 :::"associative"::: ) ) & (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" ($#k1_int_7 :::"Segm0"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k2_int_7 :::"multint0"::: ) (Set (Var "p")) ")" ) "#)" ) "is" ($#v5_group_1 :::"commutative"::: ) ) & (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" ($#k1_int_7 :::"Segm0"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k2_int_7 :::"multint0"::: ) (Set (Var "p")) ")" ) "#)" ) "is" ($#v2_group_1 :::"Group-like"::: ) ) ")" )) ; definitionlet "p" be ($#m1_hidden :::"Prime":::); func :::"Z/Z*"::: "p" -> ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) equals :: INT_7:def 4 (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" ($#k1_int_7 :::"Segm0"::: ) "p" ")" ) "," (Set "(" ($#k2_int_7 :::"multint0"::: ) "p" ")" ) "#)" ); end; :: deftheorem defines :::"Z/Z*"::: INT_7:def 4 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" ($#k1_int_7 :::"Segm0"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k2_int_7 :::"multint0"::: ) (Set (Var "p")) ")" ) "#)" ))); theorem :: INT_7:20 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y1")))) "holds" (Bool (Set (Set (Var "x")) ($#k8_group_1 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k8_group_1 :::"*"::: ) (Set (Var "y1"))))))) ; theorem :: INT_7:21 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool "(" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "p")) ")" ))) ")" )) ; theorem :: INT_7:22 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "x")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k11_algstr_0 :::"""::: ) ))))) ; registrationlet "p" be ($#m1_hidden :::"Prime":::); cluster (Set ($#k3_int_7 :::"Z/Z*"::: ) "p") -> ($#v8_struct_0 :::"finite"::: ) ($#v5_group_1 :::"commutative"::: ) ; end; theorem :: INT_7:23 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set "(" ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) ; theorem :: INT_7:24 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v4_group_1 :::"being_of_order_0"::: ) ))) "holds" (Bool "ex" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n")))) & (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k6_group_1 :::"ord"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")))) ")" ))))) ; theorem :: INT_7:25 (Bool "for" (Set (Var "G")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "G")) "is" ($#v8_struct_0 :::"finite"::: ) ) & (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool (Set (Set (Var "n")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "m"))))))) ; theorem :: INT_7:26 (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 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "p")) "is" ($#v1_uproots :::"non-zero"::: ) ))) ; theorem :: INT_7:27 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k6_polynom5 :::"Roots"::: ) (Set (Var "f"))) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ) & (Bool "ex" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "f")))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k6_polynom5 :::"Roots"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" )) ")" ))) ; theorem :: INT_7:28 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set "(" ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set "(" ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "n")) ")" )))))) ; theorem :: INT_7:29 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "b")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" ))))) ; theorem :: INT_7:30 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "d")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "G")) "is" ($#v8_struct_0 :::"finite"::: ) ) & (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k4_nat_1 :::"*"::: ) (Set (Var "l"))))) "holds" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set "(" (Set (Var "z")) ($#k5_group_1 :::"|^"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "l")))))) ; theorem :: INT_7:31 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set ($#k3_int_7 :::"Z/Z*"::: ) (Set (Var "p"))) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::))) ;