:: EULER_2  semantic presentation begin  


















theorem :: EULER_2:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) "iff" (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_int_2 :::"are_relative_prime"::: )  )  ")" )) ; 
 
theorem :: EULER_2:2 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "t")))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)))) ; 
 
theorem :: EULER_2:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "m"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "m"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Var "m")) "," (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: EULER_2:4 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Var "m")) "," (Set (Var "b"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: EULER_2:5 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n"))))) ; 
 
theorem :: EULER_2:6 (Bool  "for" (Set (Var "l")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "l"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "m")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "l"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n"))))) ; 
 
theorem :: EULER_2:7 (Bool  "for" (Set (Var "l")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "l"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "l"))  ($#k3_nat_1 :::"*"::: )  (Set  "(" (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n"))))) ; 
 
theorem :: EULER_2:8 (Bool  "for" (Set (Var "l")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "l"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "l"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n"))))) ; 
 
theorem :: EULER_2:9 (Bool  "for" (Set (Var "l")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "l"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "l"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n"))))) ; 
 begin  definitionlet "f" be    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "a" be   ($#m1_hidden :::"Nat":::); :: original: :::"*"::: redefine func "a" :::"*"::: "f" ->    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; 
theorem :: EULER_2:10 (Bool  "for" (Set (Var "R1")) "," (Set (Var "R2")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "R1")) "," (Set (Var "R2"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )) "holds"  (Bool (Set   ($#k3_wsierp_1 :::"Product"::: )  (Set (Var "R1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_wsierp_1 :::"Product"::: )  (Set (Var "R2"))))) ; 
 begin  definitionlet "f" be    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "m" be   ($#m1_hidden :::"Nat":::); func "f" :::"mod"::: "m" ->    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: EULER_2:def 1 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "f"))) "holds"  (Bool (Set it  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k4_nat_d :::"mod"::: )  "m"))  ")" )  ")" ); end; 






:: deftheorem    defines :::"mod"::: EULER_2:def 1 :  (Bool  "for" (Set (Var "f")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m"))))  ")" )  ")" )  ")" )))); 
 
theorem :: EULER_2:11 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k3_wsierp_1 :::"Product"::: )  (Set  "(" (Set (Var "f"))  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_wsierp_1 :::"Product"::: )  (Set (Var "f")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))))) ; 
 
theorem :: EULER_2:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))) & (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: EULER_2:13 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")) ")" )  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")))))) ; 
 
theorem :: EULER_2:14 (Bool  "for" (Set (Var "a")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_euler_2 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")) ")" ) ")" )  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k1_euler_2 :::"*"::: )  (Set (Var "F")) ")" )  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")))))) ; 
 
theorem :: EULER_2:15 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_wsierp_1 :::"^"::: )  (Set (Var "G")) ")" )  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "F"))  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")) ")" )  ($#k1_wsierp_1 :::"^"::: )  (Set  "(" (Set (Var "G"))  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")) ")" ))))) ; 
 
theorem :: EULER_2:16 (Bool  "for" (Set (Var "a")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_euler_2 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k1_wsierp_1 :::"^"::: )  (Set (Var "G")) ")" ) ")" )  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_euler_2 :::"*"::: )  (Set (Var "F")) ")" )  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")) ")" )  ($#k1_wsierp_1 :::"^"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_euler_2 :::"*"::: )  (Set (Var "G")) ")" )  ($#k2_euler_2 :::"mod"::: )  (Set (Var "m")) ")" ))))) ; 
 
theorem :: EULER_2:17 (Bool  "for" (Set (Var "a")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "m"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool  "for" (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "b"))) "," (Set (Var "m"))  ($#r1_int_2 :::"are_relative_prime"::: )  ))) ; 
 begin  
theorem :: EULER_2:18 (Bool  "for" (Set (Var "a")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "a")) "," (Set (Var "m"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set  "("  ($#k1_euler_1 :::"Euler"::: )  (Set (Var "m")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: EULER_2:19 (Bool  "for" (Set (Var "a")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) & (Bool (Set (Var "m")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "m"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "m")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "m"))))) ;