ec_pf_1.miz



    begin

    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 be non empty set holds for x be Element of [:X1, X2, X3:] holds x = [(x `1_3 ), (x `2_3 ), (x `3_3 )];

    definition

      let K be Field;

      :: EC_PF_1:def1

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

    

     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 :: EC_PF_1:2

    

     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 :: EC_PF_1:3

    

     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 :: EC_PF_1:4

    

     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 :: EC_PF_1:5

    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 :: EC_PF_1:6

    

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

    

     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 :: EC_PF_1:8

    

     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 :: EC_PF_1:9

    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;

      :: original: card

      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 :: EC_PF_1:10

    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;

      :: EC_PF_1:def2

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

    reserve p for Prime;

    reserve a,b,c for Element of ( GF p);

    reserve F for FinSequence of ( GF p);

    theorem :: EC_PF_1:11

    

     Th11: 0 = ( 0. ( GF p)) by NAT_1: 44, SUBSET_1:def 8;

    theorem :: EC_PF_1:12

    

     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 :: EC_PF_1:13

    

     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 :: EC_PF_1:14

    

     Th14: (i mod p) is Element of ( GF p)

    proof

      reconsider b = (i mod p) as Integer;

      b in NAT by INT_1: 3, INT_1: 57;

      then

      reconsider b as Nat;

      b < p by INT_1: 58;

      then b in ( Segm p) by NAT_1: 44;

      hence thesis;

    end;

    theorem :: EC_PF_1:15

    

     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 :: EC_PF_1:16

    

     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 :: EC_PF_1:17

    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 :: EC_PF_1:18

    

     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 :: EC_PF_1:19

    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 :: EC_PF_1:20

    

     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 :: EC_PF_1:21

    

     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 :: EC_PF_1:22

    (a |^ 2) = (a * a) by Lm2;

    theorem :: EC_PF_1:23

    

     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 :: EC_PF_1:24

    

     Th24: for K be unital associative non empty multMagma, a be Element of K, n be 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 :: EC_PF_1:25

    

     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 :: EC_PF_1:26

    

     Th26: for 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 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, RLVECT_1: 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 :: EC_PF_1:27

    

     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, INT_2: 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 :: EC_PF_1:28

    

     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 :: EC_PF_1:29

    

     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 :: EC_PF_1:30

    

     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

    definition

      let p, a;

      :: EC_PF_1:def3

      attr a is quadratic_residue means a <> 0 & ex x be Element of ( GF p) st (x |^ 2) = a;

      :: EC_PF_1:def4

      attr a is not_quadratic_residue means a <> 0 & not ex x be Element of ( GF p) st (x |^ 2) = a;

    end

    theorem :: EC_PF_1:31

    

     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;

      :: EC_PF_1:def5

      func Lege_p (a) -> Integer equals

      : Def5: 0 if a = 0 ,

1 if a is quadratic_residue

      otherwise ( - 1);

      coherence ;

      consistency ;

    end

    theorem :: EC_PF_1:32

    

     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 be 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 be Element of ( GF p) st (x |^ 2) = a;

      hence thesis;

    end;

    theorem :: EC_PF_1:33

    

     Th33: a is quadratic_residue iff ( Lege_p a) = 1 by Def5;

    theorem :: EC_PF_1:34

    

     Th34: a = 0 iff ( Lege_p a) = 0 by Def5;

    theorem :: EC_PF_1:35

    a <> 0 implies ( Lege_p (a |^ 2)) = 1 by Th31, Th33;

    theorem :: EC_PF_1:36

    

     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 be Element of ( GF p) st (x |^ 2) = a by A1;

          b <> 0 & ex x be Element of ( GF p) st (x |^ 2) = b by A3;

          then

           A6: (a * b) <> 0 by A5, Th20;

          ex x be 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 be Element of ( GF p) st (x |^ 2) = a by A1;

          

           A13: (a * b) <> 0 by A10, A12, Th20;

           not ex x be Element of ( GF p) st (x |^ 2) = (a * b)

          proof

            given xab be Element of ( GF p) such that

             A14: (xab |^ 2) = (a * b);

            consider xa be 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 be Element of ( GF p) st (x |^ 2) = b by A22;

              then

               A25: (a * b) <> 0 by A20, Th20;

               not ex x be Element of ( GF p) st (x |^ 2) = (a * b)

              proof

                given xab be Element of ( GF p) such that

                 A26: (xab |^ 2) = (a * b);

                consider xb be 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 be 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 :: EC_PF_1:37

    

     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 :: EC_PF_1:38

    (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 :: EC_PF_1:39

    

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

    definition

      let K be Field;

      :: EC_PF_1:def6

      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 :: EC_PF_1:40

    

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

      :: EC_PF_1:def7

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

      :: EC_PF_1:def8

      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 be 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 be Element of DX holds (f . x) = F(x);

        assume

         A3: for x be 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 :: EC_PF_1:41

    

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

      :: EC_PF_1:def9

      func EC_SetProjCo (a,b,p) -> non empty Subset of ( ProjCo ( GF p)) equals { P where P be 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 be 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 be 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 :: EC_PF_1:42

    

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

      hence thesis;

    end;

    theorem :: EC_PF_1:43

    

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

      :: EC_PF_1:def10

      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 :: EC_PF_1:44

    

     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 :: EC_PF_1:45

    

     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;

      :: EC_PF_1:def11

      func R_ProjCo p -> Relation of ( ProjCo ( GF p)) equals { [P, Q] where P,Q be Element of ( ProjCo ( GF p)) : P _EQ_ Q };

      correctness

      proof

        set RX = { [P, Q] where P,Q be 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 :: EC_PF_1:46

    

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

      :: EC_PF_1:def12

      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 :: EC_PF_1:47

    

     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 :: EC_PF_1:48

    

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

    

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

    

     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 :: EC_PF_1:51

    

     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 be 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 be 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 be 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 be 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 :: EC_PF_1:52

    

     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 :: EC_PF_1:53

    

     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 be 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 be 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 :: EC_PF_1:54

    

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

    

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

    

     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 :: EC_PF_1:57

    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 :: EC_PF_1:58

    

     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 be Element of ( GF p) : (Y |^ 2) = (((d |^ 3) + (a * d)) + b) } & F <> {} & G = { ( Class (( R_EllCur (a,b,p)), [d, Y, 1])) where Y be 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 be Element of ( GF p) : (Y |^ 2) = (((d |^ 3) + (a * d)) + b) } & F <> {} & G = { ( Class (( R_EllCur (a,b,p)), [d, P, 1])) where P be 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 :: EC_PF_1:59

    

     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 be 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 be Element of ( GF p) : (Y |^ 2) = (((d |^ 3) + (a * d)) + b) };

      set G = { ( Class (( R_EllCur (a,b,p)), [d, Y, 1])) where Y be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 :: EC_PF_1:60

    

     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) holds 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 be 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 be 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 be 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 be 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 be 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 :: EC_PF_1:61

    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 INT st ( len F) = p & (for n be Nat st n in ( Seg p) holds 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) holds 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 be 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 be 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;