:: EC_PF_1 semantic presentation begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); mode :::"Subfield"::: "of" "K" -> ($#l6_algstr_0 :::"Field":::) means :: EC_PF_1:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "K") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "K") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "K")) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "K")) ")" ); end; :: deftheorem defines :::"Subfield"::: EC_PF_1:def 1 : (Bool "for" (Set (Var "K")) "," (Set (Var "b2")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) ")" )); theorem :: EC_PF_1:1 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set (Var "K")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K")))) ; theorem :: EC_PF_1:2 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "ST")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ST"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "ST"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ST"))))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "ST"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ST"))))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "ST"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "ST"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set (Var "ST")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) & (Bool (Set (Var "ST")) "is" ($#v5_group_1 :::"commutative"::: ) ) & (Bool (Set (Var "ST")) "is" ($#v33_algstr_0 :::"almost_left_invertible"::: ) ) & (Bool (Bool "not" (Set (Var "ST")) "is" ($#v6_struct_0 :::"degenerated"::: ) ))) "holds" (Bool (Set (Var "ST")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K"))))) ; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_int_3 :::"Euclidian"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#m1_ec_pf_1 :::"Subfield"::: ) "of" "K"; end; theorem :: EC_PF_1:3 (Bool "for" (Set (Var "K1")) "," (Set (Var "K2")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "K1")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K2")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "K1")))) "holds" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "K2"))))) ; theorem :: EC_PF_1:4 (Bool "for" (Set (Var "K1")) "," (Set (Var "K2")) "being" ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "K1")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K2"))) & (Bool (Set (Var "K2")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K1")))) "holds" (Bool (Set (Var "K1")) ($#r1_hidden :::"="::: ) (Set (Var "K2")))) ; theorem :: EC_PF_1:5 (Bool "for" (Set (Var "K1")) "," (Set (Var "K2")) "," (Set (Var "K3")) "being" ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "K1")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K2"))) & (Bool (Set (Var "K2")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K3")))) "holds" (Bool (Set (Var "K1")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K3")))) ; theorem :: EC_PF_1:6 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "SK1")) "," (Set (Var "SK2")) "being" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "SK1")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "SK2"))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SK1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SK2")))) ")" ))) ; theorem :: EC_PF_1:7 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "SK1")) "," (Set (Var "SK2")) "being" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "SK1")) "is" ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "SK2"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "SK1")))) "holds" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "SK2")))) ")" ))) ; theorem :: EC_PF_1:8 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "SK1")) "," (Set (Var "SK2")) "being" ($#v36_algstr_0 :::"strict"::: ) ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "SK1")) ($#r1_hidden :::"="::: ) (Set (Var "SK2"))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SK1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SK2")))) ")" ))) ; theorem :: EC_PF_1:9 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "SK1")) "," (Set (Var "SK2")) "being" ($#v36_algstr_0 :::"strict"::: ) ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "SK1")) ($#r1_hidden :::"="::: ) (Set (Var "SK2"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "SK1"))) "iff" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "SK2"))) ")" )) ")" ))) ; registrationlet "K" be ($#v8_struct_0 :::"finite"::: ) ($#l6_algstr_0 :::"Field":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_int_3 :::"Euclidian"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#m1_ec_pf_1 :::"Subfield"::: ) "of" "K"; end; definitionlet "K" be ($#v8_struct_0 :::"finite"::: ) ($#l6_algstr_0 :::"Field":::); :: original: :::"card"::: redefine func :::"card"::: "K" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_int_3 :::"Euclidian"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: EC_PF_1:10 (Bool "for" (Set (Var "K")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "SK1")) "being" ($#v36_algstr_0 :::"strict"::: ) ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_ec_pf_1 :::"card"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "SK1"))))) "holds" (Bool (Set (Var "SK1")) ($#r1_hidden :::"="::: ) (Set (Var "K"))))) ; definitionlet "IT" be ($#l6_algstr_0 :::"Field":::); attr "IT" is :::"prime"::: means :: EC_PF_1:def 2 (Bool "for" (Set (Var "K1")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "K1")) "is" ($#v36_algstr_0 :::"strict"::: ) ($#m1_ec_pf_1 :::"Subfield"::: ) "of" "IT")) "holds" (Bool (Set (Var "K1")) ($#r1_hidden :::"="::: ) "IT")); end; :: deftheorem defines :::"prime"::: EC_PF_1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_ec_pf_1 :::"prime"::: ) ) "iff" (Bool "for" (Set (Var "K1")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "K1")) "is" ($#v36_algstr_0 :::"strict"::: ) ($#m1_ec_pf_1 :::"Subfield"::: ) "of" (Set (Var "IT")))) "holds" (Bool (Set (Var "K1")) ($#r1_hidden :::"="::: ) (Set (Var "IT")))) ")" )); notationlet "p" be ($#m1_hidden :::"Prime":::); synonym :::"GF"::: "p" for :::"INT.Ring"::: "p"; end; registrationlet "p" be ($#m1_hidden :::"Prime":::); cluster (Set ($#k9_int_3 :::"GF"::: ) "p") -> ($#v8_struct_0 :::"finite"::: ) ; end; registrationlet "p" be ($#m1_hidden :::"Prime":::); cluster (Set ($#k9_int_3 :::"GF"::: ) "p") -> ($#v1_ec_pf_1 :::"prime"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_int_3 :::"Euclidian"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_ec_pf_1 :::"prime"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; begin theorem :: EC_PF_1:11 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))) ; theorem :: EC_PF_1:12 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Num 1) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))) ; theorem :: EC_PF_1:13 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "ex" (Set (Var "n1")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k4_nat_d :::"mod"::: ) (Set (Var "p"))))))) ; theorem :: EC_PF_1:14 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))) ; theorem :: EC_PF_1:15 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))))) ; theorem :: EC_PF_1:16 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))))) ; theorem :: EC_PF_1:17 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))))) ; theorem :: EC_PF_1:18 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))))) ; theorem :: EC_PF_1:19 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "a")) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_int_1 :::"mod"::: ) (Set (Var "p"))))))) ; theorem :: EC_PF_1:20 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "iff" (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: EC_PF_1:21 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))) ; theorem :: EC_PF_1:22 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")))))) ; theorem :: EC_PF_1:23 (Bool "for" (Set (Var "n1")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k4_nat_d :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n1")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "p"))))))) ; theorem :: EC_PF_1:24 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))))) ; theorem :: EC_PF_1:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: EC_PF_1:26 (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k8_group_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k8_group_1 :::"*"::: ) (Set (Var "y")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "y")))) ")" ) ")" ))) ; theorem :: EC_PF_1:27 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))))) ; theorem :: EC_PF_1:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" ) ($#k11_algstr_0 :::"""::: ) ))))) ; registrationlet "p" be ($#m1_hidden :::"Prime":::); cluster (Set ($#k1_uniroots :::"MultGroup"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) -> ($#v1_gr_cy_1 :::"cyclic"::: ) ; end; theorem :: EC_PF_1:29 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_uniroots :::"MultGroup"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "x")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k2_binom :::"|^"::: ) (Set (Var "n")))))))) ; theorem :: EC_PF_1:30 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_binom :::"|^"::: ) (Set (Var "n")))))))) ; begin definitionlet "p" be ($#m1_hidden :::"Prime":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ); attr "a" is :::"quadratic_residue"::: means :: EC_PF_1:def 3 (Bool "(" (Bool "a" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) "st" (Bool (Set (Set (Var "x")) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) "a")) ")" ); attr "a" is :::"not_quadratic_residue"::: means :: EC_PF_1:def 4 (Bool "(" (Bool "a" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) "holds" (Bool (Bool "not" (Set (Set (Var "x")) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) "a")) ")" ) ")" ); end; :: deftheorem defines :::"quadratic_residue"::: EC_PF_1:def 3 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v2_ec_pf_1 :::"quadratic_residue"::: ) ) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Set (Set (Var "x")) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" ) ")" ))); :: deftheorem defines :::"not_quadratic_residue"::: EC_PF_1:def 4 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v3_ec_pf_1 :::"not_quadratic_residue"::: ) ) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Bool "not" (Set (Set (Var "x")) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" ) ")" ) ")" ))); theorem :: EC_PF_1:31 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Num 2)) "is" ($#v2_ec_pf_1 :::"quadratic_residue"::: ) ))) ; registrationlet "p" be ($#m1_hidden :::"Prime":::); cluster (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) -> ($#v2_ec_pf_1 :::"quadratic_residue"::: ) ; end; definitionlet "p" be ($#m1_hidden :::"Prime":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ); func :::"Lege_p"::: "a" -> ($#m1_hidden :::"Integer":::) equals :: EC_PF_1:def 5 (Set ($#k6_numbers :::"0"::: ) ) if (Bool "a" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) (Num 1) if (Bool "a" "is" ($#v2_ec_pf_1 :::"quadratic_residue"::: ) ) otherwise (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1)); end; :: deftheorem defines :::"Lege_p"::: EC_PF_1:def 5 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) "is" ($#v2_ec_pf_1 :::"quadratic_residue"::: ) )) "implies" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Bool "not" (Set (Var "a")) "is" ($#v2_ec_pf_1 :::"quadratic_residue"::: ) ))) "implies" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1))) ")" ")" ))); theorem :: EC_PF_1:32 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v3_ec_pf_1 :::"not_quadratic_residue"::: ) ) "iff" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1))) ")" ))) ; theorem :: EC_PF_1:33 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v2_ec_pf_1 :::"quadratic_residue"::: ) ) "iff" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))) ; theorem :: EC_PF_1:34 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: EC_PF_1:35 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: EC_PF_1:36 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "b")) ")" ))))) ; theorem :: EC_PF_1:37 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "n")) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))))) ; theorem :: EC_PF_1:38 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Set (Var "n")) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "a"))))))) ; theorem :: EC_PF_1:39 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "b")) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) : (Bool (Set (Set (Var "b")) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Var "a"))) "}" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set (Var "a")) ")" ))))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); func :::"ProjCo"::: "K" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_zfmisc_1 :::":]"::: ) ) equals :: EC_PF_1:def 6 (Set (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_zfmisc_1 :::":]"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" ) ($#k4_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"ProjCo"::: EC_PF_1:def 6 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) ($#k3_zfmisc_1 :::":]"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ($#k4_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )))); theorem :: EC_PF_1:40 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )))) ; definitionlet "p" be ($#m1_hidden :::"Prime":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ); func :::"Disc"::: "(" "a" "," "b" "," "p" ")" -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) means :: EC_PF_1:def 7 (Bool "for" (Set (Var "g4")) "," (Set (Var "g27")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) "st" (Bool (Bool (Set (Var "g4")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k4_nat_d :::"mod"::: ) "p")) & (Bool (Set (Var "g27")) ($#r1_hidden :::"="::: ) (Set (Num 27) ($#k4_nat_d :::"mod"::: ) "p"))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set "(" "a" ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g27")) ($#k8_group_1 :::"*"::: ) (Set "(" "b" ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" )))); end; :: deftheorem defines :::"Disc"::: EC_PF_1:def 7 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "g4")) "," (Set (Var "g27")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "g4")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k4_nat_d :::"mod"::: ) (Set (Var "p")))) & (Bool (Set (Var "g27")) ($#r1_hidden :::"="::: ) (Set (Num 27) ($#k4_nat_d :::"mod"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g4")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "g27")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" )))) ")" ))); definitionlet "p" be ($#m1_hidden :::"Prime":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ); func :::"EC_WEqProjCo"::: "(" "a" "," "b" "," "p" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) means :: EC_PF_1:def 8 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" "a" ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" "b" ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ")" )))); end; :: deftheorem defines :::"EC_WEqProjCo"::: EC_PF_1:def 8 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_ec_pf_1 :::"EC_WEqProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ")" )))) ")" )))); theorem :: EC_PF_1:41 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set (Set "(" ($#k5_ec_pf_1 :::"EC_WEqProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ($#k4_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Y")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "Z")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "X")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Z")) ($#k2_binom :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Z")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ))))) ; definitionlet "p" be ($#m1_hidden :::"Prime":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ); func :::"EC_SetProjCo"::: "(" "a" "," "b" "," "p" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) ")" ) equals :: EC_PF_1:def 9 "{" (Set (Var "P")) where P "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) : (Bool (Set (Set "(" ($#k5_ec_pf_1 :::"EC_WEqProjCo"::: ) "(" "a" "," "b" "," "p" ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ))) "}" ; end; :: deftheorem defines :::"EC_SetProjCo"::: EC_PF_1:def 9 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "P")) where P "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) : (Bool (Set (Set "(" ($#k5_ec_pf_1 :::"EC_WEqProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) "}" ))); theorem :: EC_PF_1:42 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )))) ; theorem :: EC_PF_1:43 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "Y")) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "X")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "X")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")))) "iff" (Bool (Set ($#k4_domain_1 :::"["::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) ")" ))) ; definitionlet "p" be ($#m1_hidden :::"Prime":::); let "P", "Q" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" )); pred "P" :::"_EQ_"::: "Q" means :: EC_PF_1:def 10 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ))) & (Bool (Set "P" ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" "Q" ($#k1_mcart_1 :::"`1_3"::: ) ")" ))) & (Bool (Set "P" ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" "Q" ($#k2_mcart_1 :::"`2_3"::: ) ")" ))) & (Bool (Set "P" ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" "Q" ($#k3_mcart_1 :::"`3_3"::: ) ")" ))) ")" )); reflexivity (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" )) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ))) & (Bool (Set (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ))) & (Bool (Set (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ))) & (Bool (Set (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ))) ")" ))) ; symmetry (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" )) "st" (Bool (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ))) & (Bool (Set (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ))) & (Bool (Set (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ))) & (Bool (Set (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ))) ")" ))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ))) & (Bool (Set (Set (Var "Q")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ))) & (Bool (Set (Set (Var "Q")) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ))) & (Bool (Set (Set (Var "Q")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ))) ")" ))) ; end; :: deftheorem defines :::"_EQ_"::: EC_PF_1:def 10 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ))) & (Bool (Set (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ))) & (Bool (Set (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ))) ")" )) ")" ))); theorem :: EC_PF_1:44 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "st" (Bool (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) & (Bool (Set (Var "Q")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "R"))))) ; theorem :: EC_PF_1:45 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) ($#k3_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "Q")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ))) & (Bool (Set (Set (Var "Q")) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ))) & (Bool (Set (Set (Var "Q")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ")" )))) "holds" (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )))))) ; definitionlet "p" be ($#m1_hidden :::"Prime":::); func :::"R_ProjCo"::: "p" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" ) ")" ) equals :: EC_PF_1:def 11 "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) ) where P, Q "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) "p" ")" )) : (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) "}" ; end; :: deftheorem defines :::"R_ProjCo"::: EC_PF_1:def 11 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) "holds" (Bool (Set ($#k7_ec_pf_1 :::"R_ProjCo"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) ) where P, Q "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) : (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) "}" )); theorem :: EC_PF_1:46 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) "iff" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_ec_pf_1 :::"R_ProjCo"::: ) (Set (Var "p")))) ")" ))) ; registrationlet "p" be ($#m1_hidden :::"Prime":::); cluster (Set ($#k7_ec_pf_1 :::"R_ProjCo"::: ) "p") -> ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ; end; definitionlet "p" be ($#m1_hidden :::"Prime":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Const "p")) ")" ); func :::"R_EllCur"::: "(" "a" "," "b" "," "p" ")" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" "a" "," "b" "," "p" ")" ")" ) equals :: EC_PF_1:def 12 (Set (Set "(" ($#k7_ec_pf_1 :::"R_ProjCo"::: ) "p" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" "a" "," "b" "," "p" ")" ")" ) ")" )); end; :: deftheorem defines :::"R_EllCur"::: EC_PF_1:def 12 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_ec_pf_1 :::"R_ProjCo"::: ) (Set (Var "p")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set "(" ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) ")" ))))); theorem :: EC_PF_1:47 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "st" (Bool (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "Q"))) "iff" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) ")" )))) ; theorem :: EC_PF_1:48 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool (Set (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool (Set (Var "Q")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "Q")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))))) ; theorem :: EC_PF_1:49 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool (Set (Set (Var "P")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool (Set (Var "Q")) ($#r1_ec_pf_1 :::"_EQ_"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "Q")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "Q")) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "Q")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: EC_PF_1:50 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ))) & (Bool "(" "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) "holds" (Bool "(" "not" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) "or" "not" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "P")) ")" )) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))(Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "P")) ")" )) ")" )))))) ; theorem :: EC_PF_1:51 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) ")" ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "P")) ")" ")" ) where P "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) : (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ))) ")" ) "}" )))) ; theorem :: EC_PF_1:52 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d1")) "," (Set (Var "Y1")) "," (Set (Var "d2")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set ($#k4_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "Y1")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool (Set ($#k4_domain_1 :::"["::: ) (Set (Var "d2")) "," (Set (Var "Y2")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set ($#k4_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "Y1")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set ($#k4_domain_1 :::"["::: ) (Set (Var "d2")) "," (Set (Var "Y2")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" )) "iff" (Bool "(" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2"))) & (Bool (Set (Var "Y1")) ($#r1_hidden :::"="::: ) (Set (Var "Y2"))) ")" ) ")" ))) ; theorem :: EC_PF_1:53 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) ")" ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Var "F2")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "P")) ")" ")" ) where P "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) : (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ))) ")" ) "}" )) "holds" (Bool (Set (Var "F1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "F2")))))) ; theorem :: EC_PF_1:54 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))))) ; theorem :: EC_PF_1:55 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v1_prob_2 :::"disjoint_valued"::: ) )))) ; theorem :: EC_PF_1:56 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))))) ; theorem :: EC_PF_1:57 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "L")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "S")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "L")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "L")))))))) ; theorem :: EC_PF_1:58 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) : (Bool (Set (Set (Var "Y")) ($#k2_binom :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "d")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")))) "}" ) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set ($#k4_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "Y")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ")" ) where Y "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) : (Bool (Set ($#k4_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "Y")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) "}" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "F")) "," (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ))))) ; theorem :: EC_PF_1:59 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set ($#k4_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "Y")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ")" ) where Y "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) : (Bool (Set ($#k4_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "Y")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) "}" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" ))))) ; theorem :: EC_PF_1:60 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" ))) ")" )) ")" ) & (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "P")) ")" ")" ) where P "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_ec_pf_1 :::"ProjCo"::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )) : (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k6_ec_pf_1 :::"EC_SetProjCo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" )) & (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ))) ")" ) "}" ) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "F")))) ")" )))) ; theorem :: EC_PF_1:61 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Prime":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 3)) & (Bool (Set ($#k4_ec_pf_1 :::"Disc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_int_3 :::"GF"::: ) (Set (Var "p")) ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k2_ec_pf_1 :::"Lege_p"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k2_binom :::"|^"::: ) (Num 3) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ))) ")" )) ")" ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k8_ec_pf_1 :::"R_EllCur"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "p")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k1_gr_cy_1 :::"Sum"::: ) (Set (Var "F")) ")" ))) ")" )))) ;