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

AA: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds x = [(x `1_3),(x `2_3),(x `3_3)]
;

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 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 Def1 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 Th1: :: EC_PF_1:1

for K being Field holds K is Subfield of K

proof end;

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

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 for Subfield of K;

existence
ex b₁ being Subfield of K st b₁ is strict

proof end;

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

proof end;

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

proof end;

theorem :: EC_PF_1:5

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

proof end;

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 )

proof end;

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 )

proof end;

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 )

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 for 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 for 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 :: EC_PF_1:def 2
for K1 being Field st K1 is strict Subfield of IT holds
K1 = IT;

end;

:: deftheorem 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 for doubleLoopStr ;

existence
ex b₁ being Field st b₁ is prime

proof end;

end;

theorem Th11: :: EC_PF_1:11

for p being Prime holds 0 = 0. (GF p) by NAT_1:44, SUBSET_1:def 8;

theorem Th12: :: EC_PF_1:12

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

proof end;

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

proof end;

theorem Th14: :: EC_PF_1:14

for i being Integer
for p being Prime holds i mod p is Element of (GF p)

proof end;

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

proof end;

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

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

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

proof end;

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 )

proof end;

Lm1: for p being Prime
for a being Element of (GF p) holds (power (GF p)) . (a,1) = a
by GROUP_1:50;

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

theorem Th23: :: EC_PF_1:23

for n, n1 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 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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

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

proof end;

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

proof end;

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

proof end;

definition

let p be Prime;
let a be Element of (GF p);

attr a is quadratic_residue means :: 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 :: EC_PF_1:def 4
( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) );

end;

:: deftheorem 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 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 by Th25;

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 :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 b₁ being Integer st a = 0 & a is quadratic_residue holds
( b₁ = 0 iff b₁ = 1 ) ;

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 )

proof end;

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

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

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 by Th31, Th33;

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)

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

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 |^ 3)) + (g27 * (b |^ 2));

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 |^ 3)) + (g27 * (b |^ 2))

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 |^ 3)) + (g27 * (b |^ 2)) ) & ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b₂ = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) 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 |^ 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 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_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_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_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 b₂ . 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
b₁ = b₂

proof end;

end;

:: deftheorem Def8 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_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)))

proof end;

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

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

proof end;

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

proof end;

definition

let p be Prime;
let P, Q be Element of ProjCo (GF p);

pred P _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) )

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

proof end;

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

proof end;

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)

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

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

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th54: :: EC_PF_1:54

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 Th55: :: EC_PF_1:55

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 Th56: :: EC_PF_1:56

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 S = X

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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

proof end;