:: Set of Points on Elliptic Curve in Projective Coordinates
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 21, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users

begin

definition

let K be Field;
mode Subfield of K -> Field means :PFDef2: :: 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 b₁ being Field st
( the carrier of b₁ c= the carrier of K & the addF of b₁ = the addF of K || the carrier of b₁ & the multF of b₁ = the multF of K || the carrier of b₁ & 1. b₁ = 1. K & 0. b₁ = 0. K )

proof end;

end;

:: deftheorem PFDef2 defines Subfield EC_PF_1:def 1 :
for K, b₂ being Field holds
( b₂ is Subfield of K iff ( the carrier of b₂ c= the carrier of K & the addF of b₂ = the addF of K || the carrier of b₂ & the multF of b₂ = the multF of K || the carrier of b₂ & 1. b₂ = 1. K & 0. b₂ = 0. K ) );

theorem PF1: :: EC_PF_1:1

for K being Field holds K is Subfield of K

proof end;

theorem PF2: :: 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

proof end;

registration

let K be Field;
cluster non empty non degenerated non trivial 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 Subfield of K;
existence
ex b₁ being Subfield of K st b₁ is strict

proof end;

end;

theorem PF4: :: 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

proof end;

theorem PF5: :: EC_PF_1:4

for K1, K2 being strict Field st K1 is Subfield of K2 & K2 is Subfield of K1 holds
K1 = K2

proof end;

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

proof end;

theorem PF7: :: 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 )

proof end;

theorem PF8: :: 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 )

proof end;

theorem PF9: :: 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 )

proof end;

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 ) )

proof end;

registration

let K be finite Field;
cluster non empty non degenerated non trivial finite 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 Subfield of K;
existence
ex b₁ being Subfield of K st b₁ is finite

proof end;

end;

definition

let K be finite Field;
:: original: card
redefine func card K -> Element of NAT ;
coherence
card K is Element of NAT

proof end;

end;

registration

cluster non empty non degenerated non trivial finite 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 doubleLoopStr ;
existence
ex b₁ being Field st
( b₁ is strict & b₁ is finite )

proof end;

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

proof end;

definition

let IT be Field;
attr IT is prime means :PFDef3: :: EC_PF_1:def 2
for K1 being Field st K1 is strict Subfield of IT holds
K1 = IT;

end;

:: deftheorem PFDef3 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

proof end;

end;

registration

cluster non empty non degenerated non trivial 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 doubleLoopStr ;
existence
ex b₁ being Field st b₁ is prime

proof end;

end;

begin

EXLm1: 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

proof end;

theorem XLm2: :: EC_PF_1:11

for p being Prime holds 0 = 0. (GF p)

proof end;

theorem XLm3: :: EC_PF_1:12

for p being Prime holds 1 = 1. (GF p)

proof end;

theorem GF1: :: EC_PF_1:13

for p being Prime
for a being Element of (GF p) ex n1 being Nat st a = n1 mod p

proof end;

theorem GF2: :: EC_PF_1:14

for i being Integer
for p being Prime ex a being Element of (GF p) st a = i mod p

proof end;

theorem GF3: :: 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

proof end;

theorem GF4: :: 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

proof end;

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

proof end;

theorem GF6: :: 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

proof end;

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

proof end;

theorem GF8: :: 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 )

proof end;

theorem EX1: :: EC_PF_1:21

for p being Prime
for a being Element of (GF p) holds
( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 )

proof end;

EXLm3: for p being Prime
for a being Element of (GF p) holds (power (GF p)) . (a,1) = a

proof end;

EXLm4: for p being Prime
for a being Element of (GF p) holds (power (GF p)) . (a,2) = a * a

proof end;

theorem :: EC_PF_1:22

for p being Prime
for a being Element of (GF p) holds a |^ 2 = a * a by EXLm4;

theorem EX4: :: 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

proof end;

theorem EX5: :: EC_PF_1:24

for n being Nat
for p being Prime
for a being Element of (GF p) holds a |^ (n + 1) = (a |^ n) * a

proof end;

theorem EX6: :: 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

proof end;

theorem EX7: :: 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 ) )

proof end;

theorem EX8: :: 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)

proof end;

theorem EX9: :: EC_PF_1:28

