:: EULER_1  semantic presentation begin  















theorem :: EULER_1:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) "iff" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: EULER_1:2 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Var "n")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool (Set (Var "k")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: EULER_1:3 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )   "{"  (Set (Var "kk")) where kk "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Var "n")) "," (Set (Var "kk"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "kk"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "kk"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" )  "}"  ) "iff" (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set (Var "n"))) & (Bool (Bool  "not" (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )))  ")" )  ")" )) ; 
 
theorem :: EULER_1:4 (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "A")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))))) ; 
 
theorem :: EULER_1:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))) ; 
 
theorem :: EULER_1:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: EULER_1:7 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: EULER_1:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b"))))) ; 
 
theorem :: EULER_1:9 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool  "ex" (Set (Var "i0")) "," (Set (Var "j0")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i0"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "j0"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) & (Bool  "("   "for" (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "l"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "j"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Var "l"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "l")))  ")" )  ")" ))) ; 
 
theorem :: EULER_1:10 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set  "(" (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "j"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k")))))) ; 
 
theorem :: EULER_1:11 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "B"))))))) ; 
 
theorem :: EULER_1:12 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ) ")" )  ($#k6_int_1 :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "n"))))) ; 
 
theorem :: EULER_1:13 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "c"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Var "c"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "b")))) ; 
 
theorem :: EULER_1:14 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))) "," (Set (Var "c"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: EULER_1:15 (Bool  "for" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set  "(" (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "y")) ")" )))) ; 
 
theorem :: EULER_1:16 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))))) ; 
 begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Euler"::: "n" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: EULER_1:def 1 (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set (Var "k")) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool "n" "," (Set (Var "k"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  "n")  ")" )  "}"  ); end; 





:: deftheorem    defines :::"Euler"::: EULER_1:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_euler_1 :::"Euler"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set (Var "k")) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Var "n")) "," (Set (Var "k"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" )  "}"  ))); 
 
theorem :: EULER_1:17 (Bool (Set   ($#k1_euler_1 :::"Euler"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: EULER_1:18 (Bool (Set   ($#k1_euler_1 :::"Euler"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: EULER_1:19 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_euler_1 :::"Euler"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 
theorem :: EULER_1:20 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool (Set   ($#k1_euler_1 :::"Euler"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 
theorem :: EULER_1:21 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set   ($#k1_euler_1 :::"Euler"::: )  (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_euler_1 :::"Euler"::: )  (Set (Var "m")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k1_euler_1 :::"Euler"::: )  (Set (Var "n")) ")" )))) ;