:: Set of Points on Elliptic Curve in Projective Coordinates :: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama :: :: Received December 21, 2010 :: Copyright (c) 2010-2019 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, 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, ORDINAL1, MCART_1, XTUPLE_0; 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; 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 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 by INT_1:def 10; 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 A5: not P in {[0,0,0]} by A2,XBOOLE_0:def 5; P`1_3 <> 0 or P`2_3 <> 0 or P`3_3 <> 0 proof assume not (P`1_3 <> 0 or P`2_3 <> 0 or P`3_3 <> 0); then P = [0,0,0]; hence contradiction by A5,TARSKI:def 1; end; 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 A3,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;