for n being Nat
for p being Prime
for a, b being Element of (GF p) holds (a |^ n) * (b |^ n) = (a * b) |^ n

proof end;

theorem EX10: :: EC_PF_1:29

for n being Nat
for p being Prime
for a being Element of (GF p) st a <> 0 holds
(a ") |^ n = (a |^ n) "

proof end;

theorem EX11: :: EC_PF_1:30

for n1, n2 being Nat
for p being Prime
for a being Element of (GF p) holds (a |^ n1) * (a |^ n2) = a |^ (n1 + n2)

proof end;

theorem EX12: :: EC_PF_1:31

for n1, n2 being Nat
for p being Prime
for a being Element of (GF p) holds (a |^ n1) |^ n2 = a |^ (n1 * n2)

proof end;

registration

let p be Prime;
cluster MultGroup (GF p) -> cyclic ;
coherence
MultGroup (GF p) is cyclic

proof end;

end;

theorem LMCycle4: :: EC_PF_1:32

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

proof end;

theorem LMCycle5: :: EC_PF_1:33

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

proof end;

begin

definition

let p be Prime;
let a be Element of (GF p);
attr a is quadratic_residue means :QRDef1: :: EC_PF_1:def 3
( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a );
attr a is not_quadratic_residue means :QRDef2: :: EC_PF_1:def 4
( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) );

end;

:: deftheorem QRDef1 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 QRDef2 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 QR1: :: EC_PF_1:34

for p being Prime
for a being Element of (GF p) st a <> 0 holds
a |^ 2 is quadratic_residue

proof end;

registration

let p be Prime;
cluster 1. (GF p) -> quadratic_residue ;
correctness
coherence
1. (GF p) is quadratic_residue ;

proof end;

end;

definition

let p be Prime;
let a be Element of (GF p);
func Lege_p a -> Integer equals :QRDef3: :: 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 b₁ being Integer st a = 0 & a is quadratic_residue holds
( b₁ = 0 iff b₁ = 1 ) by QRDef1;

end;

:: deftheorem QRDef3 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 QR10: :: EC_PF_1:35

for p being Prime
for a being Element of (GF p) holds
( a is not_quadratic_residue iff Lege_p a = - 1 )

proof end;

theorem QR11: :: EC_PF_1:36

for p being Prime
for a being Element of (GF p) holds
( a is quadratic_residue iff Lege_p a = 1 )

proof end;

theorem QR12: :: EC_PF_1:37

for p being Prime
for a being Element of (GF p) holds
( a = 0 iff Lege_p a = 0 )

proof end;

theorem :: EC_PF_1:38

for p being Prime
for a being Element of (GF p) st a <> 0 holds
Lege_p (a |^ 2) = 1

proof end;

theorem QR14: :: EC_PF_1:39

for p being Prime
for a, b being Element of (GF p) holds Lege_p (a * b) = (Lege_p a) * (Lege_p b)

proof end;

theorem QR15: :: EC_PF_1:40

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

proof end;

theorem :: EC_PF_1:41

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

proof end;

theorem QRRT1: :: EC_PF_1:42

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)

proof end;

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:];

proof end;

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 GFProjCo: :: EC_PF_1:43

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]}

proof end;

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 |^ 2)) + (g27 * (b |^ 3));
existence
ex b₁ being Element of (GF p) st
for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b₁ = (g4 * (a |^ 2)) + (g27 * (b |^ 3))

proof end;

uniqueness
for b₁, b₂ being Element of (GF p) st ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b₁ = (g4 * (a |^ 2)) + (g27 * (b |^ 3)) ) & ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b₂ = (g4 * (a |^ 2)) + (g27 * (b |^ 3)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines Disc EC_PF_1:def 7 :
for p being Prime
for a, b, b₄ being Element of (GF p) holds
( b₄ = Disc (a,b,p) iff for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b₄ = (g4 * (a |^ 2)) + (g27 * (b |^ 3)) );

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 :ECDefEQ: :: 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) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3)));
existence
ex b₁ 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 b₁ . P = (((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3)))

proof end;

