:: NAT_4  semantic presentation begin  
theorem :: NAT_4:1 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Set (Var "s"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "s")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "r"))))) "holds"  (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) ; 
 
theorem :: NAT_4:2 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) ; 
 
theorem :: NAT_4:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n")))) ; 
 
theorem :: NAT_4:4 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "n"))  ($#k6_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) ))) "holds"  (Bool (Set (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set (Var "k"))))) ; 
 
theorem :: NAT_4:5 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "n"))  ($#k6_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k10_real_1 :::"/"::: )  (Set (Var "n"))))) ; 
 
theorem :: NAT_4:6 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k6_newton :::"choose"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Num 4)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: NAT_4:7 (Bool  "for" (Set (Var "n")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "p"))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p")))) "holds"  (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p")))  ")" )) ; 
 
theorem :: NAT_4:8 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "p"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p")))  ")" ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "p"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "n"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))  ")" ))) ; 
 
theorem :: NAT_4:9 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "j"))  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "l")))) & (Bool (Set (Var "l"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "l")))) "holds"  (Bool  "not" (Bool (Set (Var "j"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "i"))))) ; 
 
theorem :: NAT_4:10 (Bool  "for" (Set (Var "n")) "," (Set (Var "q")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "q"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "q"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k6_nat_d :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NAT_4:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "b")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "c")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "b")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "c")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "c"))))) ; 
 
theorem :: NAT_4:12 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) "or" (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "p"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p")))  ")" ))  ")" ) "iff" (Bool  "not" (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ))  ")" )) ; 
 
theorem :: NAT_4:13 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "k"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "k"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  )  ")" ))) ; 
 
theorem :: NAT_4:14 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "n"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p"))) & (Bool (Set (Var "n")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool  "not" (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "p"))))  ")" )  ")" )  ")" )) ; 
 
theorem :: NAT_4:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: NAT_4:16 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "a")) ")" )))) "holds"  (Bool  "ex" (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))  ")" ))))) ; 
 
theorem :: NAT_4:17 (Bool  "for" (Set (Var "k")) "," (Set (Var "q")) "," (Set (Var "n")) "," (Set (Var "d")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "q")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "d"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) & (Bool (Bool  "not" (Set (Var "d"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set (Var "n")) ")" ))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_nat_d :::"divides"::: )  (Set (Var "d")))) ; 
 
theorem :: NAT_4:18 (Bool  "for" (Set (Var "q1")) "," (Set (Var "q")) "," (Set (Var "n1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "q1"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set (Var "n1")))) & (Bool (Set (Var "q")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "q1")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "q1")))) ; 
 
theorem :: NAT_4:19 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p")))) "holds"  (Bool  "not" (Bool (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "n"))  ($#k9_newton :::"!"::: )  ))))) ; 
 
theorem :: NAT_4:20 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "b"))))  ")" )) "holds"  (Bool  "ex" (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_nat_1 :::"*"::: )  (Set (Var "c")))))) ; 
 
theorem :: NAT_4:21 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "b"))))  ")" )) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: NAT_4:22 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "p1"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "p1"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "m")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p2"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "p2"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "m")) ")" ))) & (Bool (Set (Set (Var "p1"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))))) ; 
 begin  
