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

ex b_{1} being Field st

( the carrier of b_{1} c= the carrier of K & the addF of b_{1} = the addF of K || the carrier of b_{1} & the multF of b_{1} = the multF of K || the carrier of b_{1} & 1. b_{1} = 1. K & 0. b_{1} = 0. K )

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

ex b

( the carrier of b

proof end;

:: deftheorem Def1 defines Subfield EC_PF_1:def 1 :

for K, b_{2} being Field holds

( b_{2} is Subfield of K iff ( the carrier of b_{2} c= the carrier of K & the addF of b_{2} = the addF of K || the carrier of b_{2} & the multF of b_{2} = the multF of K || the carrier of b_{2} & 1. b_{2} = 1. K & 0. b_{2} = 0. K ) );

for K, b

( b

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

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;

ex b_{1} being Subfield of K st b_{1} is strict

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

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

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 )

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 )

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 )

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

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;

ex b_{1} being Subfield of K st b_{1} is finite

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

proof end;

definition

let K be finite Field;

:: original: card

redefine func card K -> Element of NAT ;

coherence

card K is Element of NAT

end;
:: original: card

redefine func card K -> Element of NAT ;

coherence

card K is Element of NAT

proof end;

registration

ex b_{1} being Field st

( b_{1} is strict & b_{1} is finite )
end;

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

( b

proof 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

for SK1 being strict Subfield of K st card K = card SK1 holds

SK1 = K

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

for IT being Field holds

( IT is prime iff for K1 being Field st K1 is strict Subfield of IT holds

K1 = IT );

registration

ex b_{1} being Field st b_{1} is prime
end;

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

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

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

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

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

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

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;

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

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

for a being Element of K

for n being Nat holds a |^ (n + 1) = (a |^ n) * a

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

for x, y being Element of F holds

( x * x = y * y iff ( x = y or x = - y ) )

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

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;

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

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

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

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

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

( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) );

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

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

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

definition

let p be Prime;

let a be Element of (GF p);

( ( 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_{1} being Integer st a = 0 & a is quadratic_residue holds

( b_{1} = 0 iff b_{1} = 1 )
;

end;
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 0 if a = 0

1 if a is quadratic_residue

otherwise - 1;

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

( b

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

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 )

for a being Element of (GF p) holds

( a is not_quadratic_residue iff Lege_p a = - 1 )

proof end;

theorem :: EC_PF_1:35

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

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

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)

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;

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

end;
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 [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]};

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;

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

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

ex b_{1} 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_{1} = (g4 * (a |^ 3)) + (g27 * (b |^ 2))

for b_{1}, b_{2} 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_{1} = (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_{2} = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) holds

b_{1} = b_{2}

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

ex b

for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines Disc EC_PF_1:def 7 :

for p being Prime

for a, b, b_{4} being Element of (GF p) holds

( b_{4} = Disc (a,b,p) iff for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds

b_{4} = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) );

for p being Prime

for a, b, b

( b

b

definition

let p be Prime;

let a, b be Element of (GF p);

ex b_{1} 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_{1} . 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 b_{1}, b_{2} 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_{1} . 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_{2} . 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_{1} = b_{2}

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

ex b

for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b

proof end;

uniqueness for b

b

proof 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_{4} being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) holds

( b_{4} = 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_{4} . 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 Prime

for a, b being Element of (GF p)

for b

( b

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

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

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

end;
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 { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;

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;

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

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

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

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

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

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

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;

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

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

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;

coherence

{ [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } is Relation of (ProjCo (GF p));

end;
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 { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ;

coherence

{ [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } is Relation of (ProjCo (GF p));

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

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 )

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;

coherence

( R_ProjCo p is total & R_ProjCo p is symmetric & R_ProjCo p is transitive )

end;
coherence

( R_ProjCo p is total & R_ProjCo p is symmetric & R_ProjCo p is transitive )

proof end;

definition

let p be Prime;

let a, b be Element of (GF p);

coherence

(R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) is Equivalence_Relation of (EC_SetProjCo (a,b,p));

end;
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 (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p)));

coherence

(R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) is Equivalence_Relation of (EC_SetProjCo (a,b,p));

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

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

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 )

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 )

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

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

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

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

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_{2} -valued Function

for i being set st i in dom S holds

S . i is finite Subset of X

for R being Equivalence_Relation of X

for S being Class b

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_{2} -valued Function st S is one-to-one holds

S is disjoint_valued

for R being Equivalence_Relation of X

for S being Class b

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_{2} -valued Function st S is onto holds

Union S = X

for R being Equivalence_Relation of X

for S being Class b

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_{2} -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

for R being Equivalence_Relation of X

for S being Class b

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 )

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

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 )

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

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;