:: NAT_5 semantic presentation begin theorem :: NAT_5:1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1)))) ; theorem :: NAT_5:2 (Bool "for" (Set (Var "n0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n0")) "is" ($#v1_abian :::"even"::: ) )) "holds" (Bool "ex" (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "m")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n0")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "k")) ")" ) ($#k24_binop_2 :::"*"::: ) (Set (Var "m")))) ")" ))) ; theorem :: NAT_5:3 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "k")))) & (Bool (Set (Var "m")) "is" ($#v1_abian :::"odd"::: ) )) "holds" (Bool (Set (Var "n")) "," (Set (Var "m")) ($#r1_int_2 :::"are_relative_prime"::: ) )) ; theorem :: NAT_5:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: NAT_5:5 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "n")) "," (Set (Var "m")) ($#k2_tarski :::"}"::: ) ) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: NAT_5:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: NAT_5:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "not" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: NAT_5:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: NAT_5:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f1"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Set (Var "f2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f1"))) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")))))) ; theorem :: NAT_5:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1")))) & (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) & (Bool (Set (Var "f2")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Var "f3")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "Y")) ")" )))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f2")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f3")) ")" ))))) ; theorem :: NAT_5:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f2")) "," (Set (Var "f1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f2")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "f1")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1"))))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f2")))))) ; theorem :: NAT_5:12 (Bool "for" (Set (Var "f2")) "," (Set (Var "f1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_finseq_3 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f2"))))) ; theorem :: NAT_5:13 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "f")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: NAT_5:14 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "n1")) "," (Set (Var "m1")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "n")))) & (Bool (Set (Var "m1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "m")))) & (Bool (Set (Var "n")) "," (Set (Var "m")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set (Var "n1")) "," (Set (Var "m1")) ($#r1_int_2 :::"are_relative_prime"::: ) )) ; theorem :: NAT_5:15 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "n1")) "," (Set (Var "m1")) "," (Set (Var "n2")) "," (Set (Var "m2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "n")))) & (Bool (Set (Var "m1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "m")))) & (Bool (Set (Var "n2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "n")))) & (Bool (Set (Var "m2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "m")))) & (Bool (Set (Var "n")) "," (Set (Var "m")) ($#r1_int_2 :::"are_relative_prime"::: ) ) & (Bool (Set (Set (Var "n1")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n2")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m2"))))) "holds" (Bool "(" (Bool (Set (Var "n1")) ($#r1_hidden :::"="::: ) (Set (Var "n2"))) & (Bool (Set (Var "m1")) ($#r1_hidden :::"="::: ) (Set (Var "m2"))) ")" )) ; theorem :: NAT_5:16 (Bool "for" (Set (Var "n0")) "," (Set (Var "m0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n1")) "," (Set (Var "m1")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "n0")))) & (Bool (Set (Var "m1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "m0"))))) "holds" (Bool (Set (Set (Var "n1")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m1"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set "(" (Set (Var "n0")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m0")) ")" ))))) ; theorem :: NAT_5:17 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n0")) "," (Set (Var "m0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n0")) "," (Set (Var "m0")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set (Set (Var "k")) ($#k6_nat_d :::"gcd"::: ) (Set "(" (Set (Var "n0")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n0")) ")" ) ($#k24_binop_2 :::"*"::: ) (Set "(" (Set (Var "k")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "m0")) ")" ))))) ; theorem :: NAT_5:18 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n0")) "," (Set (Var "m0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n0")) "," (Set (Var "m0")) ($#r1_int_2 :::"are_relative_prime"::: ) ) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set "(" (Set (Var "n0")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m0")) ")" )))) "holds" (Bool "ex" (Set (Var "n1")) "," (Set (Var "m1")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "n1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "n0")))) & (Bool (Set (Var "m1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "m0")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m1")))) ")" )))) ; theorem :: NAT_5:19 (Bool "for" (Set (Var "p")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) )) "holds" (Bool (Set ($#k3_moebius1 :::"NatDivisors"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "k")) ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" )) ; theorem :: NAT_5:20 (Bool "for" (Set (Var "l")) "," (Set (Var "p")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "l"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "l"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n1"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n2"))) & (Bool (Set (Set "(" (Set (Var "l")) ($#k24_binop_2 :::"*"::: ) (Set (Var "n1")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k24_binop_2 :::"*"::: ) (Set (Var "n2")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) )) "holds" (Bool (Set (Var "n1")) ($#r1_hidden :::"="::: ) (Set (Var "n2")))) ; theorem :: NAT_5:21 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n0")) "," (Set (Var "m0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) )) "holds" (Bool (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set "(" (Set (Var "n0")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "m0")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "n0")) ")" ) "," (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "m0")) ")" ) ")" )))) ; begin theorem :: NAT_5:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "n")) "is" ($#v1_int_2 :::"prime"::: ) ) "iff" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k9_newton :::"!"::: ) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) ")" ) ")" )) ; begin theorem :: NAT_5:23 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Set (Set (Var "p")) ($#k4_nat_d :::"mod"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k1_pepin :::"^2"::: ) ")" ) ($#k23_binop_2 :::"+"::: ) (Set "(" (Set (Var "m")) ($#k1_pepin :::"^2"::: ) ")" ))))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set ($#k5_numbers :::"NAT"::: ) ); let "J" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); :: original: :::"|"::: redefine func "f" :::"|"::: "J" -> ($#m1_hidden :::"bag":::) "of" "J"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set ($#k5_numbers :::"NAT"::: ) ); let "J" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); cluster (Set ($#k3_uproots :::"Sum"::: ) (Set "(" "f" ($#k1_nat_5 :::"|"::: ) "J" ")" )) -> ($#v7_ordinal1 :::"natural"::: ) for ($#m1_hidden :::"number"::: ) ; end; theorem :: NAT_5:24 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "F"))) & (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "J")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")))))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k1_nat_5 :::"|"::: ) (Set (Var "J")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_bhsp_5 :::"Func_Seq"::: ) "(" (Set (Var "F")) "," (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "J")) ")" ) ")" ")" )))))) ; theorem :: NAT_5:25 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "I")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k1_nat_5 :::"|"::: ) (Set (Var "J")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "J")) ")" )))))) ; theorem :: NAT_5:26 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "J")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "K")))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k1_nat_5 :::"|"::: ) (Set "(" (Set (Var "J")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k1_nat_5 :::"|"::: ) (Set (Var "J")) ")" ) ")" ) ($#k23_binop_2 :::"+"::: ) (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k1_nat_5 :::"|"::: ) (Set (Var "K")) ")" ) ")" )))))) ; theorem :: NAT_5:27 (Bool "for" (Set (Var "I")) "," (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "J")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "j")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k1_nat_5 :::"|"::: ) (Set (Var "J")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "j"))))))) ; theorem :: NAT_5:28 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set "(" (Set ($#k48_binop_2 :::"multnat"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k16_funct_3 :::":]"::: ) ) ")" ) ($#k1_nat_5 :::"|"::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "J")) "," (Set (Var "K")) ($#k8_mcart_1 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k1_nat_5 :::"|"::: ) (Set (Var "J")) ")" ) ")" ) ($#k24_binop_2 :::"*"::: ) (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "g")) ($#k1_nat_5 :::"|"::: ) (Set (Var "K")) ")" ) ")" )))))) ; definitionlet "k" be ($#m1_hidden :::"Nat":::); func :::"EXP"::: "k" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) means :: NAT_5:def 1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_newton :::"|^"::: ) "k"))); end; :: deftheorem defines :::"EXP"::: NAT_5:def 1 : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_nat_5 :::"EXP"::: ) (Set (Var "k")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_recdef_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Set (Var "k"))))) ")" ))); definitionlet "k", "n" be ($#m1_hidden :::"Nat":::); func :::"sigma"::: "(" "k" "," "n" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: NAT_5:def 2 (Bool "for" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "n" ($#r1_hidden :::"="::: ) (Set (Var "m")))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set "(" ($#k2_nat_5 :::"EXP"::: ) "k" ")" ) ($#k1_nat_5 :::"|"::: ) (Set "(" ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "m")) ")" ) ")" )))) if (Bool "n" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"sigma"::: NAT_5:def 2 : (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_nat_5 :::"sigma"::: ) "(" (Set (Var "k")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set "(" ($#k2_nat_5 :::"EXP"::: ) (Set (Var "k")) ")" ) ($#k1_nat_5 :::"|"::: ) (Set "(" ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "m")) ")" ) ")" )))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_nat_5 :::"sigma"::: ) "(" (Set (Var "k")) "," (Set (Var "n")) ")" )) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" ))); definitionlet "k" be ($#m1_hidden :::"Nat":::); func :::"Sigma"::: "k" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) means :: NAT_5:def 3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_nat_5 :::"sigma"::: ) "(" "k" "," (Set (Var "n")) ")" ))); end; :: deftheorem defines :::"Sigma"::: NAT_5:def 3 : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_nat_5 :::"Sigma"::: ) (Set (Var "k")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_recdef_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_nat_5 :::"sigma"::: ) "(" (Set (Var "k")) "," (Set (Var "n")) ")" ))) ")" ))); definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"sigma"::: "n" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: NAT_5:def 4 (Set ($#k3_nat_5 :::"sigma"::: ) "(" (Num 1) "," "n" ")" ); end; :: deftheorem defines :::"sigma"::: NAT_5:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_nat_5 :::"sigma"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_nat_5 :::"sigma"::: ) "(" (Num 1) "," (Set (Var "n")) ")" ))); theorem :: NAT_5:29 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_nat_5 :::"sigma"::: ) "(" (Set (Var "k")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: NAT_5:30 (Bool "for" (Set (Var "p")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) )) "holds" (Bool (Set ($#k5_nat_5 :::"sigma"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k18_binop_2 :::"/"::: ) (Set "(" (Set (Var "p")) ($#k21_binop_2 :::"-"::: ) (Num 1) ")" )))) ; theorem :: NAT_5:31 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n0"))) & (Bool (Set (Var "n0")) ($#r1_hidden :::"<>"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Num 1) ($#k23_binop_2 :::"+"::: ) (Set (Var "m")) ")" ) ($#k23_binop_2 :::"+"::: ) (Set (Var "n0"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_nat_5 :::"sigma"::: ) (Set (Var "n0")))))) ; theorem :: NAT_5:32 (Bool "for" (Set (Var "m")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n0"))) & (Bool (Set (Var "k")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n0"))) & (Bool (Set (Var "n0")) ($#r1_hidden :::"<>"::: ) (Set (Var "m"))) & (Bool (Set (Var "n0")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k23_binop_2 :::"+"::: ) (Set (Var "m")) ")" ) ($#k23_binop_2 :::"+"::: ) (Set (Var "k")) ")" ) ($#k23_binop_2 :::"+"::: ) (Set (Var "n0"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_nat_5 :::"sigma"::: ) (Set (Var "n0")))))) ; theorem :: NAT_5:33 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k5_nat_5 :::"sigma"::: ) (Set (Var "n0"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n0")) ($#k23_binop_2 :::"+"::: ) (Set (Var "m")))) & (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n0"))) & (Bool (Set (Var "n0")) ($#r1_hidden :::"<>"::: ) (Set (Var "m")))) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "n0")) "is" ($#v1_int_2 :::"prime"::: ) ) ")" ))) ; definitionlet "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ); attr "f" is :::"multiplicative"::: means :: NAT_5:def 5 (Bool "for" (Set (Var "n0")) "," (Set (Var "m0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n0")) "," (Set (Var "m0")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set "f" ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "n0")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_recdef_1 :::"."::: ) (Set (Var "n0")) ")" ) ($#k24_binop_2 :::"*"::: ) (Set "(" "f" ($#k1_recdef_1 :::"."::: ) (Set (Var "m0")) ")" )))); end; :: deftheorem defines :::"multiplicative"::: NAT_5:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_nat_5 :::"multiplicative"::: ) ) "iff" (Bool "for" (Set (Var "n0")) "," (Set (Var "m0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n0")) "," (Set (Var "m0")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "n0")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "n0")) ")" ) ($#k24_binop_2 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "m0")) ")" )))) ")" )); theorem :: NAT_5:34 (Bool "for" (Set (Var "f")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_nat_5 :::"multiplicative"::: ) ) & (Bool "(" "for" (Set (Var "n0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "n0"))) ($#r1_hidden :::"="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k1_nat_5 :::"|"::: ) (Set "(" ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "n0")) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v1_nat_5 :::"multiplicative"::: ) )) ; theorem :: NAT_5:35 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_nat_5 :::"EXP"::: ) (Set (Var "k"))) "is" ($#v1_nat_5 :::"multiplicative"::: ) )) ; theorem :: NAT_5:36 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_nat_5 :::"Sigma"::: ) (Set (Var "k"))) "is" ($#v1_nat_5 :::"multiplicative"::: ) )) ; theorem :: NAT_5:37 (Bool "for" (Set (Var "n0")) "," (Set (Var "m0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n0")) "," (Set (Var "m0")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set ($#k5_nat_5 :::"sigma"::: ) (Set "(" (Set (Var "n0")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_nat_5 :::"sigma"::: ) (Set (Var "n0")) ")" ) ($#k24_binop_2 :::"*"::: ) (Set "(" ($#k5_nat_5 :::"sigma"::: ) (Set (Var "m0")) ")" )))) ; begin definitionlet "n0" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); attr "n0" is :::"perfect"::: means :: NAT_5:def 6 (Bool (Set ($#k5_nat_5 :::"sigma"::: ) "n0") ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k24_binop_2 :::"*"::: ) "n0")); end; :: deftheorem defines :::"perfect"::: NAT_5:def 6 : (Bool "for" (Set (Var "n0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "n0")) "is" ($#v2_nat_5 :::"perfect"::: ) ) "iff" (Bool (Set ($#k5_nat_5 :::"sigma"::: ) (Set (Var "n0"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k24_binop_2 :::"*"::: ) (Set (Var "n0")))) ")" )); theorem :: NAT_5:38 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Set (Var "n0")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k24_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Var "n0")) "is" ($#v2_nat_5 :::"perfect"::: ) ))) ; theorem :: NAT_5:39 (Bool "for" (Set (Var "n0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n0")) "is" ($#v1_abian :::"even"::: ) ) & (Bool (Set (Var "n0")) "is" ($#v2_nat_5 :::"perfect"::: ) )) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Set (Var "n0")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k24_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))) ")" ))) ; begin definitionfunc :::"Euler_phi"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) means :: NAT_5:def 7 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euler_1 :::"Euler"::: ) (Set (Var "k"))))); end; :: deftheorem defines :::"Euler_phi"::: NAT_5:def 7 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_5 :::"Euler_phi"::: ) )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euler_1 :::"Euler"::: ) (Set (Var "k"))))) ")" )); theorem :: NAT_5:40 (Bool "for" (Set (Var "n0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set ($#k6_nat_5 :::"Euler_phi"::: ) ) ($#k1_nat_5 :::"|"::: ) (Set "(" ($#k3_moebius1 :::"NatDivisors"::: ) (Set (Var "n0")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n0")))) ;