:: Set of Points on Elliptic Curve in Projective Coordinates
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 21, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_3, NEWTON,
TARSKI, FINSET_1, CARD_3, FINSEQ_1, SUBSET_1, ARYTM_1, XXREAL_0, FUNCT_2,
PARTFUN1, INT_2, NAT_1, BINOP_1, BINOP_2, REALSET1, ZFMISC_1, INT_3,
SUPINF_2, ALGSTR_0, GROUP_1, MESFUNC1, INT_1, VECTSP_1, STRUCT_0,
GROUP_2, GRAPH_1, FINSEQ_2, EC_PF_1, RLVECT_1, LATTICES, EQREL_1,
RELAT_2, UNIROOTS, PROB_2, MOD_2, RECDEF_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELAT_2,
RELSET_1, PARTFUN1, XTUPLE_0, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1,
FINSET_1, CARD_3, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
INT_1,
INT_2, NAT_D, REALSET1, FINSEQ_1, FINSEQ_2, EQREL_1, RVSUM_1, NEWTON,
WSIERP_1, MOD_2, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1,
GROUP_2, GR_CY_1, INT_3, UNIROOTS, PROB_2, BINOM;
constructors NAT_D, REALSET1, GROUP_2, BINOP_1, GR_CY_1, INT_3, WSIERP_1,
UPROOTS, BINOP_2, RELSET_1, FUNCT_7, UNIROOTS, PROB_2, BINOM, MOD_2,
XTUPLE_0, NUMBERS, NEWTON;
registrations XBOOLE_0, STRUCT_0, XREAL_0, ORDINAL1, NAT_1, INT_1, GROUP_2,
FINSET_1, ALGSTR_0, VECTSP_1, INT_3, XXREAL_0, NEWTON, SUBSET_1, CARD_1,
RELAT_2, VALUED_0, EQREL_1, RELSET_1, FINSEQ_2, UNIROOTS, NUMBERS,
MEMBERED, XTUPLE_0, MCART_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions GROUP_1, ALGSTR_0, TARSKI, VECTSP_1, RLVECT_1;
equalities STRUCT_0, INT_3, ALGSTR_0, BINOP_1, FINSEQ_1, REALSET1, FINSEQ_2,
EQREL_1, BINOM, CARD_3;
expansions STRUCT_0, ALGSTR_0, FINSEQ_1, TARSKI;
theorems TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, FUNCT_1, FUNCT_2, VECTSP_1,
INT_1, RLVECT_1, GR_CY_1, NAT_1, INT_2, INT_3, PEPIN, NAT_D, NUMBERS,
CARD_1, GROUP_1, GROUP_2, XREAL_1, NEWTON, XXREAL_0, NAT_3, RVSUM_1,
CARD_2, EULER_1, XBOOLE_1, FINSEQ_1, RELSET_1, FUNCOP_1, PARTFUN1,
FINSEQ_2, BINOP_1, ALGSTR_0, MCART_1, EQREL_1, UNIROOTS, RELAT_2,
GR_CY_3, DIST_1, PROB_2, BINOM, MOD_2, XTUPLE_0, SUBSET_1, XREAL_0;
schemes NAT_1, FUNCT_2, INT_1, FINSEQ_1;
begin :: 1.Finite Prime Field $\bf{GF}(p)$
reserve x for set;
reserve i,j for Integer;
reserve n,n1,n2,n3 for Nat;
reserve K,K1,K2,K3 for Field;
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:
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
proof
take K;
thus thesis by RELSET_1:19;
end;
end;
theorem Th1:
K is Subfield of K
proof
A1: the addF of K = (the addF of K) || the carrier of K by RELSET_1:19;
A2: the multF of K = (the multF of K) || the carrier of K by RELSET_1:19;
the carrier of K c= the carrier of K & 1.K = 1.K & 0.K = 0.K;
hence thesis by A1,A2,Def1;
end;
theorem Th2:
for ST be 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 commutative almost_left_invertible
non degenerated holds ST is Subfield of K
proof
let ST be non empty doubleLoopStr such that
A1: the carrier of ST is Subset of the carrier of K and
A2: the addF of ST = (the addF of K) || the carrier of ST and
A3: the multF of ST = (the multF of K) || the carrier of ST and
A4: 1.ST = 1.K and
A5: 0.ST = 0.K and
A6: ST is right_complementable commutative
almost_left_invertible non degenerated;
set C1 = the carrier of ST;
set AC = the addF of ST;
set MC = the multF of ST;
set d0 = 0.ST;
set d1 = 1.ST;
A7: now
let a,x be Element of ST;
a*x = (the multF of K).([a,x]) by A3,FUNCT_1:49;
hence a*x = (the multF of K).(a,x);
end;
A8: now
let x,y be Element of ST;
x + y = (the addF of K).([x,y]) by A2,FUNCT_1:49;
hence x + y = (the addF of K).(x,y);
end;
ST is Abelian add-associative right_zeroed associative well-unital
distributive
proof
set MK = the multF of K;
set AK = the addF of K;
hereby
let x,y be Element of ST;
reconsider x1 = x, y1 = y as Element of K by A1,TARSKI:def 3;
x + y = x1 + y1 & y + x = y1 + x1 by A8;
hence x + y = y + x;
end;
hereby
let x,y,z be Element of ST;
reconsider x1 = x, y1 = y, z1 = z as Element of K by A1,TARSKI:def 3;
x + (y + z) = AK.(x1,y + z) by A8; then
A9: x + (y + z) = x1 + (y1 + z1) by A8;
(x + y) + z = AK.(x +y,z1) by A8;
then (x + y) + z = (x1 + y1) + z1 by A8;
hence (x + y) + z = x + (y + z) by A9,RLVECT_1:def 3;
end;
hereby
let x be Element of ST;
reconsider y = x, z = 0.ST as Element of K by A1,TARSKI:def 3;
x + 0.ST = y + 0.K by A5,A8;
hence x + 0.ST = x by RLVECT_1:4;
end;
hereby
let a,b,x be Element of ST;
reconsider y=x, a1=a, b1=b as Element of K by A1,TARSKI:def 3;
a * (b * x) = MK.(a,b * x) by A7; then
A10: a * (b * x) = a1 * (b1 * y) by A7;
a * b = a1 * b1 by A7;
then (a * b) * x = (a1 * b1) * y by A7;
hence (a * b) * x = a * (b * x) by A10,GROUP_1:def 3;
end;
hereby
let x be Element of ST;
reconsider y = x as Element of K by A1,TARSKI:def 3;
x*1.ST = y * 1.K & 1.ST * x = 1.K * y by A4,A7;
hence x*1.ST = x & 1.ST * x =x;
end;
hereby
let a,x,y be Element of ST;
reconsider x1=x, y1=y, a1=a as Element of K by A1,TARSKI:def 3;
(x+y)*a = MK.(x+y,a) by A7;
then (x+y)*a = (x1+y1)*a1 by A8;
then (x+y)*a = x1*a1 + y1*a1 by VECTSP_1:def 7;
then (x+y)*a = AK.(MK.(x1,a1),y*a) by A7; then
A11: (x+y)*a = AK.(x*a,y*a) by A7;
a*(x+y) = MK.(a,x+y) by A7;
then a*(x+y) = a1*(x1+y1) by A8;
then a*(x+y) = a1*x1 + a1*y1 by VECTSP_1:def 7;
then a*(x+y) = AK.(MK.(a,x1),a*y) by A7;
then a*(x+y) = AK.(a*x,a*y) by A7;
hence a*(x+y) = a*x + a*y & (x+y)*a = x*a + y*a by A8,A11;
end;
end;
hence thesis by A1,A2,A3,A4,A5,A6,Def1;
end;
registration let K be Field;
cluster strict for Subfield of K;
existence
proof
set C1 = [#]K;
A1: the addF of K = (the addF of K) || C1
& the multF of K = (the multF of K) || C1 by RELSET_1:19;
set ST = doubleLoopStr (# the carrier of K, the addF of K,
the multF of K, 1.K, 0.K #);
ST is right_complementable commutative almost_left_invertible
non degenerated
proof
thus ST is right_complementable
proof
let x be Element of ST;
reconsider x1 = x as Element of K;
consider v be Element of K such that
A2: x1 + v = 0.K by ALGSTR_0:def 11;
reconsider y = v as Element of ST;
take y;
thus thesis by A2;
end;
thus ST is commutative
proof
let x,y be Element of ST;
reconsider x1 = x, y1 = y as Element of K;
x * y = x1 * y1 & y * x = y1 * x1;
hence x * y = y * x;
end;
thus ST is almost_left_invertible
proof
let x be Element of ST such that A3: x <> 0.ST;
reconsider x1 = x as Element of K;
x1 is left_invertible by A3,ALGSTR_0:def 39;
then consider v be Element of K such that
A4: v * x1 = 1.K;
reconsider y = v as Element of ST;
take y;
thus thesis by A4;
end;
thus thesis;
end; then
ST is Subfield of K by A1,Th2;
hence thesis;
end;
end;
reserve SK1,SK2 for Subfield of K;
reserve ek,ek1,ek2 for Element of K;
theorem Th3:
K1 is Subfield of K2 implies for x st x in K1 holds x in K2
proof
assume K1 is Subfield of K2;
then A1: the carrier of K1 c= the carrier of K2 by Def1;
for x st x in K1 holds x in K2
by A1;
hence thesis;
end;
theorem Th4:
for K1,K2 be strict Field st
K1 is Subfield of K2 & K2 is Subfield of K1 holds K1 = K2
proof
let K1,K2 be strict Field;
assume A1: K1 is Subfield of K2
& K2 is Subfield of K1;
A2: the carrier of K1 c= the carrier of K2 &
the carrier of K2 c= the carrier of K1 by A1,Def1; then
A3: the carrier of K1 = the carrier of K2 by XBOOLE_0:def 10;
A4: the addF of K2 = (the addF of K2) || the carrier of K1 by A3,RELSET_1:19
.= the addF of K1 by A1,Def1;
A5: the multF of K2 = (the multF of K2) || the carrier of K1
by A3,RELSET_1:19
.= the multF of K1 by A1,Def1;
1.K1 = 1.K2 & 0.K1 = 0.K2 by A1,Def1;
hence thesis by A4,A5,A2,XBOOLE_0:def 10;
end;
theorem
for K1, K2, K3 be Field st
K1 is Subfield of K2 & K2 is Subfield of K3 holds K1 is Subfield of K3
proof
let K1, K2, K3 be Field;
assume A1: K1 is Subfield of K2 & K2 is Subfield of K3;
set C1 = the carrier of K1;
set C2 = the carrier of K2;
set C = the carrier of K3;
set ADD = the addF of K3;
set MULT = the multF of K3;
A2: C1 c= C2 by A1,Def1;
then A3: [:C1,C1:] c= [:C2,C2:] by ZFMISC_1:96;
C2 c= C by A1,Def1; then
A4: C1 c= C by A2;
A5: the addF of K2 = ADD || C2 by A1,Def1;
A6: the addF of K1 = (the addF of K2) || C1 by A1,Def1
.= ADD || C1 by A3,A5,FUNCT_1:51;
A7: the multF of K2 = MULT || C2 by A1,Def1;
A8: the multF of K1 = (the multF of K2) || C1 by A1,Def1
.= MULT || C1 by A3,A7,FUNCT_1:51;
1.K1 = 1.K2 & 0.K1 = 0.K2 by A1,Def1;
then 1.K1 = 1.K3 & 0.K1 = 0.K3 by A1,Def1;
hence thesis by A4,A6,A8,Def1;
end;
theorem Th6:
SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2
proof
set C1 = the carrier of SK1;
set C2 = the carrier of SK2;
set ADD = the addF of K;
set MULT = the multF of K;
thus SK1 is Subfield of SK2 implies C1 c= C2 by Def1;
assume A1: C1 c= C2;
then A2: [:C1,C1:] c= [:C2,C2:] by ZFMISC_1:96;
the addF of SK2 = ADD || C2 by Def1;
then A3: (the addF of SK2) || C1 = ADD || C1 by A2,FUNCT_1:51
.= the addF of SK1 by Def1;
the multF of SK2 = MULT || C2 by Def1;
then A4: (the multF of SK2) || C1 = MULT || C1 by A2,FUNCT_1:51
.= the multF of SK1 by Def1;
1.SK1 = 1.K & 0.SK1 = 0.K by Def1;
then 1.SK1 = 1.SK2 & 0.SK1 = 0.SK2 by Def1;
hence thesis by A1,A3,A4,Def1;
end;
theorem Th7:
SK1 is Subfield of SK2 iff for x st x in SK1 holds x in SK2
proof
thus SK1 is Subfield of SK2 implies
for x st x in SK1 holds x in SK2 by Th3;
assume A1: for x st x in SK1 holds x in SK2;
the carrier of SK1 c= the carrier of SK2
proof
let x be object;
assume x in the carrier of SK1;
then reconsider x as Element of SK1;
x in SK1;
then x in SK2 by A1;
hence thesis;
end;
hence thesis by Th6;
end;
theorem Th8:
for SK1,SK2 be strict Subfield of K holds
SK1 = SK2 iff the carrier of SK1 = the carrier of SK2
proof
let SK1, SK2 be strict Subfield of K;
thus SK1 = SK2 implies
the carrier of SK1 = the carrier of SK2;
assume A1: the carrier of SK1 = the carrier of SK2;
then A2: SK2 is strict Subfield of SK1 by Th6;
SK1 is strict Subfield of SK2 by A1,Th6;
hence thesis by A2,Th4;
end;
theorem
for SK1, SK2 be strict Subfield of K holds
(SK1 = SK2 iff for x holds x in SK1 iff x in SK2)
proof
let SK1,SK2 be strict Subfield of K;
thus SK1 = SK2 implies for x holds x in SK1 iff x in SK2;
assume for x holds x in SK1 iff x in SK2;
then SK1 is strict Subfield of SK2
& SK2 is strict Subfield of SK1 by Th7;
hence thesis by Th4;
end;
registration
let K be finite Field;
cluster finite for Subfield of K;
existence
proof
reconsider L = K as Subfield of K by Th1;
take L;
thus thesis;
end;
end;
definition
let K be finite Field;
redefine func card K -> Element of NAT; :: redefines card (STRUCT_0, definition)
coherence
proof
card the carrier of K in NAT;
hence thesis;
end;
end;
registration
cluster strict finite for Field;
existence
proof
Z_3 is finite by MOD_2:def 20;
hence thesis by MOD_2:27;
end;
end;
theorem
for K be strict finite Field,
SK1 be strict Subfield of K st
card K = card SK1 holds SK1 = K
proof
let K be strict finite Field, SK1 be strict Subfield of K;
assume
A1: card K = card SK1;
A2: the carrier of SK1 = the carrier of K
proof
assume A3: the carrier of SK1 <> the carrier of K;
A4: the carrier of SK1 c= the carrier of K by Def1; then
the carrier of SK1 c< the carrier of K by A3,XBOOLE_0:def 8;
hence contradiction by A1,A4,CARD_2:48;
end;
K is Subfield of K by Th1;
hence thesis by A2,Th8;
end;
definition let IT be Field;
attr IT is prime means
K1 is strict Subfield of IT implies K1 = IT;
end;
notation let p be Prime;
synonym GF(p) for INT.Ring(p);
end;
registration let p be Prime;
cluster GF(p) -> finite;
coherence;
end;
registration let p be Prime;
cluster GF(p) -> prime;
coherence
proof
set K = GF(p);
A1: p > 1 by INT_2:def 4;
now let K1 be strict Subfield of K;
set C = the carrier of K;
set C1 = the carrier of K1;
set n1 = p-1;
reconsider n1 as Element of NAT by A1,NAT_1:20;
A2: for x st x in K holds x in K1
proof
A3: for n be Element of NAT st n in Segm(p) holds n in C1
proof
defpred P[Nat] means $1 in C1;
0 in Segm(p) by NAT_1:44;
then 0.K = 0 by SUBSET_1:def 8;
then 0.K1 = 0 by Def1;
then A4: P[0];
A5: now let n be Element of NAT such that A6: 0<=n & n<n1;
assume A7: P[n];
A8: 1.K1 = 1.K by Def1
.= 1 by A1,INT_3:14;
then A9: [1,n] in [:C1,C1:] by A7,ZFMISC_1:87;
A10: the addF of K1 = (the addF of K) || C1 by Def1;
A11: 1+n < n1+1 by A6,XREAL_1:6;
n < n1+1 by A6,NAT_1:13;
then A12: 1 in Segm(p) & n in Segm(p) by A1,NAT_1:44;
(the addF of K1).(1,n) = (addint(p)).(1,n) by A9,A10,FUNCT_1:49
.= (1+n) mod p by A12,GR_CY_1:def 4
.= 1+n by A11,NAT_D:63;
hence P[n+1] by A7,A8,BINOP_1:17;
end;
A13: for n being Element of NAT st 0 <= n & n <= n1 holds P[n]
from INT_1:sch 7(A4,A5);
thus for n be Element of NAT st n in Segm(p) holds P[n]
proof
let n be Element of NAT such that A14: n in Segm(p);
0 <= n & n < n1+1 by A14,NAT_1:44;
then 0 <= n & n <= n1 by NAT_1:13;
hence P[n] by A13;
end;
end;
thus for x st x in K holds x in K1
by A3;
end;
K is strict Subfield of K by Th1;
then K is strict Subfield of K1 by A2,Th7;
hence K1 = K by Th4;
end;
then K1 is strict Subfield of K implies K1 = K;
hence thesis;
end;
end;
registration
cluster prime for Field;
existence
proof
take GF(the Prime);
thus thesis;
end;
end;
begin :: 2. Arithmetic in $\bf{GF}(p)$
reserve p for Prime;
reserve a,b,c for Element of GF(p);
reserve F for FinSequence of GF(p);
theorem Th11:
0 = 0.(GF p) by NAT_1:44,SUBSET_1:def 8;
theorem Th12:
1 = 1.(GF p)
proof
1 < p by INT_2:def 4;
then 1 in Segm p by NAT_1:44;
hence thesis by SUBSET_1:def 8;
end;
theorem Th13:
ex n1 st a = n1 mod p
proof
reconsider a as Element of Segm(p);
0<=a & a<p by NAT_1:44;
then a = a mod p by NAT_D:63;
hence thesis;
end;
theorem Th14:
i mod p is Element of GF(p)
proof
reconsider b = i mod p as Integer;
b in NAT by INT_1:3;
then reconsider b as Nat;
b<p by INT_1:58;
then b in Segm(p) by NAT_1:44;
hence thesis;
end;
theorem Th15:
a = i mod p & b = j mod p implies a+b = (i+j) mod p
proof
assume A1: a = i mod p & b = j mod p;
a+b = ((i mod p) + (j mod p)) mod p by A1,GR_CY_1:def 4;
hence thesis by NAT_D:66;
end;
theorem Th16:
a = i mod p implies -a = (p-i) mod p
proof
assume A1: a = i mod p;
reconsider b = (p-i) mod p as Element of GF(p) by Th14;
a+b = (i+(p-i)) mod p by A1,Th15
.= 0 by INT_1:50
.= 0.GF(p) by Th11;
hence thesis by VECTSP_1:16;
end;
theorem
a = i mod p & b = j mod p implies a-b = (i-j) mod p
proof
assume A1: a = i mod p & b = j mod p; then
-b = (p-j) mod p by Th16;
then a-b = (i+(p-j)) mod p by A1,Th15
.= (i-j+1*p) mod p;
hence thesis by NAT_D:61;
end;
theorem Th18:
a = i mod p & b = j mod p implies a*b = (i*j) mod p
proof
assume a = i mod p & b = j mod p; then
a*b = ((i mod p) * (j mod p)) mod p by INT_3:def 10;
hence thesis by NAT_D:67;
end;
theorem
a = i mod p & i*j mod p = 1 implies a" = j mod p
proof
assume A1: a = i mod p & i*j mod p = 1;
reconsider b = j mod p as Element of GF(p) by Th14;
A2: p > 1 by INT_2:def 4;
A3: b*a = 1 by A1,Th18
.= 1.GF(p) by A2,INT_3:14; then
a <> 0.(GF(p));
hence thesis by A3,VECTSP_1:def 10;
end;
theorem Th20:
a = 0 or b = 0 iff a*b = 0
proof
a = 0.GF(p) or b = 0.GF(p) iff a*b = 0.GF(p) by VECTSP_1:12;
hence thesis;
end;
theorem Th21:
a |^ 0 = 1_GF(p) & a |^ 0 = 1
proof
thus A1: a |^ 0 = 1_GF(p) by BINOM:8;
p > 1 by INT_2:def 4;
hence a |^ 0 = 1 by A1,INT_3:14;
end;
Lm1: (power GF(p)).(a,1) = a by GROUP_1:50;
Lm2: (power GF(p)).(a,2) = a*a by GROUP_1:51;
theorem
a |^ 2 = a*a by Lm2;
theorem Th23:
a = n1 mod p implies a|^n = n1|^n mod p
proof
A1: p > 1 by INT_2:def 4;
assume A2: a = n1 mod p;
defpred P[Nat] means
(power GF(p)).(a,$1) = n1|^($1) mod p;
a|^0 = 1 by Th21;
then A3: a|^0 = 1 mod p by A1,NAT_D:63;
A4: P[0] by A3,NEWTON:4;
A5: now let n be Nat;
assume A6: P[n];
reconsider b = (power GF(p)).(a,n) as Element of GF(p);
(power GF(p)).(a,n+1) = b*a by GROUP_1:def 7
.= (n1|^n*n1) mod p by A2,A6,Th18
.= n1|^(n+1) mod p by NEWTON:6;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
theorem Th24:
for K being unital associative non empty multMagma, a being
Element of K, n being Nat holds a|^(n+1) = (a|^n) * a
proof
let K be unital associative non empty multMagma, a be
Element of K, n be Nat;
a|^(n+1) = (a|^n) * (a|^1) by BINOM:10 .= (a|^n) * a by BINOM:8;
hence thesis;
end;
theorem Th25:
a <> 0 implies a |^ n <> 0
proof
assume A1: a <> 0;
consider n1 be Nat such that A2: a = n1 mod p by Th13;
not p divides n1 by A1,A2,INT_1:62;
then not p divides n1|^n by NAT_3:5;
then n1|^n mod p <> 0 by INT_1:62;
hence thesis by A2,Th23;
end;
theorem Th26:
for F being Abelian add-associative right_zeroed right_complementable
associative commutative well-unital almost_left_invertible distributive
non empty doubleLoopStr, x,y being Element of F holds x*x=y*y
iff x=y or x=-y
proof
let F be Abelian add-associative right_zeroed right_complementable
associative commutative well-unital almost_left_invertible
distributive non empty doubleLoopStr, x,y be Element of F;
A1: (x-y)*(x+y) =(x-y)*x +(x-y)*y by VECTSP_1:def 7
.=x*x -x*y +(x-y)*y by VECTSP_1:11
.=x*x -x*y + (y*x-y*y) by VECTSP_1:11
.=(x*x -x*y + y*x) + -y*y by RLVECT_1:def 3
.=(x*x + ((-x*y) + y*x)) + -y*y by RLVECT_1:def 3
.=(x*x + (y*x - x*y )) + -y*y
.= (x*x + (x-x)*y ) + -y*y by VECTSP_1:11
.= (x*x + 0.F * y )-y*y by RLVECT_1:5
.= (x*x + 0.F )-y*y
.= x*x - y*y by RLVECT_1:def 4;
hereby assume A2: x*x=y*y;
(x-y)*(x+y) = 0.F by A1,A2,RLVECT_1:5;
then x-y =0.F or x + y = 0.F by VECTSP_1:12;
hence x = y or x =-y by RLVECT_1:6,21;
end;
assume x = y or x =-y;
then x-y =0.F or x+y = 0.F by RLVECT_1:5;
hence x*x = y*y by A1,RLVECT_1:21;
end;
theorem Th27:
for p be Prime, x be Element of GF(p) st 2 < p & x+x = 0.(GF p)
holds x = 0.(GF(p))
proof
let p be Prime, x be Element of GF(p);
assume A1:2 < p & x+x = 0.(GF(p));
x in Segm p; then
reconsider Ix=x as Element of NAT;
A2: 1= 1.(GF(p)) by Th12;
A3: 1+1 < p by A1;
A4: 1.(GF(p))+1.(GF(p)) = 2 by A2,A3,INT_3:7;
set d = 1.(GF(p))+1.(GF(p));
A5: d*x = 2*Ix mod p by A4,INT_3:def 10;
x+x =1.(GF(p))*x +x
.=1.(GF(p))*x +1.(GF(p))*x
.= 2*Ix mod p by A5,VECTSP_1:def 7; then
2*Ix mod p = 0 by A1,Th11; then
2*Ix - (2*Ix div p) * p= 0 by INT_1:def 10; then
A6: p divides 2*Ix by INT_1:def 3;
p divides Ix by A1,A6,EULER_1:13,INT_2:28,30; then
Ix = p * (Ix div p) by NAT_D:3; then
Ix - (Ix div p)*p = 0; then
A7: Ix mod p = 0;
Ix < p by NAT_1:44;
then Ix = 0 by A7,NAT_D:63;
hence x = 0.(GF(p));
end;
theorem Th28:
a <> 0 implies (a") |^n = (a|^n)"
proof
assume A1: a <> 0;
A2: p > 1 by INT_2:def 4;
consider n1 be Nat such that A3: a = n1 mod p by Th13;
consider n2 be Nat such that A4: a" = n2 mod p by Th13;
A5: a|^n = n1|^n mod p by A3,Th23;
A6: (a") |^ n = (n2|^n) mod p by A4,Th23;
A7: (n1 * n2) |^ n mod p = (n1|^n * n2|^n) mod p by NEWTON:7
.= (a|^n) * ((a") |^ n) by A5,A6,Th18;
a <> 0.GF(p) by A1,Th11;
then a" * a = 1.GF(p) by VECTSP_1:def 10
.= 1 by Th12;
then (n1*n2) mod p = 1 by A3,A4,Th18;
then (n1 * n2) |^ n mod p = 1 by A2,PEPIN:35;
then A8: ((a") |^ n) * (a|^n) = 1.GF(p) by A7;
then a|^n <> 0.GF(p);
hence thesis by A8,VECTSP_1:def 10;
end;
Lm3: a|^n1 * a|^n2 = a|^(n1+n2) by BINOM:10;
Lm4:
(a|^n1) |^ n2 = a|^(n1*n2) by BINOM:11;
registration let p;
cluster MultGroup GF(p) -> cyclic;
coherence
proof
MultGroup GF(p) is finite Subgroup of MultGroup GF(p) by GROUP_2:54;
hence thesis by GR_CY_3:38;
end;
end;
theorem Th29:
for x be Element of MultGroup GF(p), x1 be Element of GF(p),
n be Nat st x = x1 holds x|^n = x1 |^n
proof
let x be Element of MultGroup GF(p), x1 be Element of GF(p), n be Nat;
assume
A1: x = x1;
defpred P[Nat] means x|^$1 = x1 |^$1;
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
A3: x|^(n+1) = (x|^n)*x by GROUP_1:34;
A4: x1 |^(n+1) = (x1 |^n)*x1 by Th24;
assume x|^n = x1 |^n;
hence thesis by A1,A3,A4,UNIROOTS:16;
end;
x|^0 = 1_(MultGroup GF(p)) by GROUP_1:25
.= 1_GF(p) by UNIROOTS:17
.= x1 |^0 by Th21; then
A5: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th30:
ex g be Element of GF(p) st
for a be Element of GF(p) st a <> 0.GF(p) holds
ex n be Nat st a = g|^n
proof
consider g be Element of MultGroup GF(p) such that
A1: for a be Element of MultGroup GF(p)
holds ex n be Nat st a= g|^n by GR_CY_1:18;
reconsider g0=g as Element of GF(p) by UNIROOTS:19;
take g0;
now let a be Element of GF(p);
assume a <> 0.GF(p); then
A2:not a in {0.GF(p)} by TARSKI:def 1;
the carrier of GF(p) = (the carrier of MultGroup GF(p))
\/ {0.GF(p)} by UNIROOTS:15; then
reconsider a0 = a as Element of MultGroup GF(p) by A2,XBOOLE_0:def 3;
consider n be Nat such that
A3: a0= g|^n by A1;
take n;
thus a = g0|^n by A3,Th29;
end;
hence thesis;
end;
begin :: 3.Relation between Legendre symbol and the number of roots in $\bf{GF}(p)$
definition let p, a;
attr a is quadratic_residue means
a <> 0 & ex x being Element of GF(p) st x|^2 = a;
attr a is not_quadratic_residue means
a <> 0 & not ex x being Element of GF(p) st x|^2 = a;
end;
theorem Th31:
a <> 0 implies a|^2 is quadratic_residue
by Th25;
registration let p be Prime;
cluster 1.(GF p) -> quadratic_residue;
correctness
proof
A1: p > 1 by INT_2:def 4;
reconsider a = 1.GF(p) as Element of GF p;
A2: a = 1 by A1,INT_3:14;
a|^2 = (1.GF(p))*(1.GF(p)) by Lm2
.= 1_GF(p);
hence thesis by A2;
end;
end;
definition let p, a;
func Lege_p(a) -> Integer equals :Def5:
0 if a = 0,
1 if a is quadratic_residue
otherwise -1;
coherence;
consistency;
end;
theorem Th32:
a is not_quadratic_residue iff Lege_p(a) = -1
proof
hereby assume a is not_quadratic_residue;
then a <> 0 & not ex x being Element
of GF(p) st x|^2= a;
then a <> 0 & not a is quadratic_residue;
hence Lege_p(a) = -1 by Def5;
end;
assume Lege_p(a) = -1;
then a <> 0 & not a is quadratic_residue by Def5;
then a <> 0 & not ex x being Element of GF(p)
st x|^2 = a;
hence thesis;
end;
theorem Th33:
a is quadratic_residue iff Lege_p(a) = 1
by Def5;
theorem Th34:
a = 0 iff Lege_p(a) = 0
by Def5;
theorem
a <> 0 implies Lege_p(a|^2) = 1
by Th31,Th33;
theorem Th36:
Lege_p(a*b) = Lege_p(a) * Lege_p(b)
proof
per cases;
suppose A1: a is quadratic_residue;
then A2: Lege_p(a) = 1 by Th33;
per cases;
suppose A3: b is quadratic_residue;
then A4: Lege_p(b) = 1 by Th33;
A5: a <> 0 & ex x being Element of GF(p) st x|^2 = a by A1;
b <> 0 & ex x being Element of GF(p) st x|^2 = b by A3;
then A6: a*b <> 0 by A5,Th20;
ex x being Element of GF(p) st x|^2 = a*b
proof
consider a1 be Element of GF(p) such that
A7: a1|^2 = a by A1;
consider b1 be Element of GF(p) such that
A8: b1|^2 = b by A3;
(a1|^2) * (b1|^2) = (a1*b1) |^ 2 by BINOM:9;
hence thesis by A7,A8;
end;
then a*b is quadratic_residue by A6;
hence thesis by A2,A4,Th33;
end;
suppose A9: b = 0;
then Lege_p(b) = 0 by Def5;
hence thesis by A9,Th20;
end;
suppose A10: b <> 0 & not b is quadratic_residue;
then A11: Lege_p(b) = -1 by Def5;
A12: a <> 0 &
ex x being Element of GF(p) st x|^2 = a by A1;
A13: a*b <> 0 by A10,A12,Th20;
not ex x being Element of GF(p) st x|^2 = a*b
proof
given xab being Element of GF(p) such that
A14: xab|^2 = a*b;
consider xa being Element of GF(p) such that
A15: xa|^2 = a by A1;
A16: xa|^2 <> 0.GF(p) by A12,A15,Th11;
A17: xa <> 0
proof
assume xa =0; then
xa = 0.GF(p); then
xa*xa=0.GF(p); then
xa|^2 = 0.GF(p) by Lm2;
hence contradiction by A15,A12,Th11;
end;
(xa"*xab) |^2 = (xa") |^2* (a*b) by A14,BINOM:9
.=(xa") |^2* (xa|^2) *b by A15,GROUP_1:def 3
.=(xa|^2)" * (xa|^2) *b by Th28,A17
.= 1.GF(p) *b by A16,VECTSP_1:def 10
.= b;
hence contradiction by A10;
end;
then a*b is not_quadratic_residue by A13;
hence thesis by A2,A11,Th32;
end;
end;
suppose A18: not a is quadratic_residue;
now per cases;
suppose A19: a = 0;
then Lege_p(a) = 0 by Th34;
hence thesis by A19,Th20;
end;
suppose A20: a <> 0;
then A21: Lege_p(a) = -1 by A18,Def5;
per cases;
suppose A22: b is quadratic_residue;
then A23: Lege_p(b) = 1 by Th33;
A24: b <> 0 &
ex x being Element of GF(p) st x|^2 = b by A22;
then A25: a*b <> 0 by A20,Th20;
not ex x being Element of GF(p) st x|^2 = a*b
proof
given xab being Element of GF(p) such that
A26: xab|^2 = a*b;
consider xb being Element of GF(p) such that
A27: xb|^2 = b by A22;
A28: xb|^2 <> 0.GF(p) by A24,A27,Th11;
A29: xb <> 0
proof
assume xb = 0; then
xb = 0.GF(p); then
xb*xb=0.GF(p); then
xb|^2 = 0.GF(p) by Lm2;
hence contradiction by A27,A24,Th11;
end;
(xab*xb") |^2 = (a*b) * (xb") |^2 by A26,BINOM:9
.= a * ((xb|^2) *(xb") |^2) by A27,GROUP_1:def 3
.= a * ((xb|^2) * (xb|^2)" ) by Th28,A29
.= a * 1.GF(p) by A28,VECTSP_1:def 10
.= a;
hence contradiction by A18,A20;
end;
then a*b is not_quadratic_residue by A25;
hence thesis by A21,A23,Th32;
end;
suppose A30: b = 0;
then Lege_p(b) = 0 by Th34;
hence thesis by A30,Th20;
end;
suppose A31: b <> 0 & not b is quadratic_residue;
then A32: Lege_p(b) = -1 by Def5;
A33: a*b <> 0 by A20,A31,Th20;
ex x being Element of GF(p) st x|^2 = a*b
proof
consider g be Element of GF(p) such that
A34:for a be Element of GF(p) st a <> 0.GF(p)
holds ex n be Nat st a= g|^n by Th30;
a <> 0.GF(p) by A20,Th11; then
consider na be Nat such that
A35: a= g|^na by A34;
b <> 0.GF(p) by A31,Th11; then
consider nb be Nat such that
A36: b= g|^nb by A34;
A37: na = (na div 2)*2 + (na mod 2) by NAT_D:2;
A38: nb = (nb div 2)*2 + (nb mod 2) by NAT_D:2;
na mod 2 <> 0
proof
assume A39: na mod 2 = 0;
reconsider nn= (na div 2) as Element of NAT;
a = (g|^nn) |^2 by A35,A37,A39,Lm4;
hence contradiction by A18,A20;
end; then
A40: na mod 2 = 1 by NAT_D:12;
nb mod 2 <> 0
proof
assume A41: nb mod 2 = 0;
reconsider nn= (nb div 2) as Element of NAT;
b = (g|^nn) |^2 by A36,A38,A41,Lm4;
hence contradiction by A31;
end; then
A42: nb mod 2 = 1 by NAT_D:12;
reconsider nc = ((na div 2)+(nb div 2) + 1) as Nat;
A43:na+nb = ((na div 2)*2 + 1) + nb by A40,NAT_D:2
.=((na div 2)*2 + 1) + ((nb div 2)*2 + 1) by A42,NAT_D:2
.=nc * 2;
a*b =g|^(na+nb) by A35,A36,Lm3
.= (g|^nc) |^2 by A43,Lm4;
hence thesis;
end;
then a*b is quadratic_residue by A33;
hence thesis by A21,A32,Th33;
end;
end;
end;
hence thesis;
end;
end;
theorem Th37:
a <> 0 & n mod 2 = 0 implies Lege_p(a|^n) = 1
proof
assume A1: a <> 0 & n mod 2 = 0;
A2: n = (n div 2) * 2 + (n mod 2) by INT_1:59
.= (n div 2) * 2 by A1;
reconsider n1 = n div 2 as Nat;
(a|^n1) |^ 2 is quadratic_residue by A1,Th31,Th25;
then a|^n is quadratic_residue by A2,Lm4;
hence thesis by Def5;
end;
theorem
n mod 2 = 1 implies Lege_p(a|^n) = Lege_p(a)
proof
assume A1: n mod 2 = 1;
A2: n = (n div 2) * 2 + 1 by A1,INT_1:59;
reconsider n1 = n - 1 as Nat by A2;
a |^ (n1+1) = a |^ n1 * a by Th24;
then A3: Lege_p(a|^n) = Lege_p(a |^ n1) * Lege_p(a) by Th36;
per cases;
suppose a = 0;
then Lege_p(a) = 0 by Def5;
hence thesis by A3;
end;
suppose A4: a <> 0;
n-1 mod 2 = 0 + ((n div 2) * 2) mod 2 by A2
.= 0 mod 2 by NAT_D:61
.= 0 by NAT_D:26;
then Lege_p(a |^ n1) = 1 by A4,Th37;
hence thesis by A3;
end;
end;
theorem Th39:
2 < p implies card({b : b|^2 = a}) = 1 + Lege_p(a)
proof
assume A1:2 < p;
per cases;
suppose A2: a is quadratic_residue; then
consider x being Element of GF(p) such that
A3: x|^2= a;
A4: x in {b : b|^2 = a} by A3;
(-x) |^2 = (-x)*(-x) by Lm2
.=x*x by VECTSP_1:10
.=a by A3,Lm2; then
-x in {b : b|^2 = a}; then
A5: {x,-x } c= {b : b|^2 = a} by A4,ZFMISC_1:32;
A6: x <> -x
proof
assume x = -x; then
x+x = 0.(GF(p)) by VECTSP_1:16; then
A7: x = 0.(GF(p)) by A1,Th27;
x|^2 = (0.(GF(p))) * (0.(GF(p))) by A7,Lm2
.= 0.(GF(p))
.= 0 by Th11;
hence contradiction by A3,A2;
end;
now let y be object;
assume y in {b : b|^2 = a}; then
consider z be Element of GF(p) such that
A8: y=z & z|^2 = a;
z*z = z|^2 by Lm2
.=x*x by A3,A8,Lm2; then
z = x or z = -x by Th26;
hence y in {x,-x } by A8,TARSKI:def 2;
end; then
{b : b|^2 = a} c={x,-x };
hence card ({b : b|^2 = a}) = card ({x,-x }) by A5,XBOOLE_0:def 10
.= 1+1 by A6,CARD_2:57
.= 1+Lege_p(a) by A2,Def5;
end;
suppose A9: not a is quadratic_residue;
now per cases;
suppose A10: a = 0;
thus card({b : b|^2 = a})=1+Lege_p(a)
proof
now let x be object;
assume x in {b : b|^2 = a};
then consider b such that
A11: x = b & b|^2 = 0 by A10;
b = 0 by Th25,A11
.= 0.(GF(p)) by Th11;
hence x in {0.(GF(p))} by A11,TARSKI:def 1;
end; then
A12: {b : b|^2 = a} c= {0.(GF(p))};
(0.(GF(p))) |^2 = (0.(GF(p))) * (0.(GF(p))) by Lm2
.= 0.(GF(p))
.= 0 by Th11; then
0.(GF(p)) in {b : b|^2 = a} by A10; then
{0.(GF(p))} c= {b : b|^2 = a} by ZFMISC_1:31; then
{b : b|^2 = a} = {0.(GF(p))} by A12,XBOOLE_0:def 10;
hence card ({b : b|^2 = a}) = 1+0 by CARD_2:42
.= 1+ Lege_p(a) by A10,Def5;
end;
end;
suppose A13: a <> 0;
A14: {b : b|^2 = a} = {}
proof
assume {b : b|^2 = a} <> {}; then
consider x be object
such that A15: x in {b : b|^2 = a} by XBOOLE_0:def 1;
ex b st x = b & b|^2 = a by A15;
hence contradiction by A9,A13;
end;
thus card({b : b|^2 = a}) = 1 + - 1 by A14
.= 1+ Lege_p(a) by A9,A13,Def5;
end;
end;
hence card({b : b|^2 = a})=1+Lege_p(a);
end;
end;
begin :: 4.Set of points on an elliptic curve over $\bf{GF}(p)$
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
[:the carrier of K, the carrier of K, the carrier of K:] \ {[0.K,0.K,0.K]};
correctness
proof
[1.K,1.K,1.K] <> [0.K,0.K,0.K] by XTUPLE_0:3; then
not [1.K,1.K,1.K] in {[0.K,0.K,0.K]} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 5;
end;
end;
theorem Th40:
ProjCo(GF(p)) = [:the carrier of GF(p),
the carrier of GF(p), the carrier of GF(p):] \ {[0,0,0]}
proof
0.GF(p) = 0 by Th11;
hence thesis;
end;
reserve Px,Py,Pz for Element of GF(p);
definition
let p be Prime;
let a, b be Element of GF(p);
func Disc(a,b,p) -> Element of GF(p) means
for g4, g27 be Element of GF(p) st g4 = 4 mod p & g27 = 27 mod p
holds it = g4*a|^3 + g27*b|^2;
existence
proof
reconsider g40 = 4 mod p as Element of GF(p) by Th14;
reconsider g270 = 27 mod p as Element of GF(p) by Th14;
reconsider d = g40*a|^3 + g270*b|^2 as Element of GF(p);
take d;
thus thesis;
end;
uniqueness
proof
let d1,d2 be Element of GF(p);
assume
A1: for g4, g27 be Element of GF(p) st g4 = 4 mod p & g27 = 27 mod p
holds d1 = g4*a|^3 + g27*b|^2;
assume
A2: for g4, g27 be Element of GF(p) st g4 = 4 mod p & g27 = 27 mod p
holds d2 = g4*a|^3 + g27*b|^2;
reconsider g4 = 4 mod p as Element of GF(p) by Th14;
reconsider g27 = 27 mod p as Element of GF(p) by Th14;
thus d1 = g4*a|^3 + g27*b|^2 by A1
.= d2 by A2;
end;
end;
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:
for P be 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
proof
set DX = [:the carrier of GF(p),
the carrier of GF(p), the carrier of GF(p):];
deffunc F(Element of DX) = (($1`2_3) |^2)*($1`3_3)-(($1`1_3) |^3
+a*($1`1_3)*($1`3_3) |^2+b*($1`3_3) |^3);
consider f be Function of DX,the carrier of GF(p)
such that A1: for x being Element of DX holds f.x = F(x)
from FUNCT_2:sch 4;
take f;
thus thesis by A1;
end;
uniqueness
proof
set DX = [:the carrier of GF(p), the carrier of GF(p),
the carrier of GF(p):];
deffunc F(Element of DX)
=(($1`2_3) |^2)*($1`3_3)-(($1`1_3) |^3
+a*($1`1_3)*($1`3_3) |^2+b*($1`3_3) |^3);
let f,g be Function of DX,the carrier of GF(p);
assume A2: for x being Element of DX holds f.x = F(x);
assume A3: for x being Element of DX holds g.x = F(x);
now let x be Element of DX;
thus f.x = F(x) by A2
.=g.x by A3;
end;
hence f=g by FUNCT_2:def 8;
end;
end;
theorem Th41:
for X,Y,Z be 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
let X,Y,Z be Element of GF(p);
set DX = [:the carrier of GF(p),
the carrier of GF(p), the carrier of GF(p):];
reconsider P = [X,Y,Z] as Element of DX;
P`1_3 = X & P`2_3 = Y & P`3_3 = Z;
hence thesis by Def8;
end;
Lm5:[0,1,0] is Element of ProjCo(GF(p))
& EC_WEqProjCo(a,b,p).([0,1,0]) = 0.GF(p)
proof
set P = [0,1,0];
hereby P <> [0,0,0] by XTUPLE_0:3;
then A1: not P in {[0,0,0]} by TARSKI:def 1;
A2: 0 in the carrier of GF(p) by NAT_1:44;
1.GF(p) in the carrier of GF(p);
then 1 in the carrier of GF(p) by Th12;
then P in [:the carrier of GF(p),
the carrier of GF(p), the carrier of GF(p):] by A2,MCART_1:69;
then P in [:the carrier of GF(p),
the carrier of GF(p), the carrier of GF(p):] \ {[0,0,0]}
by A1,XBOOLE_0:def 5;
hence P is Element of ProjCo(GF(p)) by Th40;
end;
then reconsider P=[0,1,0] as Element of ProjCo(GF(p));
set Px = P`1_3, Py = P`2_3, Pz = P`3_3;
A6: (Px) |^3 = (Px) |^(2+1)
.= (Px) |^2 * (Px) by Th24
.= 0.GF(p);
A7: (Pz) |^3 = (Pz) |^(2+1)
.= (Pz) |^2 * (Pz) by Th24
.= 0.GF(p);
EC_WEqProjCo(a,b,p).P =
(Py |^2)*Pz-(Px |^3 +a*Px*Pz |^2+b*Pz |^3) by Def8
.= 0.GF(p) -(Px |^3 +a*Px*Pz |^2+b*Pz |^3)
.= -(0.GF(p) +a*Px*Pz |^2+b*Pz |^3) by A6,RLVECT_1:4
.= -(a*Px*Pz |^2+b*Pz |^3) by RLVECT_1:4
.= -(0.GF(p)+b*Pz |^3)
.= -(b*Pz |^3) by RLVECT_1:4
.= -(0.GF(p)) by A7
.= 0.GF(p) - (0.GF(p)) by RLVECT_1:4;
hence thesis by VECTSP_1:19;
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
{P where P is Element of ProjCo(GF(p)) : EC_WEqProjCo(a,b,p).P = 0.GF(p) };
correctness
proof
A1: now let x be object;
assume x in {P where P is Element of ProjCo(GF(p)) :
EC_WEqProjCo(a,b,p).P = 0.GF(p) }; then
ex P be Element of ProjCo(GF(p)) st
x = P & EC_WEqProjCo(a,b,p).P = 0.GF(p);
hence x in ProjCo(GF(p));
end;
reconsider D0=[0,1,0] as Element of ProjCo(GF(p)) by Lm5;
EC_WEqProjCo(a,b,p).D0 = 0.GF(p) by Lm5;
then
D0 in {P where P is Element of ProjCo(GF(p)) :
EC_WEqProjCo(a,b,p).P = 0.GF(p) };
hence thesis by A1,TARSKI:def 3;
end;
end;
Lm6:
for p be Prime, d,Y be Element of GF(p)
holds [d,Y,1] is Element of ProjCo(GF(p))
proof
let p be Prime, d,Y be Element of GF(p);
set P = [d,Y,1];
P <> [0,0,0] by XTUPLE_0:3;
then A1: not P in {[0,0,0]} by TARSKI:def 1;
1.GF(p) in the carrier of GF(p);
then 1 in the carrier of GF(p) by Th12;
then P in [:the carrier of GF(p),
the carrier of GF(p),
the carrier of GF(p):] by MCART_1:69;
then P in [:the carrier of GF(p),
the carrier of GF(p),
the carrier of GF(p):] \ {[0,0,0]} by A1,XBOOLE_0:def 5;
hence P is Element of ProjCo(GF(p)) by Th40;
end;
theorem Th42:
[0,1,0] is Element of EC_SetProjCo(a,b,p)
proof
[0,1,0] is Element of ProjCo(GF(p))
& EC_WEqProjCo(a,b,p).([0,1,0]) = 0.GF(p) by Lm5;
then [0,1,0] in {P where P is Element of ProjCo(GF(p)) :
EC_WEqProjCo(a,b,p).P = 0.GF(p)};
hence thesis;
end;
theorem Th43:
for p be Prime, a, b, X, Y be 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
let p be Prime, a, b, X, Y be Element of GF(p);
A1: 1 = 1.(GF p) by Th12;
reconsider Q=[X,Y,1] as Element of ProjCo(GF(p)) by Lm6;
A2: Y|^2 = Y|^2 * 1.(GF(p));
A3: a*X = a*X*(1.(GF(p)))
.= a*X*((1.(GF(p)))*(1.(GF(p))))
.= a*X*((1.(GF(p))) |^2) by Lm2;
A4: b = b*(1.(GF(p)))
.= b*((1.(GF(p)))*(1.(GF(p))))
.= b*((1.(GF(p))) |^2) by Lm2
.= b*(((1.(GF(p))) |^2) *(1.(GF(p))))
.= b*((1.(GF(p))) |^(2+1)) by Th24
.= b*((1.(GF(p))) |^3);
hereby
assume A5: Y|^2 = X|^3 + a*X + b;
Y|^2 - (X|^3 + a*X + b) = 0.(GF(p)) by A5,VECTSP_1:19;
then EC_WEqProjCo(a,b,p).Q = 0.(GF(p)) by A1,A2,A3,A4,Th41;
then Q in {P where P is Element of ProjCo(GF(p)) :
EC_WEqProjCo(a,b,p).P = 0.GF(p)};
hence [X,Y,1] is Element of EC_SetProjCo(a,b,p);
end;
assume [X,Y,1] is Element of EC_SetProjCo(a,b,p);
then Q in {P where P is Element of ProjCo(GF(p)) :
EC_WEqProjCo(a,b,p).P = 0.GF(p)};
then ex P be Element of ProjCo(GF(p)) st P=Q &
EC_WEqProjCo(a,b,p).P = 0.GF(p);
then Y|^2 - (X|^3 + a*X + b) = 0.(GF(p)) by A1,A2,A3,A4,Th41;
hence Y|^2 = X|^3 + a*X + b by VECTSP_1:19;
end;
definition
let p be Prime;
let P,Q be Element of ProjCo(GF(p));
pred P _EQ_ Q means :Def10:
ex a be 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
proof
for R be Element of ProjCo(GF(p)) holds
ex a be Element of GF(p) st a <> 0.GF(p)&
R`1_3 = a*(R`1_3) & R`2_3 = a*(R`2_3) & R`3_3 = a*(R`3_3)
proof
let R be Element of ProjCo(GF(p));
reconsider a = 1.(GF(p)) as Element of GF(p);
R`1_3 = a*(R`1_3) & R`2_3 = a*(R`2_3) & R`3_3 = a*(R`3_3);
hence thesis;
end;
hence thesis;
end;
symmetry
proof
thus for P,Q be Element of ProjCo(GF(p))
st ex a be 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 b be Element of GF(p) st b <> 0.GF(p)
& Q`1_3 = b*(P`1_3) & Q`2_3 = b*(P`2_3) & Q`3_3 = b*(P`3_3)
proof
let P,Q be Element of ProjCo(GF(p));
given a be Element of GF(p) such that
A1: 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);
take b=a";
A2: b <> 0.GF(p)
proof
assume b = 0.GF(p);
then b*a = 0.GF(p);
then 1.GF(p) =0.GF(p) by A1,VECTSP_1:def 10;
hence contradiction;
end;
A3: Q`1_3 = (1.(GF(p)))*(Q`1_3)
.=(b*a)*(Q`1_3) by A1,VECTSP_1:def 10
.=b*(P`1_3) by A1,GROUP_1:def 3;
A4: Q`2_3 = (1.(GF(p)))*(Q`2_3)
.=(b*a)*(Q`2_3) by A1,VECTSP_1:def 10
.=b*(P`2_3) by A1,GROUP_1:def 3;
Q`3_3 = (1.(GF(p)))*(Q`3_3)
.=(b*a)*(Q`3_3) by A1,VECTSP_1:def 10
.=b*(P`3_3) by A1,GROUP_1:def 3;
hence thesis by A2,A3,A4;
end;
end;
end;
theorem Th44:
for p be Prime, P,Q,R be Element of ProjCo(GF(p)) holds
( P _EQ_ Q & Q _EQ_ R implies P _EQ_ R)
proof
let p be Prime, P,Q,R be Element of ProjCo(GF(p));
assume A1:P _EQ_ Q & Q _EQ_ R; then
consider a be Element of GF(p) such that
A2: 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);
consider b be Element of GF(p) such that
A3: b <> 0.GF(p) & Q`1_3 = b*(R`1_3) & Q`2_3 = b*(R`2_3)
& Q`3_3 = b*(R`3_3) by A1;
take d = a*b;
thus thesis by A2,A3,GROUP_1:def 3,VECTSP_1:12;
end;
theorem Th45:
for p be Prime, a, b be Element of GF(p),
P,Q be Element of [:the carrier of GF(p), the carrier of GF(p),
the carrier of GF(p):], d be 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
let p be Prime, a, b be Element of GF(p),
P,Q be Element of [:the carrier of GF(p), the carrier of GF(p),
the carrier of GF(p):], d be Element of GF(p);
assume
A1: 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);
set DX = [:the carrier of GF(p), the carrier of GF(p),
the carrier of GF(p):];
consider PP be Element of ProjCo(GF(p)) such that
A2: P = PP & EC_WEqProjCo(a,b,p).PP = 0.GF(p) by A1;
A3: EC_WEqProjCo(a,b,p).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)
by Def8;
A4: EC_WEqProjCo(a,b,p).Q
= ((d*(P`2_3)) |^2)*(d*(P`3_3))-((d*(P`1_3)) |^3
+a*(d*(P`1_3))*(d*(P`3_3)) |^2+b*(d*(P`3_3)) |^3) by A1,Def8
.=(d|^2 * (P`2_3) |^2 )*(d*(P`3_3))-((d*(P`1_3)) |^3
+a*(d*(P`1_3))*(d*(P`3_3)) |^2+b*(d*(P`3_3)) |^3) by BINOM:9
.=(d|^2 * (P`2_3) |^2 *d)*(P`3_3)-((d*(P`1_3)) |^3
+a*(d*(P`1_3))*(d*(P`3_3)) |^2+b*(d*(P`3_3)) |^3) by GROUP_1:def 3
.=(d|^2 *d* (P`2_3) |^2 )*(P`3_3)-((d*(P`1_3)) |^3
+a*(d*(P`1_3))*(d*(P`3_3)) |^2+b*(d*(P`3_3)) |^3) by GROUP_1:def 3
.=(d|^(2+1) * (P`2_3) |^2 )*(P`3_3)-((d*(P`1_3)) |^3
+a*(d*(P`1_3))*(d*(P`3_3)) |^2+b*(d*(P`3_3)) |^3) by Th24
.=(d|^3 * (P`2_3) |^2 )*(P`3_3)-(d|^3 *(P`1_3) |^3
+a*(d*(P`1_3))*(d*(P`3_3)) |^2+b*(d*(P`3_3)) |^3) by BINOM:9
.=(d|^3 * (P`2_3) |^2 )*(P`3_3)-(d|^3 *(P`1_3) |^3
+a*(d*(P`1_3))*(d|^2*(P`3_3) |^2)+b*(d*(P`3_3)) |^3) by BINOM:9
.=(d|^3) * ((P`2_3) |^2 )*(P`3_3)-(d|^3 *(P`1_3) |^3
+(a*(d*(P`1_3))*(d|^2))*(P`3_3) |^2+b*(d*(P`3_3)) |^3) by GROUP_1:def 3
.=(d|^3) * ((P`2_3) |^2 )*(P`3_3)-(d|^3 *(P`1_3) |^3
+(a*(d*(P`1_3)*(d|^2)))*(P`3_3) |^2+b*(d*(P`3_3)) |^3) by GROUP_1:def 3
.=(d|^3) * ((P`2_3) |^2 )*(P`3_3)-(d|^3 *(P`1_3) |^3
+(a*((d|^2)*d*(P`1_3)))*(P`3_3) |^2+b*(d*(P`3_3)) |^3) by GROUP_1:def 3
.=(d|^3) * ((P`2_3) |^2 )*(P`3_3)-(d|^3 *(P`1_3) |^3
+(a*(d|^(2+1)*(P`1_3)))*(P`3_3) |^2+b*(d*(P`3_3)) |^3) by Th24
.=(d|^3) * ((P`2_3) |^2 )*(P`3_3)-((d|^3) *(P`1_3) |^3
+(d|^3)*(a*(P`1_3))*(P`3_3) |^2+b*(d*(P`3_3)) |^3) by GROUP_1:def 3
.=(d|^3) * ((P`2_3) |^2 )*(P`3_3)-((d|^3) *(P`1_3) |^3
+(d|^3)*(a*(P`1_3))*(P`3_3) |^2+b*(d|^3*(P`3_3) |^3)) by BINOM:9
.=(d|^3) * ((P`2_3) |^2 )*(P`3_3)-((d|^3) *(P`1_3) |^3
+(d|^3)*(a*(P`1_3))*(P`3_3) |^2+(d|^3)*b*(P`3_3) |^3) by GROUP_1:def 3
.=(d|^3) * (((P`2_3) |^2 )*(P`3_3))-((d|^3) *(P`1_3) |^3
+(d|^3)*(a*(P`1_3))*(P`3_3) |^2+(d|^3)*b*(P`3_3) |^3) by GROUP_1:def 3
.=(d|^3) * (((P`2_3) |^2 )*(P`3_3))-((d|^3) *(P`1_3) |^3
+(d|^3)*((a*(P`1_3))*(P`3_3) |^2)+(d|^3)*b*(P`3_3) |^3) by GROUP_1:def 3
.=(d|^3) * (((P`2_3) |^2 )*(P`3_3))-((d|^3) *(P`1_3) |^3
+(d|^3)*((a*(P`1_3))*(P`3_3) |^2)+(d|^3)*(b*(P`3_3) |^3)) by GROUP_1:def 3
.=(d|^3) * (((P`2_3) |^2 )*(P`3_3))-((d|^3) *((P`1_3) |^3
+a*(P`1_3)*(P`3_3) |^2)+(d|^3)*(b*(P`3_3) |^3)) by VECTSP_1:def 7
.=(d|^3) * (((P`2_3) |^2 )*(P`3_3))
-(d|^3) * ((P`1_3) |^3 +a*(P`1_3)*(P`3_3) |^2+b*(P`3_3) |^3) by
VECTSP_1:def 7
.= d|^3*(((P`2_3) |^2)*(P`3_3)-((P`1_3) |^3
+a*(P`1_3)*(P`3_3) |^2+b*(P`3_3) |^3)) by VECTSP_1:11
.= 0.GF(p) by A2,A3;
PP in ProjCo(GF(p)); then
PP in [:the carrier of GF(p), the carrier of GF(p),
the carrier of GF(p):] \ {[0,0,0]} by Th40; then
not P in {[0,0,0]} by A2,XBOOLE_0:def 5; then
P`1_3 <> 0 or P`2_3 <> 0 or P`3_3 <> 0 by TARSKI:def 1; then
P`1_3 <> 0.GF(p) or P`2_3 <> 0.GF(p) or P`3_3 <> 0.GF(p) by Th11; then
d*(P`1_3) <> 0.GF(p) or d*(P`2_3) <> 0.GF(p) or d*(P`3_3) <> 0.GF(p)
by A1,VECTSP_1:12; then
Q`1_3 <> 0 or Q`2_3 <> 0 or Q`3_3 <> 0 by A1; then
[Q`1_3,Q`2_3,Q`3_3] <> [0,0,0] by XTUPLE_0:3; then
not Q in {[0,0,0]} by TARSKI:def 1; then
Q in [:the carrier of GF(p), the carrier of GF(p),
the carrier of GF(p):] \ {[0,0,0]} by XBOOLE_0:def 5; then
Q in ProjCo(GF(p)) by Th40;
hence thesis by A4;
end;
definition
let p be Prime;
func R_ProjCo p -> Relation of ProjCo(GF(p)) equals
{[P,Q] where P,Q is Element of ProjCo(GF(p)) : P _EQ_ Q};
correctness
proof
set RX = {[P,Q] where P,Q is Element of ProjCo(GF(p)) : P _EQ_ Q};
now let x be object;
assume x in RX; then
consider P,Q be Element of ProjCo(GF(p)) such that
A1: x = [P,Q] & P _EQ_ Q;
thus x in [:ProjCo(GF(p)),ProjCo(GF(p)):] by A1;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th46:
for p be Prime, P,Q be Element of ProjCo(GF(p)) holds
P _EQ_ Q iff [P,Q] in R_ProjCo p
proof
let p be Prime, P,Q be Element of ProjCo(GF(p));
thus P _EQ_ Q implies [P,Q] in R_ProjCo p;
assume [P,Q] in R_ProjCo p; then
consider X0,Y0 be Element of ProjCo(GF(p)) such that
A1: [P,Q] = [X0,Y0] & X0 _EQ_ Y0;
P=X0 & Q=Y0 by A1,XTUPLE_0:1;
hence P _EQ_ Q by A1;
end;
registration let p be Prime;
cluster R_ProjCo p -> total symmetric transitive;
coherence
proof
set R = R_ProjCo p;
for x be object holds
x in ProjCo(GF(p)) iff ex y be object st [x,y] in R
proof
let x be object;
hereby assume x in ProjCo(GF(p)); then
reconsider X =x as Element of ProjCo(GF(p));
X _EQ_ X;
then [x,x] in R;
hence ex y be object st [x,y] in R;
end;
given y be object such that
A1: [x,y] in R;
consider X,Y be Element of ProjCo(GF(p)) such that
A2: [x,y] = [X,Y] & X _EQ_ Y by A1;
x=X by A2,XTUPLE_0:1;
hence x in ProjCo(GF(p));
end; then
dom R = ProjCo(GF(p)) by XTUPLE_0:def 12;
hence R is total by PARTFUN1:def 2;
for x,y be object holds
(x in field R & y in field R & [x,y] in R implies [ y,x] in R)
proof
let x,y be object;
assume x in field R & y in field R & [x,y] in R;
then consider X,Y be Element of ProjCo(GF(p)) such that
A3: [x,y] = [X,Y] & X _EQ_ Y;
x=X & y=Y by A3,XTUPLE_0:1;
hence [y,x] in R by A3;
end; then
R is_symmetric_in field R by RELAT_2:def 3;
hence R is symmetric by RELAT_2:def 11;
for x,y,z be object holds
(x in field R & y in field R & z in field R
& [x,y] in R & [y,z] in R implies [x,z] in R)
proof
let x,y,z be object;
assume A4: x in field R & y in field R & z in field R
& [x,y] in R & [y,z] in R; then
consider X,Y be Element of ProjCo(GF(p)) such that
A5: [x,y] = [X,Y] & X _EQ_ Y;
A6: x=X & y=Y by A5,XTUPLE_0:1;
consider Y1,Z be Element of ProjCo(GF(p)) such that
A7: [y,z] = [Y1,Z] & Y1 _EQ_ Z by A4;
X _EQ_ Y & Y _EQ_ Z by A5,A6,A7,XTUPLE_0:1; then
A8: X _EQ_ Z by Th44;
[x,z] = [X,Z] by A6,A7,XTUPLE_0:1;
hence [x,z] in R by A8;
end; then
R is_transitive_in field R by RELAT_2:def 8;
hence R is transitive by RELAT_2:def 16;
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
(R_ProjCo p) /\ nabla EC_SetProjCo(a,b,p);
correctness
proof
set P = R_ProjCo p;
set R = nabla EC_SetProjCo(a,b,p);
reconsider PR = (P /\ R) as Relation of EC_SetProjCo(a,b,p);
for x be object holds
x in EC_SetProjCo(a,b,p) iff ex y be object st [x,y] in PR
proof
let x be object;
hereby assume A1:x in EC_SetProjCo(a,b,p); then
reconsider X =x as Element of ProjCo(GF(p));
X _EQ_ X; then
A2: [x,x] in P;
[x,x] in [:EC_SetProjCo(a,b,p),EC_SetProjCo(a,b,p):]
by A1,ZFMISC_1:87;
then [x,x] in PR by A2,XBOOLE_0:def 4;
hence ex y be object st [x,y] in PR;
end;
thus thesis by ZFMISC_1:87;
end; then
dom PR = EC_SetProjCo(a,b,p) by XTUPLE_0:def 12;
hence thesis by PARTFUN1:def 2;
end;
end;
theorem Th47:
for p be Prime, a, b be Element of GF(p),
P,Q be 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
let p be Prime, a, b be Element of GF(p),
P,Q be Element of ProjCo(GF(p));
assume A1: Disc(a,b,p) <> 0.GF(p)
& P in EC_SetProjCo(a,b,p) & Q in EC_SetProjCo(a,b,p);
hereby assume P _EQ_ Q; then
A2: [P,Q] in R_ProjCo p;
[P,Q] in [:EC_SetProjCo(a,b,p),EC_SetProjCo(a,b,p):]
by A1,ZFMISC_1:87;
hence [P,Q] in R_EllCur (a,b,p) by A2,XBOOLE_0:def 4;
end;
assume [P,Q] in R_EllCur (a,b,p); then
[P,Q] in (R_ProjCo p) by XBOOLE_0:def 4;
hence P _EQ_ Q by Th46;
end;
theorem Th48:
for p be Prime, a, b be Element of GF(p),
P be 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 be Element of ProjCo(GF(p)) st Q in EC_SetProjCo(a,b,p)
& Q _EQ_ P & Q`3_3 = 1
proof
let p be Prime, a, b be Element of GF(p), P be Element of ProjCo(GF(p));
assume
A1: p > 3 & Disc(a,b,p) <> 0.GF(p) &
P in EC_SetProjCo(a,b,p) & P`3_3 <> 0;
set d=(P`3_3)";
A2: P`3_3 <> 0.GF(p) by A1,Th11;
A3: d <> 0.GF(p)
proof
assume A4: d = 0.GF(p);
A5: d*(P`3_3) = 1_GF(p) by A2,VECTSP_1:def 10
.=1 by Th12;
d*(P`3_3) = 0.GF(p) by A4
.= 0 by Th11;
hence contradiction by A5;
end;
reconsider Q =[d*(P`1_3),d*(P`2_3),d*(P`3_3)] as Element of
[:the carrier of GF(p), the carrier of GF(p), the carrier of GF(p):];
A6: Q`1_3 = d*(P`1_3) & Q`2_3 = d*(P`2_3) & Q`3_3 = d*(P`3_3);
then
Q in EC_SetProjCo(a,b,p) by A1,A3,Th45; then
consider PP be Element of ProjCo(GF(p)) such that
A7: Q = PP & EC_WEqProjCo(a,b,p).PP = 0.GF(p);
reconsider Q as Element of ProjCo(GF(p)) by A7;
take Q;
thus Q in EC_SetProjCo(a,b,p) by A6,A1,A3,Th45;
thus Q _EQ_ P by A3;
thus Q`3_3 = d*(P`3_3)
.= 1_GF(p) by A2,VECTSP_1:def 10
.= 1 by Th12;
end;
theorem Th49:
for p be Prime, a, b be Element of GF(p),
P be 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 be 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
let p be Prime, a, b be Element of GF(p),
P be Element of ProjCo(GF(p));
assume
A1: p > 3 & Disc(a,b,p) <> 0.GF(p) &
P in EC_SetProjCo(a,b,p) & P`3_3 = 0;
A2: P`3_3 = 0.GF(p) by A1;
set d=(P`2_3)";
A3: ex X0 be Element of ProjCo(GF(p))
st P=X0 & EC_WEqProjCo(a,b,p).X0 = 0.GF(p) by A1;
A4: (P`3_3) |^3 = (P`3_3) |^(2+1)
.= (P`3_3) |^2 * (P`3_3) by Th24
.= 0.GF(p) by A2;
A5: (P`3_3) |^2 = (P`3_3) |^(1+1)
.= (P`3_3) |^1 * (P`3_3) by Th24
.= 0.GF(p) by A2;
0.GF(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) by A3,Def8
.= 0.GF(p)-((P`1_3) |^3
+a*(P`1_3)*(P`3_3) |^2+b*(P`3_3) |^3) by A2
.= 0.GF(p)-((P`1_3) |^3 +0.GF(p)+b*(P`3_3) |^3) by A5
.= 0.GF(p)-((P`1_3) |^3 +0.GF(p)+0.GF(p)) by A4
.= 0.GF(p)-((P`1_3) |^3 +0.GF(p)) by RLVECT_1:4
.= 0.GF(p)-(P`1_3) |^3 by RLVECT_1:4
.= - (P`1_3) |^3 by RLVECT_1:14; then
A6: (P`1_3) |^3 = (P`1_3) |^3 + - (P`1_3) |^3 by RLVECT_1:4;
A7:P`1_3 = 0.GF(p)
proof
assume A8: P`1_3 <> 0.GF(p); then
P`1_3 * (P`1_3) <> 0.GF(p) by VECTSP_1:12; then
(P`1_3) |^1 * (P`1_3) <> 0.GF(p) by Lm1; then
(P`1_3) |^(1+1) <> 0.GF(p) by Th24; then
(P`1_3) |^2 * (P`1_3) <> 0.GF(p) by A8,VECTSP_1:12; then
(P`1_3) |^(2+1) <> 0.GF(p) by Th24;
hence contradiction by A6,RLVECT_1:5;
end;
A9: P`2_3 <> 0.GF(p)
proof
assume P`2_3 = 0.GF(p); then
P`2_3 = 0 by Th11; then
[P`1_3,P`2_3,P`3_3] = [0,0,0] by A1,A7; then
P = [0,0,0] by AA; then
P in {[0,0,0]} by TARSKI:def 1; then
not P in [:the carrier of GF(p), the carrier of GF(p),
the carrier of GF(p):] \ {[0,0,0]} by XBOOLE_0:def 5;
then not P in ProjCo(GF(p)) by Th40;
hence contradiction;
end;
A10: d <> 0.GF(p)
proof
assume A11: d = 0.GF(p);
A12: d*(P`2_3) = 1_GF(p) by A9,VECTSP_1:def 10
.=1 by Th12;
d*(P`2_3) = 0.GF(p) by A11
.= 0 by Th11;
hence contradiction by A12;
end;
reconsider Q =[d*(P`1_3),d*(P`2_3),d*(P`3_3)] as Element of
[:the carrier of GF(p), the carrier of GF(p), the carrier of GF(p):];
A13: Q`1_3 = d*(P`1_3) & Q`2_3 = d*(P`2_3) & Q`3_3 = d*(P`3_3);
then
Q in EC_SetProjCo(a,b,p) by A1,A10,Th45; then
consider PP be Element of ProjCo(GF(p)) such that
A14: Q = PP & EC_WEqProjCo(a,b,p).PP = 0.GF(p);
reconsider Q as Element of ProjCo(GF(p)) by A14;
take Q;
thus Q in EC_SetProjCo(a,b,p) by A13,A1,A10,Th45;
thus Q _EQ_ P by A10;
thus Q`1_3 = d*(P`1_3)
.=0.GF(p) by A7
.=0 by Th11;
thus Q`2_3 = d*(P`2_3)
.= 1_GF(p) by A9,VECTSP_1:def 10
.= 1 by Th12;
thus Q`3_3 = d*(P`3_3)
.=0.GF(p) by A2
.=0 by Th11;
end;
theorem Th50:
for p be Prime, a, b be Element of GF(p), x be set st
p > 3 & Disc(a,b,p) <> 0.GF(p)
& x in Class (R_EllCur(a,b,p)) holds
( ex P be Element of ProjCo(GF(p)) st P in EC_SetProjCo(a,b,p) & P=[0,1,0]
& x = Class(R_EllCur(a,b,p),P) ) or
ex P be Element of ProjCo(GF(p)), X,Y be 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
let p be Prime, a, b be Element of GF(p), x be set;
assume A1: p > 3 & Disc(a,b,p) <> 0.GF(p)
& x in Class (R_EllCur(a,b,p)); then
consider y0 be Element of EC_SetProjCo(a,b,p) such that
A2: x = Class(R_EllCur(a,b,p),y0) by EQREL_1:36;
reconsider w=y0 as Element of ProjCo(GF(p));
per cases;
suppose w`3_3 = 0; then
consider y be Element of ProjCo(GF(p)) such that
A3: y in EC_SetProjCo(a,b,p) & y _EQ_ w
& y`1_3 = 0 & y`2_3= 1 & y`3_3= 0 by A1,Th49;
[y,w] in R_EllCur(a,b,p) by A1,Th47,A3; then
x = Class(R_EllCur(a,b,p),y) by A2,A3,EQREL_1:35;
hence thesis by A3,AA;
end;
suppose w`3_3 <> 0; then
consider y be Element of ProjCo(GF(p)) such that
A4: y in EC_SetProjCo(a,b,p) & y _EQ_ w & y`3_3 = 1 by A1,Th48;
set e=y`1_3;
set f=y`2_3;
A5: y = [e,f,1] by A4,AA;
[y,w] in R_EllCur(a,b,p) by A1,Th47,A4; then
x = Class(R_EllCur(a,b,p),y) by A2,A4,EQREL_1:35;
hence thesis by A5,A4;
end;
end;
theorem Th51:
for p be Prime, a, b be 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 be Element of GF(p) st P=[X,Y,1]}
proof
let p be Prime, a, b be Element of GF(p);
assume
A1: p > 3 & Disc(a,b,p) <> 0.GF(p);
set A = Class (R_EllCur(a,b,p));
set B = {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 be Element of GF(p) st P=[X,Y,1]};
reconsider d0=[0,1,0] as Element of EC_SetProjCo(a,b,p) by Th42;
for x be object holds x in A iff x in B
proof
let x be object;
hereby assume x in A; then
( ex y be Element of ProjCo(GF(p))
st y in EC_SetProjCo(a,b,p) & y=[0,1,0]
& x = Class(R_EllCur(a,b,p),y) ) or
ex y be Element of ProjCo(GF(p)), e,f be Element of GF(p)
st y in EC_SetProjCo(a,b,p) & y=[e,f,1]
& x = Class(R_EllCur(a,b,p),y) by A1,Th50; then
x in {Class(R_EllCur(a,b,p),[0,1,0])} or
x in {Class(R_EllCur(a,b,p),y)
where y is Element of ProjCo(GF(p)): y in EC_SetProjCo(a,b,p) &
ex e,f be Element of GF(p) st y=[e,f,1]} by TARSKI:def 1;
hence x in B by XBOOLE_0:def 3;
end;
assume x in B; then
A2: x in {Class(R_EllCur(a,b,p),[0,1,0])} or
x in {Class(R_EllCur(a,b,p),y) where y is Element of ProjCo(GF(p)):
y in EC_SetProjCo(a,b,p) & ex e,f be Element of GF(p)
st y=[e,f,1]} by XBOOLE_0:def 3;
now per cases by A2,TARSKI:def 1;
suppose A3: x = Class(R_EllCur(a,b,p),[0,1,0]);
EqClass(R_EllCur(a,b,p),d0) is Element of A;
hence x in A by A3;
end;
suppose
ex y be Element of ProjCo(GF(p))
st x = Class(R_EllCur(a,b,p),y) & y in EC_SetProjCo(a,b,p)
& ex e,f be Element of GF(p) st y=[e,f,1];
then consider y be Element of ProjCo(GF(p)) such that
A4: x = Class(R_EllCur(a,b,p),y)
& y in EC_SetProjCo(a,b,p)
& ex e,f be Element of GF(p) st y=[e,f,1];
reconsider y as Element of EC_SetProjCo(a,b,p) by A4;
EqClass(R_EllCur(a,b,p),y) is Element of A;
hence x in A by A4;
end;
end;
hence x in A;
end;
hence thesis by TARSKI:2;
end;
theorem Th52:
for p be Prime,
a, b,d1,Y1,d2,Y2 be 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
let p be Prime, a, b,d1,Y1,d2,Y2 be Element of GF(p);
assume
A1: 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);
hereby assume
Class(R_EllCur(a,b,p),[d1,Y1,1])
= Class(R_EllCur(a,b,p),[d2,Y2,1]); then
[d2,Y2,1] in Class(R_EllCur(a,b,p),[d1,Y1,1]) by A1,EQREL_1:23; then
A2: [[d1,Y1,1],[d2,Y2,1]] in R_EllCur(a,b,p) by EQREL_1:18;
reconsider P=[d1,Y1,1], Q=[d2,Y2,1] as Element of ProjCo(GF(p)) by A1;
P _EQ_ Q by Th47,A1,A2; then
consider a be Element of GF(p) such that
A3: 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)
by Def10;
A4: p > 1 by INT_2:def 4;
A5: 1.GF(p)= 1 by A4,INT_3:14
.=P`3_3;
A6: 1.GF(p)= 1 by A4,INT_3:14
.=a*(P`3_3) by A3
.=a by A5;
thus d2 = a*(P`1_3) by A3
.= P`1_3 by A6
.= d1;
thus Y2 = a*(P`2_3) by A3
.= P`2_3 by A6
.=Y1;
end;
assume d1=d2 & Y1=Y2;
hence thesis;
end;
theorem Th53:
for p be Prime, a, b be Element of GF(p),
F1,F2 be 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 be Element of GF(p) st P=[X,Y,1]} holds F1 misses F2
proof
let p be Prime, a, b be Element of GF(p), F1,F2 be set;
assume A1: 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 be Element of GF(p) st P=[X,Y,1]};
assume F1 meets F2; then
F1 /\ F2 <> {} by XBOOLE_0:def 7; then
consider z be object such that A2: z in F1 /\ F2 by XBOOLE_0:def 1;
A3: z in F1 & z in F2 by A2,XBOOLE_0:def 4;
consider P be Element of ProjCo(GF(p)) such that
A4:z=Class(R_EllCur(a,b,p),P) & P in EC_SetProjCo(a,b,p) &
ex X,Y be Element of GF(p) st P=[X,Y,1] by A1,A3;
consider X1,Y1 be Element of GF(p) such that
A5: P=[X1,Y1,1] by A4;
A6: z= Class(R_EllCur(a,b,p),[0,1,0]) by A1,A3,TARSKI:def 1;
reconsider Q=[0,1,0] as Element of ProjCo(GF(p)) by Lm5;
A7: Q is Element of EC_SetProjCo(a,b,p) by Th42;
Q in Class(R_EllCur(a,b,p),P) by A4,A6,EQREL_1:23;
then [P,Q] in R_EllCur(a,b,p) by EQREL_1:18;
then P _EQ_ Q by Th47,A1,A7,A4;
then consider a be Element of GF(p) such that
A8: 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) by Def10;
A9: p > 1 by INT_2:def 4;
A10: 1.GF(p)= 1 by A9,INT_3:14
.=P`3_3 by A5;
0.GF(p)= 0 by Th11
.=a*(P`3_3) by A8
.=a by A10;
hence contradiction by A8;
end;
theorem Th54:
for X be non empty finite set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function, i be set st i in dom S holds
S.i is finite Subset of X
proof
let X be non empty finite set,
R be Equivalence_Relation of X, S be Class(R)-valued Function,
i be set;
assume i in dom S; then
S.i in Class(R) by FUNCT_1:102;
hence thesis;
end;
theorem Th55:
for X be non empty set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function st S is one-to-one
holds S is disjoint_valued
proof
let X be non empty set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function;
assume A1:S is one-to-one;
now let x,y be object;
assume
A2: x <> y;
per cases;
suppose
A3: x in dom S & y in dom S; then
A4: S.x <> S.y by A1,A2,FUNCT_1:def 4;
S.x in Class(R) & S.y in Class(R) by A3,FUNCT_1:102;
hence S.x misses S.y by A4,EQREL_1:def 4;
end;
suppose
not (x in dom S & y in dom S);
then S.x = {} or S.y = {} by FUNCT_1:def 2;
hence S.x misses S.y by XBOOLE_1:65;
end;
end;
hence thesis by PROB_2:def 2;
end;
theorem Th56:
for X be non empty set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function st S is onto
holds Union S = X
proof
let X be non empty set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function;
assume A1:S is onto;
union (Class R) = X by EQREL_1:def 4;
hence thesis by A1,FUNCT_2:def 3;
end;
theorem
for X be non empty finite set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function,
L be FinSequence of NAT
st S is one-to-one onto & dom S = dom L
& (for i be Nat st i in dom S holds L.i = card (S.i))
holds card (X) = Sum L
proof
let X be non empty finite set,
R be Equivalence_Relation of X,
S be Class(R)-valued Function,
L be FinSequence of NAT;
assume
A1: S is one-to-one onto &
dom S = dom L & (for i be Nat st i in dom S holds L.i = card (S.i));
A2: S is disjoint_valued by A1,Th55;
A3: for i be Nat st i in dom S holds
S.i is finite & L.i = card (S.i) by A1,Th54;
Union S = X by Th56,A1;
hence thesis by A1,A2,A3,DIST_1:17;
end;
theorem Th58:
for p be Prime, a, b,d be Element of GF(p), F,G be 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 be Function of F,G st I is onto & I is one-to-one
proof
let p be Prime, a, b,d be Element of GF(p), F,G be set;
assume A1:
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,P,1]) where P is Element of GF(p)
: [d,P,1] in EC_SetProjCo(a,b,p) };
consider z be object such that
A2: z in F by A1,XBOOLE_0:def 1;
consider W be Element of GF(p)
such that A3: z=W & W|^2= d|^3 + a*d + b by A1,A2;
[d,W,1] is Element of EC_SetProjCo(a,b,p) by A3,Th43; then
A4: Class(R_EllCur(a,b,p),[d,W,1]) in G by A1;
deffunc FG(object) = Class(R_EllCur(a,b,p),[d,$1,1]);
A5: for x be object st x in F holds FG(x) in G
proof
let x be object;
assume x in F; then
consider Y be Element of GF(p)
such that A6:x=Y & Y|^2= d|^3 + a*d + b by A1;
[d,Y,1] is Element of EC_SetProjCo(a,b,p) by A6,Th43;
hence FG(x) in G by A1,A6;
end;
consider I be Function of F,G such that
A7: for x be object st x in F holds I.x = FG(x) from FUNCT_2:sch 2(A5);
take I;
now let y be object;
assume y in G; then
consider P be Element of GF(p)
such that A8: y= Class(R_EllCur(a,b,p),[d,P,1])
& [d,P,1] in EC_SetProjCo(a,b,p) by A1;
P|^2= d|^3 + a*d + b by A8,Th43; then
A9: P in F by A1; then
y=I.P by A7,A8;
hence y in rng I by A9,A4,FUNCT_2:112;
end; then
G c= rng I; then
G = rng I by XBOOLE_0:def 10;
hence I is onto by FUNCT_2:def 3;
now let x1,x2 be object
such that A10: x1 in dom I & x2 in dom I & I.x1 = I.x2;
A11: x1 in F & x2 in F by A10; then
consider Y1 be Element of GF(p)
such that A12:x1=Y1 & Y1|^2= d|^3 + a*d + b by A1;
consider Y2 be Element of GF(p)
such that A13:x2=Y2 & Y2|^2= d|^3 + a*d + b by A1,A11;
A14: I.x1 = Class(R_EllCur(a,b,p),[d,x1,1]) by A10,A7;
A15: Class(R_EllCur(a,b,p),[d,x1,1])
= Class(R_EllCur(a,b,p),[d,x2,1]) by A10,A7,A14;
A16: [d,Y2,1] is Element of EC_SetProjCo(a,b,p) by Th43,A13;
[d,Y1,1] is Element of EC_SetProjCo(a,b,p) by Th43,A12;
hence x1=x2 by A1,A12,A13,A15,A16,Th52;
end;
hence I is one-to-one by FUNCT_1:def 4;
end;
theorem Th59:
for p be Prime, a, b, d be 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
let p be Prime, a,b,d be Element of GF(p);
assume
A1: p > 3 & Disc(a,b,p) <> 0.GF(p);
set F = {Y where Y is Element of GF(p) : Y|^2= d|^3 + a*d + b};
set 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) };
per cases;
suppose A2: F = {};
A3: G ={}
proof
assume G <> {}; then
consider z be object such that
A4: z in G by XBOOLE_0:def 1;
consider Y be Element of GF(p) such that
A5: z= Class(R_EllCur(a,b,p),[d,Y,1])
& [d,Y,1] in EC_SetProjCo(a,b,p) by A4;
Y|^2= d|^3 + a*d + b by A5,Th43;
then Y in F;
hence contradiction by A2;
end;
2 < p by A1,XXREAL_0:2;
hence thesis by A3,A2,Th39;
end;
suppose A6: F <> {};
then consider z be object such that A7: z in F by XBOOLE_0:def 1;
consider W be Element of GF(p)
such that A8: z=W & W|^2= d|^3 + a*d + b by A7;
[d,W,1] is Element of EC_SetProjCo(a,b,p) by A8,Th43; then
A9: Class(R_EllCur(a,b,p),[d,W,1]) in G;
consider I be Function of F,G such that
A10: I is onto & I is one-to-one by A1,A6,Th58;
A11: dom I = F by A9,FUNCT_2:def 1;
A12: rng I = G by A10,FUNCT_2:def 3; then
A13: card F c= card G by A10,A11,CARD_1:10;
reconsider h=I" as Function of G,F by A10,A12,FUNCT_2:25;
I"*I = id F & I*I" = id G by A10,A12,A9,FUNCT_2:29; then
A14: h is onto & h is one-to-one by FUNCT_2:23; then
A15:rng h = F by FUNCT_2:def 3;
dom h = G by A6,FUNCT_2:def 1; then
card G c= card F by A14,A15,CARD_1:10; then
A16: card F = card G by A13,XBOOLE_0:def 10;
2 < p by A1,XXREAL_0:2;
hence thesis by A16,Th39;
end;
end;
Lm7:
for p be Prime, n be Nat st n in Seg p holds n-1 is Element of GF(p)
proof
let p be Prime, n be Nat;
assume n in Seg p;
then 1<=n & n<= p by FINSEQ_1:1; then
A1:1-1 <=n-1 & n-1 <=p-1 by XREAL_1:9; then
A2: n-1 is Element of NAT by INT_1:3;
p-1 < p-0 by XREAL_1:15;
then n-1 < p by A1,XXREAL_0:2;
hence thesis by A2,NAT_1:44;
end;
Lm8:
for p be Prime, a, b, c, d be Element of GF(p)
st p > 3 & Disc(a,b,p) <> 0.GF(p) holds
ex S be Function st dom S = Seg p &
(for n be 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 be 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 be Element of GF(p) st P=[X,Y,1]}
proof
let p be Prime, a, b, c, d be Element of GF(p);
assume A1: p > 3 & Disc(a,b,p) <> 0.GF(p);
deffunc F(Nat) = {Class(R_EllCur(a,b,p),[($1-1),Y,1])
where Y is Element of GF(p) : [($1-1),Y,1] in EC_SetProjCo(a,b,p) };
consider S be FinSequence such that
A2: len S = p &
for i be Nat st i in dom S holds S.i = F(i) from FINSEQ_1:sch 2;
take S;
thus A3: dom S = Seg p by A2,FINSEQ_1:def 3;
thus for n be 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) } by A2;
now let x,y be object;
assume
A4: x <> y;
per cases;
suppose
A5: x in dom S & y in dom S; then
reconsider n=x,m=y as Nat;
x in Seg p & y in Seg p by A5,A2,FINSEQ_1:def 3; then
A6: n-1 is Element of GF(p) & m-1 is Element of GF(p) by Lm7;
A7: 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) } by A5,A2;
A8: S.m= {Class(R_EllCur(a,b,p),[(m-1),Y,1])
where Y is Element of GF(p) :
[(m-1),Y,1] in EC_SetProjCo(a,b,p) } by A5,A2;
thus S.x misses S.y
proof
assume S.x meets S.y;
then consider z be object such that
A9: z in S.x & z in S.y by XBOOLE_0:3;
consider Yx be Element of GF(p) such that
A10: z = Class(R_EllCur(a,b,p),[(n-1),Yx,1])
& [(n-1),Yx,1] in EC_SetProjCo(a,b,p) by A7,A9;
consider Yy be Element of GF(p) such that
A11: z = Class(R_EllCur(a,b,p),[(m-1),Yy,1])
& [(m-1),Yy,1] in EC_SetProjCo(a,b,p) by A8,A9;
n-1 = m-1 by Th52,A1,A10,A11,A6;
hence contradiction by A4;
end;
end;
suppose
not (x in dom S & y in dom S);
then S.x = {} or S.y = {} by FUNCT_1:def 2;
hence S.x misses S.y by XBOOLE_1:65;
end;
end;
hence S is disjoint_valued by PROB_2:def 2;
thus for n be Nat st n in dom S holds S.n is finite
proof
let n be Nat;
assume A12: n in dom S; then
A13: 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) } by A2;
1<=n & n<= p by A12,A3,FINSEQ_1:1; then
A14: 1-1 <=n-1 & n-1 <=p-1 by XREAL_1:9; then
A15: n-1 is Element of NAT by INT_1:3;
p-1 < p-0 by XREAL_1:15; then
n-1 < p by A14,XXREAL_0:2; then
reconsider d=n-1 as Element of GF(p) by A15,NAT_1:44;
A16: card (S.n) = 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) }) by A13
.= 1 + Lege_p(d|^3 + a*d + b) by Th59,A1;
0 <= 1 + Lege_p(d|^3 + a*d + b)
proof
per cases;
suppose not (d|^3 + a*d + b = 0 or d|^3 + a*d + b is quadratic_residue);
then Lege_p(d|^3 + a*d + b) = -1 by Def5;
hence 0<= 1 + Lege_p(d|^3 + a*d + b);
end;
suppose A17: d|^3 + a*d + b = 0
or d|^3 + a*d + b is quadratic_residue;
now per cases by A17;
suppose d|^3 + a*d + b = 0;
then Lege_p(d|^3 + a*d + b) = 0 by Def5;
hence 0<= 1 + Lege_p(d|^3 + a*d + b);
end;
suppose d|^3 + a*d + b is quadratic_residue;
then Lege_p(d|^3 + a*d + b) = 1 by Def5;
hence 0<= 1 + Lege_p(d|^3 + a*d + b);
end;
end;
hence 0<= 1 + Lege_p(d|^3 + a*d + b);
end;
end; then
card (S.n) in NAT by A16,INT_1:3;
hence S.n is finite;
end;
set B={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 be Element of GF(p) st P=[X,Y,1]};
for x be object holds x in union rng S iff x in B
proof
let x be object;
hereby assume x in union rng S; then
consider Z be set such that A18:
x in Z & Z in rng S by TARSKI:def 4;
consider n be object such that A19:
n in dom S & Z = S.n by A18,FUNCT_1:def 3;
reconsider n as Nat by A19;
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) } by A19,A2; then
consider Y be Element of GF(p) such that
A20: x = Class(R_EllCur(a,b,p),[(n-1),Y,1])
& [(n-1),Y,1] in EC_SetProjCo(a,b,p) by A18,A19;
n-1 is Element of GF(p) by A3,A19,Lm7;
hence x in B by A20;
end;
assume x in B;
then consider P be Element of ProjCo(GF(p)) such that
A21: x = Class(R_EllCur(a,b,p),P) & P in EC_SetProjCo(a,b,p) &
ex X,Y be Element of GF(p) st P=[X,Y,1];
consider X,Y be Element of GF(p) such that
A22: P=[X,Y,1] by A21;
reconsider n1=X as Nat;
A23: 0<=n1 & n1 < p by NAT_1:44;
A24: (0 qua Nat) + 1 <= n1+1 by XREAL_1:6;
A25: n1 + 1 <= p by A23,NAT_1:13;
set n=n1+1;
A26: n in Seg p & n-1=X by A24,A25;
x in {Class(R_EllCur(a,b,p),[(n-1),Q,1]) where Q is Element of GF(p) :
[(n-1),Q,1] in EC_SetProjCo(a,b,p) } by A21,A22; then
A27: x in S.n by A26,A2,A3;
S.n in rng S by A26,A3,FUNCT_1:3;
hence x in union rng S by A27,TARSKI:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem Th60:
for p be Prime, a, b be Element of GF(p)
st p > 3 & Disc(a,b,p) <> 0.GF(p) holds
ex F be FinSequence of NAT st len F = p
& (for n be Nat st n in Seg p
ex d be 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 be Element of GF(p) st P=[X,Y,1]} = Sum(F)
proof
let p be Prime, a, b be Element of GF(p);
assume A1: p > 3 & Disc(a,b,p) <> 0.GF(p); then
consider S be Function such that
A2: dom S =Seg p & (for n be 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 be 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 be Element of GF(p) st P=[X,Y,1]} by Lm8;
defpred P0[Nat,Nat] means $2= card (S.$1);
A3:now let i be Nat;
assume i in Seg p;
then S.i is finite by A2; then
reconsider x = card (S.i) as Element of NAT by ORDINAL1:def 12;
take x;
thus P0[i,x];
end;
consider L be FinSequence of NAT such that
A4: dom L= Seg p &
for i be Nat st i in Seg p holds P0[i,L.i] from FINSEQ_1:sch 5(A3);
take L;
p is Element of NAT by ORDINAL1:def 12;
hence len L = p by A4,FINSEQ_1:def 3;
A5: now let n be Nat;
assume A6:n in Seg p; then
1<=n & n<= p by FINSEQ_1:1; then
A7:1-1 <=n-1 & n-1 <=p-1 by XREAL_1:9; then
A8: n-1 is Element of NAT by INT_1:3;
p-1 < p-0 by XREAL_1:15; then
n-1 < p by A7,XXREAL_0:2; then
reconsider d=n-1 as Element of GF(p) by A8,NAT_1:44;
take d;
thus d=n-1;
thus L.n = card (S.n) by A4,A6
.= card ({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) } ) by A2,A6
.= 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) by Th59,A1;
end;
for i be Nat st i in dom S holds
S.i is finite & L.i = card (S.i) by A2,A4;
hence thesis by A2,A4,A5,DIST_1:17;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem
for p be Prime, a, b be Element of GF(p)
st p > 3 & Disc(a,b,p) <> 0.GF(p)
ex F be FinSequence of INT st len F = p &
(for n be Nat st n in Seg p ex d be 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
let p be Prime, a, b be Element of GF(p);
assume
A1: p > 3 & Disc(a,b,p) <> 0.GF(p); then
consider L be FinSequence of NAT such that
A2: len L = p
& (for n be Nat st n in Seg p ex d be Element of GF(p) st d=n-1 &
L.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 be Element of GF(p) st P=[X,Y,1]} = Sum(L) by Th60;
A3: p is Element of NAT by ORDINAL1:def 12;
defpred P0[Nat,set] means
ex d be Element of GF(p) st d=$1-1 & $2 = Lege_p(d|^3 + a*d + b);
A4:now let n be Nat;
assume n in Seg p; then
1<=n & n<= p by FINSEQ_1:1; then
A5:1-1 <=n-1 & n-1 <=p-1 by XREAL_1:9; then
A6: n-1 is Element of NAT by INT_1:3;
p-1 < p-0 by XREAL_1:15; then
n-1 < p by A5,XXREAL_0:2; then
reconsider d=n-1 as Element of GF(p) by A6,NAT_1:44;
reconsider x = Lege_p(d|^3 + a*d + b) as Element of INT by INT_1:def 2;
take x;
thus P0[n,x];
end;
consider F be FinSequence of INT such that
A7: dom F= Seg p &
for i be Nat st i in Seg p holds P0[i,F.i] from FINSEQ_1:sch 5(A4);
take F;
thus A8:len F = p by A7,A3,FINSEQ_1:def 3;
reconsider pp= p |-> jj as Element of p-tuples_on REAL;
F is FinSequence of REAL by FINSEQ_2:24,NUMBERS:15;
then reconsider FF=F as Element of p-tuples_on REAL by A8,FINSEQ_2:92;
A9: now let n be Nat;
assume 1<=n & n<=p; then
A10: n in Seg p; then
A11: ex d be Element of GF(p) st d=n-1 &
L.n = 1 + Lege_p(d|^3 + a*d + b) by A2;
ex f be Element of GF(p) st f=n-1 &
F.n = Lege_p(f|^3 + a*f + b) by A7,A10; then
L.n=(p |-> 1).n +F.n by A11,A10,FUNCOP_1:7;
hence L.n=(pp+FF).n by RVSUM_1:11;
end;
len (pp+FF) = p by FINSEQ_2:132; then
L=pp+FF by A2,A9; then
Sum(L)=Sum(p |-> 1)+Sum(F) by RVSUM_1:89; then
A12: Sum(L)=p*1+Sum(F) by RVSUM_1:80;
reconsider F1 = {Class(R_EllCur(a,b,p),[0,1,0])} as finite set;
reconsider 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 be Element of GF(p)
st P=[X,Y,1]} as finite set by A2;
A13: card F1 = 1 by CARD_2:42;
card (Class (R_EllCur(a,b,p))) = card(F1 \/ F2) by A1,Th51
.= 1 + (p+Sum(F)) by A1,A13,A2,A12,Th53,CARD_2:40;
hence thesis by A7;
end;