:: NAT_3 semantic presentation begin registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "a" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); let "b" be ($#m1_hidden :::"Nat":::); cluster (Set "a" ($#k1_newton :::"|^"::: ) "b") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registration cluster ($#v7_ordinal1 :::"natural"::: ) ($#v1_int_2 :::"prime"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: NAT_3:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_nat_d :::"divides"::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_nat_d :::"divides"::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b"))) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "c")) ($#k24_binop_2 :::"*"::: ) (Set (Var "d"))))) ; theorem :: NAT_3:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "b"))))) ; theorem :: NAT_3:3 (Bool "for" (Set (Var "a")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "n")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Set (Var "a"))))) ; theorem :: NAT_3:4 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "m")) ($#k1_newton :::"|^"::: ) (Set (Var "j"))) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "m")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "i")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) ; theorem :: NAT_3:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "p")) ($#r1_nat_d :::"divides"::: ) (Set (Var "a"))))) ; theorem :: NAT_3:6 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "being" ($#m1_hidden :::"Prime":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: NAT_3:7 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "a")) ($#r1_nat_d :::"divides"::: ) (Set ($#k3_wsierp_1 :::"Product"::: ) (Set (Var "f")))))) ; theorem :: NAT_3:8 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "f")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_nat_d :::"divides"::: ) (Set ($#k3_wsierp_1 :::"Product"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")))))) ; definitionlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "a" be ($#m1_hidden :::"Nat":::); func "f" :::"|^"::: "a" -> ($#m1_hidden :::"FinSequence":::) means :: NAT_3: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_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_newton :::"|^"::: ) "a")) ")" ) ")" ); end; :: deftheorem defines :::"|^"::: NAT_3:def 1 : (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_nat_3 :::"|^"::: ) (Set (Var "a")))) "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_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "a")))) ")" ) ")" ) ")" )))); registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "a" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k1_nat_3 :::"|^"::: ) "a") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "a" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k1_nat_3 :::"|^"::: ) "a") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "a" be ($#m1_hidden :::"Nat":::); :: original: :::"|^"::: redefine func "f" :::"|^"::: "a" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "f" be ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "a" be ($#m1_hidden :::"Nat":::); :: original: :::"|^"::: redefine func "f" :::"|^"::: "a" -> ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: NAT_3:9 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k2_nat_3 :::"|^"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Num 1)))) ; theorem :: NAT_3:10 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k2_nat_3 :::"|^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: NAT_3:11 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k2_pre_poly :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) ($#k2_nat_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_poly :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: NAT_3:12 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "r")) ($#k3_pre_poly :::"*>"::: ) ) ($#k2_nat_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set "(" (Set (Var "r")) ($#k2_newton :::"|^"::: ) (Set (Var "a")) ")" ) ($#k3_pre_poly :::"*>"::: ) )))) ; theorem :: NAT_3:13 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "r")) ($#k3_pre_poly :::"*>"::: ) ) ")" ) ($#k2_nat_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_nat_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "r")) ($#k3_pre_poly :::"*>"::: ) ) ($#k2_nat_3 :::"|^"::: ) (Set (Var "a")) ")" )))))) ; theorem :: NAT_3:14 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "f")) ($#k2_nat_3 :::"|^"::: ) (Set "(" (Set (Var "b")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "f")) ($#k2_nat_3 :::"|^"::: ) (Set (Var "b")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "f")) ")" ))))) ; theorem :: NAT_3:15 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "f")) ($#k2_nat_3 :::"|^"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "f")) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "a")))))) ; begin registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1("X") ($#v4_valued_0 :::"natural-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "a" be ($#m1_hidden :::"Nat":::); func "a" :::"*"::: "b" -> ($#m1_hidden :::"ManySortedSet":::) "of" "X" means :: NAT_3:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k11_binop_2 :::"*"::: ) (Set "(" "b" ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"*"::: NAT_3:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_nat_3 :::"*"::: ) (Set (Var "b")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "a" be ($#m1_hidden :::"Nat":::); cluster (Set "a" ($#k4_nat_3 :::"*"::: ) "b") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "a" be ($#m1_hidden :::"Nat":::); cluster (Set "a" ($#k4_nat_3 :::"*"::: ) "b") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); cluster (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_nat_3 :::"*"::: ) "b" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: NAT_3:16 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set (Var "a")) ($#k4_nat_3 :::"*"::: ) (Set (Var "b")) ")" )))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "a" be ($#m1_hidden :::"Nat":::); cluster (Set "a" ($#k4_nat_3 :::"*"::: ) "b") -> ($#v2_pre_poly :::"finite-support"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); func :::"min"::: "(" "b1" "," "b2" ")" -> ($#m1_hidden :::"ManySortedSet":::) "of" "X" means :: NAT_3:def 3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set "b1" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set "b2" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "b1" ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" & "(" (Bool (Bool (Set "b1" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set "b2" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "b2" ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ")" )); end; :: deftheorem defines :::"min"::: NAT_3:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_nat_3 :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" & "(" (Bool (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ")" )) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); cluster (Set ($#k5_nat_3 :::"min"::: ) "(" "b1" "," "b2" ")" ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); cluster (Set ($#k5_nat_3 :::"min"::: ) "(" "b1" "," "b2" ")" ) -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; theorem :: NAT_3:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k5_nat_3 :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b2")) ")" ))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v3_valued_0 :::"real-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); cluster (Set ($#k5_nat_3 :::"min"::: ) "(" "b1" "," "b2" ")" ) -> ($#v2_pre_poly :::"finite-support"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); func :::"max"::: "(" "b1" "," "b2" ")" -> ($#m1_hidden :::"ManySortedSet":::) "of" "X" means :: NAT_3:def 4 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set "b1" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set "b2" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "b2" ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" & "(" (Bool (Bool (Set "b1" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set "b2" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "b1" ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ")" )); end; :: deftheorem defines :::"max"::: NAT_3:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_3 :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" & "(" (Bool (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ")" )) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); cluster (Set ($#k6_nat_3 :::"max"::: ) "(" "b1" "," "b2" ")" ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); cluster (Set ($#k6_nat_3 :::"max"::: ) "(" "b1" "," "b2" ")" ) -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; theorem :: NAT_3:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k6_nat_3 :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b2")) ")" ))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v3_valued_0 :::"real-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); cluster (Set ($#k6_nat_3 :::"max"::: ) "(" "b1" "," "b2" ")" ) -> ($#v2_pre_poly :::"finite-support"::: ) ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "A" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1("A") ($#v1_valued_0 :::"complex-yielding"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#v1_valued_0 :::"complex-yielding"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "A")); func :::"Product"::: "b" -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) means :: NAT_3:def 5 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k20_rvsum_1 :::"Product"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "b" ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) "b" ")" ) ")" ))) ")" )); end; :: deftheorem defines :::"Product"::: NAT_3:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_valued_0 :::"complex-yielding"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_3 :::"Product"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k20_rvsum_1 :::"Product"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b")) ")" ) ")" ))) ")" )) ")" )))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "A")); :: original: :::"Product"::: redefine func :::"Product"::: "b" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: NAT_3:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "a"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "b"))))) "holds" (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set "(" (Set (Var "a")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_nat_3 :::"Product"::: ) (Set (Var "a")) ")" ) ($#k24_binop_2 :::"*"::: ) (Set "(" ($#k8_nat_3 :::"Product"::: ) (Set (Var "b")) ")" ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); func "b" :::"|^"::: "n" -> ($#m1_hidden :::"ManySortedSet":::) "of" "X" means :: NAT_3:def 6 (Bool "(" (Bool (Set ($#k13_pre_poly :::"support"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k13_pre_poly :::"support"::: ) "b")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "b" ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_newton :::"|^"::: ) "n")) ")" ) ")" ); end; :: deftheorem defines :::"|^"::: NAT_3:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k9_nat_3 :::"|^"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")))) ")" ) ")" ) ")" ))))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set "b" ($#k9_nat_3 :::"|^"::: ) "n") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set "b" ($#k9_nat_3 :::"|^"::: ) "n") -> ($#v2_pre_poly :::"finite-support"::: ) ; end; theorem :: NAT_3:20 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; begin definitionlet "n", "d" be ($#m1_hidden :::"Nat":::); assume that (Bool (Set (Const "d")) ($#r1_hidden :::"<>"::: ) (Num 1)) and (Bool (Set (Const "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ; func "d" :::"|-count"::: "n" -> ($#m1_hidden :::"Nat":::) means :: NAT_3:def 7 (Bool "(" (Bool (Set "d" ($#k1_newton :::"|^"::: ) it) ($#r1_nat_d :::"divides"::: ) "n") & (Bool (Bool "not" (Set "d" ($#k1_newton :::"|^"::: ) (Set "(" it ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_nat_d :::"divides"::: ) "n")) ")" ); end; :: deftheorem defines :::"|-count"::: NAT_3:def 7 : (Bool "for" (Set (Var "n")) "," (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k10_nat_3 :::"|-count"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set (Set (Var "d")) ($#k1_newton :::"|^"::: ) (Set (Var "b3"))) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) & (Bool (Bool "not" (Set (Set (Var "d")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "b3")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) ")" ) ")" ))); definitionlet "n", "d" be ($#m1_hidden :::"Nat":::); :: original: :::"|-count"::: redefine func "d" :::"|-count"::: "n" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: NAT_3:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "n")) ($#k11_nat_3 :::"|-count"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: NAT_3:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "n")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: NAT_3:23 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "a")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: NAT_3:24 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "p")))) "holds" (Bool (Set (Set (Var "a")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: NAT_3:25 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "b")) ($#k11_nat_3 :::"|-count"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: NAT_3:26 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "b")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "a")) ")" )))) "holds" (Bool (Set (Var "b")) ($#r1_nat_d :::"divides"::: ) (Set (Var "a")))) ; theorem :: NAT_3:27 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "b")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "iff" (Bool (Bool "not" (Set (Var "b")) ($#r1_nat_d :::"divides"::: ) (Set (Var "a")))) ")" )) ; theorem :: NAT_3:28 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set "(" (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "a")) ")" ) ($#k23_binop_2 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "b")) ")" ))))) ; theorem :: NAT_3:29 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set "(" (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "a")) ")" ) ")" ) ($#k24_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "b")) ")" ) ")" ))))) ; theorem :: NAT_3:30 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_nat_d :::"divides"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "a")))))) ; theorem :: NAT_3:31 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_nat_d :::"divides"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set "(" (Set (Var "a")) ($#k3_nat_d :::"div"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "a")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "b")) ")" ))))) ; theorem :: NAT_3:32 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k24_binop_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "a")) ")" )))))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"prime_exponents"::: "n" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) means :: NAT_3:def 8 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) "n"))); end; :: deftheorem defines :::"prime_exponents"::: NAT_3:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_nat_3 :::"prime_exponents"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "n"))))) ")" ))); notationlet "n" be ($#m1_hidden :::"Nat":::); synonym :::"pfexp"::: "n" for :::"prime_exponents"::: "n"; end; theorem :: NAT_3:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Prime":::)))) ; theorem :: NAT_3:34 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Prime":::)))) ; theorem :: NAT_3:35 (Bool "for" (Set (Var "a")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k12_nat_3 :::"prime_exponents"::: ) "n") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; theorem :: NAT_3:36 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "b")) ")" )))) "holds" (Bool (Set (Var "a")) ($#r1_nat_d :::"divides"::: ) (Set (Var "b")))) ; theorem :: NAT_3:37 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "b")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "a")) "is" ($#m1_hidden :::"Prime":::)) & (Bool (Set (Var "a")) ($#r1_nat_d :::"divides"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "b")) ")" )))) ; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k12_nat_3 :::"prime_exponents"::: ) "n") -> ($#v2_pre_poly :::"finite-support"::: ) ; end; theorem :: NAT_3:38 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_nat_d :::"divides"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "a")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: NAT_3:39 (Bool (Set ($#k12_nat_3 :::"pfexp"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set ($#k10_newton :::"SetPrimes"::: ) ))) ; registration cluster (Set ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Num 1) ")" )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: NAT_3:40 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: NAT_3:41 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "p")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: NAT_3:42 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "a")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: NAT_3:43 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) ))) ; registrationlet "p" be ($#m1_hidden :::"Prime":::); let "a" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set "(" "p" ($#k1_newton :::"|^"::: ) "a" ")" ) ")" )) -> (Num 1) ($#v3_card_1 :::"-element"::: ) ; end; registrationlet "p" be ($#m1_hidden :::"Prime":::); cluster (Set ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) "p" ")" )) -> (Num 1) ($#v3_card_1 :::"-element"::: ) ; end; theorem :: NAT_3:44 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "a")) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "b")) ")" )))) ; theorem :: NAT_3:45 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "a")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ")" )))) ; theorem :: NAT_3:46 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "a")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "b")) ")" ) ")" )))) ; theorem :: NAT_3:47 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k23_binop_2 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "b")) ")" ) ")" ) ")" )))) ; theorem :: NAT_3:48 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "b")) ")" ) ")" )))) ; theorem :: NAT_3:49 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "n")) ($#k24_binop_2 :::"*"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "m")) ")" )))) ; theorem :: NAT_3:50 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "n")) ($#k3_nat_d :::"div"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" ) ($#k12_pre_poly :::"-'"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "m")) ")" )))) ; theorem :: NAT_3:51 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_nat_3 :::"*"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" ))))) ; theorem :: NAT_3:52 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: NAT_3:53 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "n")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_nat_3 :::"min"::: ) "(" (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "m")) ")" ) ")" ))) ; theorem :: NAT_3:54 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_nat_3 :::"pfexp"::: ) (Set "(" (Set (Var "n")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_3 :::"max"::: ) "(" (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "m")) ")" ) ")" ))) ; begin definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); func :::"prime_factorization"::: "n" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) means :: NAT_3:def 9 (Bool "(" (Bool (Set ($#k13_pre_poly :::"support"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) "n" ")" ))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) "n" ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) "n" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"prime_factorization"::: NAT_3:def 9 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k10_newton :::"SetPrimes"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_nat_3 :::"prime_factorization"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" ))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k12_nat_3 :::"pfexp"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" ))); notationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); synonym :::"ppf"::: "n" for :::"prime_factorization"::: "n"; end; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k13_nat_3 :::"prime_factorization"::: ) "n") -> ($#v4_valued_0 :::"natural-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) ; end; theorem :: NAT_3:55 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: NAT_3:56 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k11_nat_3 :::"|-count"::: ) (Set (Var "n")) ")" ))))) ; theorem :: NAT_3:57 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: NAT_3:58 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set ($#k13_nat_3 :::"ppf"::: ) (Set "(" (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "a")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "b")) ")" )))) ; theorem :: NAT_3:59 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")))))) ; theorem :: NAT_3:60 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k13_nat_3 :::"ppf"::: ) (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "n")) ")" ) ($#k9_nat_3 :::"|^"::: ) (Set (Var "m"))))) ; theorem :: NAT_3:61 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k8_nat_3 :::"Product"::: ) (Set "(" ($#k13_nat_3 :::"ppf"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ;