let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & not P _EQ_ O holds
( P `2_3 = 0. (GF p) iff (addell_ProjCo (z,p)) . (P,P) _EQ_ O )
let z be Element of EC_WParam p; :: thesis: for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & not P _EQ_ O holds
( P `2_3 = 0. (GF p) iff (addell_ProjCo (z,p)) . (P,P) _EQ_ O )
let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] & not P _EQ_ O implies ( P `2_3 = 0. (GF p) iff (addell_ProjCo (z,p)) . (P,P) _EQ_ O ) )
assume that
A1: O = [0,1,0] and
A2: not P _EQ_ O ; :: thesis: ( P `2_3 = 0. (GF p) iff (addell_ProjCo (z,p)) . (P,P) _EQ_ O )
reconsider g2 = 2 mod p, g3 = 3 mod p, g4 = 4 mod p, g8 = 8 mod p as Element of (GF p) by EC_PF_1:14;
set gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2));
set gf2 = (P `2_3) * (P `3_3);
set gf3 = ((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3));
set gf4 = ((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3))));
A3: (addell_ProjCo (z,p)) . (P,P) = [((g2 * (((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)))))) * ((P `2_3) * (P `3_3))),(((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) * ((g4 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)))) - (((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3))))))) - ((g8 * ((P `2_3) |^ 2)) * (((P `2_3) * (P `3_3)) |^ 2))),(g8 * (((P `2_3) * (P `3_3)) |^ 3))] by A1, A2, EC_PF_2:def 9;

hereby :: thesis: ( (addell_ProjCo (z,p)) . (P,P) _EQ_ O implies P `2_3 = 0. (GF p) )

assume P `2_3 = 0. (GF p) ; :: thesis: (addell_ProjCo (z,p)) . (P,P) _EQ_ O
then g8 * (((P `2_3) * (P `3_3)) |^ 3) = g8 * ((0. (GF p)) |^ (2 + 1))
.= g8 * (((0. (GF p)) |^ 2) * (0. (GF p))) by EC_PF_1:24
.= 0. (GF p) ;
then ((addell_ProjCo (z,p)) . (P,P)) `3_3 = 0. (GF p) by A3, EC_PF_2:def 5
.= 0 by EC_PF_1:11 ;
hence (addell_ProjCo (z,p)) . (P,P) _EQ_ O by A1, ThEQO; :: thesis: verum

end;

assume (addell_ProjCo (z,p)) . (P,P) _EQ_ O ; :: thesis: P `2_3 = 0. (GF p)
then B1: ((addell_ProjCo (z,p)) . (P,P)) `3_3 = 0 by A1, ThEQO
.= 0. (GF p) by EC_PF_1:11 ;
B2: ((addell_ProjCo (z,p)) . (P,P)) `3_3 = g8 * (((P `2_3) * (P `3_3)) |^ 3) by A3, EC_PF_2:def 5;
g8 <> 0. (GF p)

proof

C1: g2 |^ 3 = (2 |^ (2 + 1)) mod p by EC_PF_1:23
.= ((2 |^ (1 + 1)) * 2) mod p by NEWTON:6
.= (((2 |^ 1) * 2) * 2) mod p by NEWTON:6
.= g8 ;
p >= 3 + 2 by EC_PF_2:def 1;
then p > 2 by XXREAL_0:2;
hence g8 <> 0. (GF p) by C1, EC_PF_2:28; :: thesis: verum

end;

then ((P `2_3) * (P `3_3)) |^ 3 = 0. (GF p) by B1, B2, VECTSP_1:12
.= 0 by EC_PF_1:11 ;
then B4: (P `2_3) * (P `3_3) = 0. (GF p) by EC_PF_1:25;
P `3_3 <> 0 by A1, A2, ThEQO;
then P `3_3 <> 0. (GF p) by EC_PF_1:11;
hence P `2_3 = 0. (GF p) by B4, VECTSP_1:12; :: thesis: verum