:: Set of Points on Elliptic Curve in Projective Coordinates :: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama :: :: Received December 21, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin definition let K be Field; mode Subfield of K -> Field means :Def1: :: EC_PF_1:def 1 ( the carrier of it c= the carrier of K & the addF of it = the addF of K || the carrier of it & the multF of it = the multF of K || the carrier of it & 1. it = 1. K & 0. it = 0. K ); existence ex b1 being Field st ( the carrier of b1 c= the carrier of K & the addF of b1 = the addF of K || the carrier of b1 & the multF of b1 = the multF of K || the carrier of b1 & 1. b1 = 1. K & 0. b1 = 0. K ) proofend; end; :: deftheorem Def1 defines Subfield EC_PF_1:def_1_:_ for K, b2 being Field holds ( b2 is Subfield of K iff ( the carrier of b2 c= the carrier of K & the addF of b2 = the addF of K || the carrier of b2 & the multF of b2 = the multF of K || the carrier of b2 & 1. b2 = 1. K & 0. b2 = 0. K ) ); theorem Th1: :: EC_PF_1:1 for K being Field holds K is Subfield of K proofend; theorem Th2: :: EC_PF_1:2 for K being Field for ST being non empty doubleLoopStr st the carrier of ST is Subset of the carrier of K & the addF of ST = the addF of K || the carrier of ST & the multF of ST = the multF of K || the carrier of ST & 1. ST = 1. K & 0. ST = 0. K & ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated holds ST is Subfield of K proofend; registration let K be Field; cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed for Subfield of K; existence ex b1 being Subfield of K st b1 is strict proofend; end; theorem Th3: :: EC_PF_1:3 for K1, K2 being Field st K1 is Subfield of K2 holds for x being set st x in K1 holds x in K2 proofend; theorem Th4: :: EC_PF_1:4 for K1, K2 being strict Field st K1 is Subfield of K2 & K2 is Subfield of K1 holds K1 = K2 proofend; theorem :: EC_PF_1:5 for K1, K2, K3 being strict Field st K1 is Subfield of K2 & K2 is Subfield of K3 holds K1 is Subfield of K3 proofend; theorem Th6: :: EC_PF_1:6 for K being Field for SK1, SK2 being Subfield of K holds ( SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2 ) proofend; theorem Th7: :: EC_PF_1:7 for K being Field for SK1, SK2 being Subfield of K holds ( SK1 is Subfield of SK2 iff for x being set st x in SK1 holds x in SK2 ) proofend; theorem Th8: :: EC_PF_1:8 for K being Field for SK1, SK2 being strict Subfield of K holds ( SK1 = SK2 iff the carrier of SK1 = the carrier of SK2 ) proofend; theorem :: EC_PF_1:9 for K being Field for SK1, SK2 being strict Subfield of K holds ( SK1 = SK2 iff for x being set holds ( x in SK1 iff x in SK2 ) ) proofend; registration let K be finite Field; cluster non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed for Subfield of K; existence ex b1 being Subfield of K st b1 is finite proofend; end; definition let K be finite Field; :: original:card redefine func card K -> Element of NAT ; coherence card K is Element of NAT proofend; end; registration cluster non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed for doubleLoopStr ; existence ex b1 being Field st ( b1 is strict & b1 is finite ) proofend; end; theorem :: EC_PF_1:10 for K being finite strict Field for SK1 being strict Subfield of K st card K = card SK1 holds SK1 = K proofend; definition let IT be Field; attrIT is prime means :Def2: :: EC_PF_1:def 2 for K1 being Field st K1 is strict Subfield of IT holds K1 = IT; end; :: deftheorem Def2 defines prime EC_PF_1:def_2_:_ for IT being Field holds ( IT is prime iff for K1 being Field st K1 is strict Subfield of IT holds K1 = IT ); notation let p be Prime; synonym GF p for INT.Ring p; end; registration let p be Prime; cluster GF p -> finite ; coherence GF p is finite ; end; registration let p be Prime; cluster GF p -> prime ; coherence GF p is prime proofend; end; registration cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed prime for doubleLoopStr ; existence ex b1 being Field st b1 is prime proofend; end; begin Lm1: for M being non empty multMagma for a being Element of M for n being Nat holds (power M) . (a,n) is Element of M proofend; theorem Th11: :: EC_PF_1:11 for p being Prime holds 0 = 0. (GF p) proofend; theorem Th12: :: EC_PF_1:12 for p being Prime holds 1 = 1. (GF p) proofend; theorem Th13: :: EC_PF_1:13 for p being Prime for a being Element of (GF p) ex n1 being Nat st a = n1 mod p proofend; theorem Th14: :: EC_PF_1:14 for i being Integer for p being Prime holds i mod p is Element of (GF p) proofend; theorem Th15: :: EC_PF_1:15 for i, j being Integer for p being Prime for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a + b = (i + j) mod p proofend; theorem Th16: :: EC_PF_1:16 for i being Integer for p being Prime for a being Element of (GF p) st a = i mod p holds - a = (p - i) mod p proofend; theorem :: EC_PF_1:17 for i, j being Integer for p being Prime for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a - b = (i - j) mod p proofend; theorem Th18: :: EC_PF_1:18 for i, j being Integer for p being Prime for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a * b = (i * j) mod p proofend; theorem :: EC_PF_1:19 for i, j being Integer for p being Prime for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds a " = j mod p proofend; theorem Th20: :: EC_PF_1:20 for p being Prime for a, b being Element of (GF p) holds ( ( a = 0 or b = 0 ) iff a * b = 0 ) proofend; theorem Th21: :: EC_PF_1:21 for p being Prime for a being Element of (GF p) holds ( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 ) proofend; Lm2: for p being Prime for a being Element of (GF p) holds (power (GF p)) . (a,1) = a by GROUP_1:50; Lm3: for p being Prime for a being Element of (GF p) holds (power (GF p)) . (a,2) = a * a by GROUP_1:51; theorem :: EC_PF_1:22 for p being Prime for a being Element of (GF p) holds a |^ 2 = a * a by Lm3; theorem Th23: :: EC_PF_1:23 for n1, n being Nat for p being Prime for a being Element of (GF p) st a = n1 mod p holds a |^ n = (n1 |^ n) mod p proofend; theorem Th24: :: EC_PF_1:24 for K being non empty unital associative multMagma for a being Element of K for n being Nat holds a |^ (n + 1) = (a |^ n) * a proofend; theorem Th25: :: EC_PF_1:25 for n being Nat for p being Prime for a being Element of (GF p) st a <> 0 holds a |^ n <> 0 proofend; theorem Th26: :: EC_PF_1:26 for F being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for x, y being Element of F holds ( x * x = y * y iff ( x = y or x = - y ) ) proofend; theorem Th27: :: EC_PF_1:27 for p being Prime for x being Element of (GF p) st 2 < p & x + x = 0. (GF p) holds x = 0. (GF p) proofend; theorem Th28: :: EC_PF_1:28 for n being Nat for p being Prime for a being Element of (GF p) st a <> 0 holds (a ") |^ n = (a |^ n) " proofend; Lm4: for n1, n2 being Nat for p being Prime for a being Element of (GF p) holds (a |^ n1) * (a |^ n2) = a |^ (n1 + n2) by BINOM:10; Lm5: for n1, n2 being Nat for p being Prime for a being Element of (GF p) holds (a |^ n1) |^ n2 = a |^ (n1 * n2) by BINOM:11; registration let p be Prime; cluster MultGroup (GF p) -> cyclic ; coherence MultGroup (GF p) is cyclic proofend; end; theorem Th29: :: EC_PF_1:29 for p being Prime for x being Element of (MultGroup (GF p)) for x1 being Element of (GF p) for n being Nat st x = x1 holds x |^ n = x1 |^ n proofend; theorem Th30: :: EC_PF_1:30 for p being Prime ex g being Element of (GF p) st for a being Element of (GF p) st a <> 0. (GF p) holds ex n being Nat st a = g |^ n proofend; begin definition let p be Prime; let a be Element of (GF p); attra is quadratic_residue means :Def3: :: EC_PF_1:def 3 ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ); attra is not_quadratic_residue means :Def4: :: EC_PF_1:def 4 ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ); end; :: deftheorem Def3 defines quadratic_residue EC_PF_1:def_3_:_ for p being Prime for a being Element of (GF p) holds ( a is quadratic_residue iff ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) ); :: deftheorem Def4 defines not_quadratic_residue EC_PF_1:def_4_:_ for p being Prime for a being Element of (GF p) holds ( a is not_quadratic_residue iff ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) ); theorem Th31: :: EC_PF_1:31 for p being Prime for a being Element of (GF p) st a <> 0 holds a |^ 2 is quadratic_residue proofend; registration let p be Prime; cluster 1. (GF p) -> quadratic_residue ; correctness coherence 1. (GF p) is quadratic_residue ; proofend; end; definition let p be Prime; let a be Element of (GF p); func Lege_p a -> Integer equals :Def5: :: EC_PF_1:def 5 0 if a = 0 1 if a is quadratic_residue otherwise - 1; coherence ( ( a = 0 implies 0 is Integer ) & ( a is quadratic_residue implies 1 is Integer ) & ( not a = 0 & not a is quadratic_residue implies - 1 is Integer ) ) ; consistency for b1 being Integer st a = 0 & a is quadratic_residue holds ( b1 = 0 iff b1 = 1 ) by Def3; end; :: deftheorem Def5 defines Lege_p EC_PF_1:def_5_:_ for p being Prime for a being Element of (GF p) holds ( ( a = 0 implies Lege_p a = 0 ) & ( a is quadratic_residue implies Lege_p a = 1 ) & ( not a = 0 & not a is quadratic_residue implies Lege_p a = - 1 ) ); theorem Th32: :: EC_PF_1:32 for p being Prime for a being Element of (GF p) holds ( a is not_quadratic_residue iff Lege_p a = - 1 ) proofend; theorem Th33: :: EC_PF_1:33 for p being Prime for a being Element of (GF p) holds ( a is quadratic_residue iff Lege_p a = 1 ) proofend; theorem Th34: :: EC_PF_1:34 for p being Prime for a being Element of (GF p) holds ( a = 0 iff Lege_p a = 0 ) proofend; theorem :: EC_PF_1:35 for p being Prime for a being Element of (GF p) st a <> 0 holds Lege_p (a |^ 2) = 1 proofend; theorem Th36: :: EC_PF_1:36 for p being Prime for a, b being Element of (GF p) holds Lege_p (a * b) = (Lege_p a) * (Lege_p b) proofend; theorem Th37: :: EC_PF_1:37 for n being Nat for p being Prime for a being Element of (GF p) st a <> 0 & n mod 2 = 0 holds Lege_p (a |^ n) = 1 proofend; theorem :: EC_PF_1:38 for n being Nat for p being Prime for a being Element of (GF p) st n mod 2 = 1 holds Lege_p (a |^ n) = Lege_p a proofend; theorem Th39: :: EC_PF_1:39 for p being Prime for a being Element of (GF p) st 2 < p holds card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) proofend; begin definition let K be Field; func ProjCo K -> non empty Subset of [: the carrier of K, the carrier of K, the carrier of K:] equals :: EC_PF_1:def 6 [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]}; correctness coherence [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]} is non empty Subset of [: the carrier of K, the carrier of K, the carrier of K:]; proofend; end; :: deftheorem defines ProjCo EC_PF_1:def_6_:_ for K being Field holds ProjCo K = [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]}; theorem Th40: :: EC_PF_1:40 for p being Prime holds ProjCo (GF p) = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} proofend; definition let p be Prime; let a, b be Element of (GF p); func Disc (a,b,p) -> Element of (GF p) means :: EC_PF_1:def 7 for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds it = (g4 * (a |^ 3)) + (g27 * (b |^ 2)); existence ex b1 being Element of (GF p) st for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds b1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) proofend; uniqueness for b1, b2 being Element of (GF p) st ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds b1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) & ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds b2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) holds b1 = b2 proofend; end; :: deftheorem defines Disc EC_PF_1:def_7_:_ for p being Prime for a, b, b4 being Element of (GF p) holds ( b4 = Disc (a,b,p) iff for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds b4 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ); definition let p be Prime; let a, b be Element of (GF p); func EC_WEqProjCo (a,b,p) -> Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) means :Def8: :: EC_PF_1:def 8 for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds it . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))); existence ex b1 being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) st for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b1 . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) proofend; uniqueness for b1, b2 being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) st ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b1 . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) ) & ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b2 . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines EC_WEqProjCo EC_PF_1:def_8_:_ for p being Prime for a, b being Element of (GF p) for b4 being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) holds ( b4 = EC_WEqProjCo (a,b,p) iff for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b4 . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) ); theorem Th41: :: EC_PF_1:41 for p being Prime for a, b, X, Y, Z being Element of (GF p) holds (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3))) proofend; Lm6: for p being Prime for a, b being Element of (GF p) holds ( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) ) proofend; definition let p be Prime; let a, b be Element of (GF p); func EC_SetProjCo (a,b,p) -> non empty Subset of (ProjCo (GF p)) equals :: EC_PF_1:def 9 { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; correctness coherence { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } is non empty Subset of (ProjCo (GF p)); proofend; end; :: deftheorem defines EC_SetProjCo EC_PF_1:def_9_:_ for p being Prime for a, b being Element of (GF p) holds EC_SetProjCo (a,b,p) = { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; Lm7: for p being Prime for d, Y being Element of (GF p) holds [d,Y,1] is Element of ProjCo (GF p) proofend; theorem Th42: :: EC_PF_1:42 for p being Prime for a, b being Element of (GF p) holds [0,1,0] is Element of EC_SetProjCo (a,b,p) proofend; theorem Th43: :: EC_PF_1:43 for p being Prime for a, b, X, Y being Element of (GF p) holds ( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) ) proofend; definition let p be Prime; let P, Q be Element of ProjCo (GF p); predP _EQ_ Q means :Def10: :: EC_PF_1:def 10 ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ); reflexivity for P being Element of ProjCo (GF p) ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (P `1_3) & P `2_3 = a * (P `2_3) & P `3_3 = a * (P `3_3) ) proofend; symmetry for P, Q being Element of ProjCo (GF p) st ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) holds ex a being Element of (GF p) st ( a <> 0. (GF p) & Q `1_3 = a * (P `1_3) & Q `2_3 = a * (P `2_3) & Q `3_3 = a * (P `3_3) ) proofend; end; :: deftheorem Def10 defines _EQ_ EC_PF_1:def_10_:_ for p being Prime for P, Q being Element of ProjCo (GF p) holds ( P _EQ_ Q iff ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) ); theorem Th44: :: EC_PF_1:44 for p being Prime for P, Q, R being Element of ProjCo (GF p) st P _EQ_ Q & Q _EQ_ R holds P _EQ_ R proofend; theorem Th45: :: EC_PF_1:45 for p being Prime for a, b being Element of (GF p) for P, Q being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds Q in EC_SetProjCo (a,b,p) proofend; definition let p be Prime; func R_ProjCo p -> Relation of (ProjCo (GF p)) equals :: EC_PF_1:def 11 { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ; correctness coherence { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } is Relation of (ProjCo (GF p)); proofend; end; :: deftheorem defines R_ProjCo EC_PF_1:def_11_:_ for p being Prime holds R_ProjCo p = { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ; theorem Th46: :: EC_PF_1:46 for p being Prime for P, Q being Element of ProjCo (GF p) holds ( P _EQ_ Q iff [P,Q] in R_ProjCo p ) proofend; registration let p be Prime; cluster R_ProjCo p -> total symmetric transitive ; coherence ( R_ProjCo p is total & R_ProjCo p is symmetric & R_ProjCo p is transitive ) proofend; end; definition let p be Prime; let a, b be Element of (GF p); func R_EllCur (a,b,p) -> Equivalence_Relation of (EC_SetProjCo (a,b,p)) equals :: EC_PF_1:def 12 (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))); correctness coherence (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) is Equivalence_Relation of (EC_SetProjCo (a,b,p)); proofend; end; :: deftheorem defines R_EllCur EC_PF_1:def_12_:_ for p being Prime for a, b being Element of (GF p) holds R_EllCur (a,b,p) = (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))); theorem Th47: :: EC_PF_1:47 for p being Prime for a, b being Element of (GF p) for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) ) proofend; theorem Th48: :: EC_PF_1:48 for p being Prime for a, b being Element of (GF p) for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 holds ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 ) proofend; theorem Th49: :: EC_PF_1:49 for p being Prime for a, b being Element of (GF p) for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 holds ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) proofend; theorem Th50: :: EC_PF_1:50 for p being Prime for a, b being Element of (GF p) for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds ( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) proofend; theorem Th51: :: EC_PF_1:51 for p being Prime for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } proofend; theorem Th52: :: EC_PF_1:52 for p being Prime for a, b, d1, Y1, d2, Y2 being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) holds ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) ) proofend; theorem Th53: :: EC_PF_1:53 for p being Prime for a, b being Element of (GF p) for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } holds F1 misses F2 proofend; theorem Th54: :: EC_PF_1:54 for X being non empty finite set for R being Equivalence_Relation of X for S being Class b2 -valued Function for i being set st i in dom S holds S . i is finite Subset of X proofend; theorem Th55: :: EC_PF_1:55 for X being non empty set for R being Equivalence_Relation of X for S being Class b2 -valued Function st S is one-to-one holds S is disjoint_valued proofend; theorem Th56: :: EC_PF_1:56 for X being non empty set for R being Equivalence_Relation of X for S being Class b2 -valued Function st S is onto holds Union S = X proofend; theorem :: EC_PF_1:57 for X being non empty finite set for R being Equivalence_Relation of X for S being Class b2 -valued Function for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds L . i = card (S . i) ) holds card X = Sum L proofend; theorem Th58: :: EC_PF_1:58 for p being Prime for a, b, d being Element of (GF p) for F, G being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } holds ex I being Function of F,G st ( I is onto & I is one-to-one ) proofend; theorem Th59: :: EC_PF_1:59 for p being Prime for a, b, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) proofend; Lm8: for p being Prime for n being Nat st n in Seg p holds n - 1 is Element of (GF p) proofend; Lm9: for p being Prime for a, b, c, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds ex S being Function st ( dom S = Seg p & ( for n being Nat st n in dom S holds S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) proofend; theorem Th60: :: EC_PF_1:60 for p being Prime for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds ex F being FinSequence of NAT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F ) proofend; theorem :: EC_PF_1:61 for p being Prime for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds ex F being FinSequence of INT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) proofend;