theorem :: NAT_4:23 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "n1")) "," (Set (Var "p")) "," (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "n"))  ($#k9_real_1 :::"-"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set (Var "n1")) ")" ))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n1"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "q")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set (Set  "(" (Set (Var "a"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "q")) ")" ) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set (Var "n1")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NAT_4:24 (Bool  "for" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "n"))  ($#k9_real_1 :::"-"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "c")))) & (Bool (Set (Var "f"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "f"))) & (Bool (Set (Var "q")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool  "ex" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "q")) ")" ) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" ))  ")" )) "holds"  (Bool (Set (Var "n")) "is"   ($#v1_int_2 :::"prime"::: )  )) ; 
 
theorem :: NAT_4:25 (Bool  "for" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "d")) "," (Set (Var "n1")) "," (Set (Var "a")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "n"))  ($#k9_real_1 :::"-"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set (Var "n1")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "d")))) & (Bool (Set (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set (Var "n1")))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "d"))) & (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "q")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "q")) ")" ) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "n")) "is"   ($#v1_int_2 :::"prime"::: )  )) ; 
 begin  
theorem :: NAT_4:26 (Bool (Num 7) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:27 (Bool (Num 11) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:28 (Bool (Num 13) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:29 (Bool (Num 19) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:30 (Bool (Num 23) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:31 (Bool (Num 37) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:32 (Bool (Num 43) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:33 (Bool (Num 83) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:34 (Bool (Num 139) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:35 (Bool (Num 163) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:36 (Bool (Num 317) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:37 (Bool (Num 631) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:38 (Bool (Num 1259) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:39 (Bool (Num 2503) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: NAT_4:40 (Bool (Num 4001) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 begin  
theorem :: NAT_4:41 (Bool  "for" (Set (Var "f")) "," (Set (Var "f0")) "," (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f0"))  ($#k4_rvsum_1 :::"+"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f0")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f1")) ")" )))) ; 
 
theorem :: NAT_4:42 (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F"))))) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set (Var "F")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: NAT_4:43 (Bool  "for" (Set (Var "X1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X2")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X1"))  ($#r1_tarski :::"c="::: )  (Set (Var "X2"))) & (Bool (Set (Var "X2"))  ($#r1_tarski :::"c="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool (Bool  "not" (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "X2"))))) "holds"  (Bool (Set   ($#k3_wsierp_1 :::"Product"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set (Var "X1")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_wsierp_1 :::"Product"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set (Var "X2")) ")" ))))) ; 
 
theorem :: NAT_4:44 (Bool  "for" (Set (Var "a")) "," (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k10_newton :::"SetPrimes"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_newton :::"SetPrimes"::: )  )) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "k")))) & (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set   ($#k14_finseq_1 :::"Sgm"::: )  (Set (Var "X")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_wsierp_1 :::"Product"::: )  (Set (Var "F"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "F"))))) "implies" (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "F")))))) "implies" (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" ))))) ; 
 
theorem :: NAT_4:45 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_wsierp_1 :::"Product"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )   "{"  (Set (Var "p")) where p "is"   ($#v1_int_2 :::"prime"::: )     ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))  "}"   ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 4)  ($#k4_power :::"to_power"::: )  (Set (Var "n"))))) ; 
 
theorem :: NAT_4:46 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k3_wsierp_1 :::"Product"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )   "{"  (Set (Var "p")) where p "is"   ($#v1_int_2 :::"prime"::: )     ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x")))  "}"   ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 4)  ($#k4_power :::"to_power"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )))) ; 
 
theorem :: NAT_4:47 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Set (Var "f"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Num 1))) "implies" (Bool (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))  ")"  &  "("  (Bool (Bool (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))) "implies" (Bool (Set (Set (Var "f"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Set (Set (Var "f"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "not" (Bool (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))))) "implies" (Bool (Set (Set (Var "f"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )  ")" ) & (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wsierp_1 :::"Sum"::: )  (Set (Var "f"))))  ")" )))) ; 
 
theorem :: NAT_4:48 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::) (Bool  "ex" (Set (Var "f")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "n"))  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ))  ")" ) & (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set  "(" (Set (Var "n"))  ($#k9_newton :::"!"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wsierp_1 :::"Sum"::: )  (Set (Var "f"))))  ")" )))) ; 
 
theorem :: NAT_4:49 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::) (Bool  "ex" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) )  ($#k5_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "n"))  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ) ")" )))  ")" ) & (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k6_newton :::"choose"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "f"))))  ")" )))) ; 
 definitionlet "f" be    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p" be   ($#m1_hidden :::"Prime":::); func "p" :::"|-count"::: "f" ->    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: NAT_4: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 :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set "p"  ($#k11_nat_3 :::"|-count"::: )  (Set  "(" "f"  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")) ")" )))  ")" )  ")" ); end; 






:: deftheorem    defines :::"|-count"::: NAT_4:def 1 :  (Bool  "for" (Set (Var "f")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  (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 "p"))  ($#k1_nat_4 :::"|-count"::: )  (Set (Var "f")))) "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 :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b3"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set  "(" (Set (Var "f"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")) ")" )))  ")" )  ")" )  ")" )))); 
 
theorem :: NAT_4:50 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_nat_4 :::"|-count"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: NAT_4:51 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_nat_4 :::"|-count"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_wsierp_1 :::"^"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k1_nat_4 :::"|-count"::: )  (Set (Var "f1")) ")" )  ($#k1_wsierp_1 :::"^"::: )  (Set  "(" (Set (Var "p"))  ($#k1_nat_4 :::"|-count"::: )  (Set (Var "f2")) ")" ))))) ; 
 
theorem :: NAT_4:52 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  (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 "p"))  ($#k1_nat_4 :::"|-count"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "n")) ($#k3_pre_poly :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set  "(" (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "n")) ")" ) ($#k3_pre_poly :::"*>"::: ) )))) ; 
 
theorem :: NAT_4:53 (Bool  "for" (Set (Var "f")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set   ($#k3_wsierp_1 :::"Product"::: )  (Set (Var "f")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set  "("  ($#k3_wsierp_1 :::"Product"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wsierp_1 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k1_nat_4 :::"|-count"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: NAT_4:54 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f1"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))) & (Bool (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set (Var "f1")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set (Var "f2"))))) ; 
 
theorem :: NAT_4:55 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_power :::"to_power"::: )  (Set (Var "n")))))) ; 
 scheme  :: NAT_4:sch 1 scheme1{ P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "m")) "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"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "p9"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "p9"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "m")) ")" ) ")" ) where p9 "is"   ($#v1_int_2 :::"prime"::: )     ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool P1[(Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "p9"))])  "}"  )) "holds"  (Bool (Set   ($#k3_wsierp_1 :::"Product"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set (Var "X")) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))))))
 proof 


end; scheme  :: NAT_4:sch 2 scheme2{ P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "m")) "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"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "p9"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "p9"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "m")) ")" ) ")" ) where p9 "is"   ($#v1_int_2 :::"prime"::: )     ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool P1[(Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "p9"))])  "}"  ) & (Bool (Bool  "not" (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "m")) ")" ))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set  "("  ($#k3_wsierp_1 :::"Product"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set (Var "X")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))))
 proof 


end; scheme  :: NAT_4:sch 3 scheme3{ P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "m")) "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"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "p9"))  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "p9"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "m")) ")" ) ")" ) where p9 "is"   ($#v1_int_2 :::"prime"::: )     ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool P1[(Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "p9"))])  "}"  ) & (Bool (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "m")) ")" ))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set  "("  ($#k3_wsierp_1 :::"Product"::: )  (Set  "("  ($#k14_finseq_1 :::"Sgm"::: )  (Set (Var "X")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k11_nat_3 :::"|-count"::: )  (Set (Var "m"))))))))
 proof 


end; scheme  :: NAT_4:sch 4 scheme4{ F1(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set F1 "(" (Set (Var "p")) "," (Set (Var "m")) ")" ) where p "is"   ($#v1_int_2 :::"prime"::: )     ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool P1[(Set (Var "p")) "," (Set (Var "m"))])  ")" )  "}"  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )))))
 proof 


end; begin  
theorem :: NAT_4:56 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n"))))  ")" ))) ;