uniqueness
for b₁, b₂ 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 b₁ . P = (((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3))) ) & ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b₂ . P = (((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem ECDefEQ defines EC_WEqProjCo EC_PF_1:def 8 :
for p being Prime
for a, b being Element of (GF p)
for b₄ being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) holds
( b₄ = 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 b₄ . P = (((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3))) );

theorem LmECDefEQ: :: EC_PF_1:44

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)))

proof end;

LML: 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) )

proof end;

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));

proof end;

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) } ;

LMNGA0: for p being Prime
for d, Y being Element of (GF p) holds [d,Y,1] is Element of ProjCo (GF p)

proof end;

theorem ECZERO: :: EC_PF_1:45

for p being Prime
for a, b being Element of (GF p) holds [0,1,0] is Element of EC_SetProjCo (a,b,p)

proof end;

theorem ECAFF: :: EC_PF_1:46

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) )

proof end;

definition

let p be Prime;
let P, Q be Element of ProjCo (GF p);
pred P _EQ_ Q means :DefEQV: :: EC_PF_1:def 10
ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1 = a * (Q `1) & P `2 = a * (Q `2) & P `3 = a * (Q `3) );
reflexivity
for P being Element of ProjCo (GF p) ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1 = a * (P `1) & P `2 = a * (P `2) & P `3 = a * (P `3) )

proof end;

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 = a * (Q `1) & P `2 = a * (Q `2) & P `3 = a * (Q `3) ) holds
ex a being Element of (GF p) st
( a <> 0. (GF p) & Q `1 = a * (P `1) & Q `2 = a * (P `2) & Q `3 = a * (P `3) )

proof end;

end;

:: deftheorem DefEQV 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 = a * (Q `1) & P `2 = a * (Q `2) & P `3 = a * (Q `3) ) );

theorem LmEQV3: :: EC_PF_1:47

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

proof end;

theorem LmEQV4: :: EC_PF_1:48

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 = d * (P `1) & Q `2 = d * (P `2) & Q `3 = d * (P `3) holds
Q in EC_SetProjCo (a,b,p)

proof end;

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));

proof end;

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 LmDefREQ: :: EC_PF_1:49

for p being Prime
for P, Q being Element of ProjCo (GF p) holds
( P _EQ_ Q iff [P,Q] in R_ProjCo p )

proof end;

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 )

proof end;

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));

proof end;

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 LmDefREQ0: :: EC_PF_1:50

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) )

proof end;

theorem LmDefREQ1: :: EC_PF_1:51

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 <> 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3 = 1 )

proof end;

theorem LmDefREQ2: :: EC_PF_1:52

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 = 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1 = 0 & Q `2 = 1 & Q `3 = 0 )

proof end;

theorem LmDefREQ3: :: EC_PF_1:53

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) )

proof end;

theorem LmDefREQ4: :: EC_PF_1:54

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] ) }

proof end;

theorem LMNGA2: :: EC_PF_1:55

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 ) )

proof end;

theorem MIS: :: EC_PF_1:56

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

proof end;

theorem LmDefREQ42: :: EC_PF_1:57

for X being non empty finite set
for R being Equivalence_Relation of X
for S being Class b₂ -valued Function
for i being set st i in dom S holds
S . i is finite Subset of X

proof end;

theorem LmDefREQ43: :: EC_PF_1:58

for X being non empty set
for R being Equivalence_Relation of X
for S being Class b₂ -valued Function st S is one-to-one holds
S is disjoint_valued

proof end;

theorem LmDefREQ44: :: EC_PF_1:59

for X being non empty set
for R being Equivalence_Relation of X
for S being Class b₂ -valued Function st S is onto holds
union (rng S) = X

proof end;

theorem :: EC_PF_1:60

for X being non empty finite set
for R being Equivalence_Relation of X
for S being Class b₂ -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

proof end;

theorem LmCardA: :: EC_PF_1:61

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 )

proof end;

theorem LmECPFCardB: :: EC_PF_1:62

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))

proof end;

LMNG: for p being Prime
for n being Nat st n in Seg p holds
n - 1 is Element of (GF p)

proof end;

LmECPFCardC: 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 (rng 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] ) } )

proof end;

theorem LmECPFCardY: :: EC_PF_1:63

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 )

proof end;

theorem :: EC_PF_1:64

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) )

proof end;