let p be 5 _or_greater Prime; for z being Element of EC_WParam p
for g3 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st g3 = 3 mod p & P `2_3 = 0 & P `3_3 <> 0 holds
((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) <> 0
let z be Element of EC_WParam p; for g3 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st g3 = 3 mod p & P `2_3 = 0 & P `3_3 <> 0 holds
((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) <> 0
let g3 be Element of (GF p); for P being Element of EC_SetProjCo ((z `1),(z `2),p) st g3 = 3 mod p & P `2_3 = 0 & P `3_3 <> 0 holds
((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) <> 0
let P be Element of EC_SetProjCo ((z `1),(z `2),p); ( g3 = 3 mod p & P `2_3 = 0 & P `3_3 <> 0 implies ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) <> 0 )
assume that
A1:
g3 = 3 mod p
and
A2:
P `2_3 = 0
and
A3:
P `3_3 <> 0
; ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) <> 0
set a = z `1 ;
set b = z `2 ;
A4:
( p > 3 & Disc ((z `1),(z `2),p) <> 0. (GF p) )
by Th30;
(P `3_3) |^ 2 <> 0
by A3, EC_PF_1:25;
then A5:
(P `3_3) |^ 2 <> 0. (GF p)
by EC_PF_1:11;
0 = 0. (GF p)
by EC_PF_1:11;
then A6:
(P `2_3) |^ 2 = 0. (GF p)
by A2, Th5;
reconsider g2 = 2 mod p as Element of (GF p) by EC_PF_1:14;
reconsider g4 = 4 mod p as Element of (GF p) by EC_PF_1:14;
reconsider g9 = 9 mod p as Element of (GF p) by EC_PF_1:14;
reconsider g27 = 27 mod p as Element of (GF p) by EC_PF_1:14;
A7:
3 = 2 + 1
;
A8: g2 |^ 2 =
g2 * g2
by EC_PF_1:22
.=
(2 * 2) mod p
by EC_PF_1:18
.=
g4
;
A9: g3 |^ 2 =
g3 * g3
by EC_PF_1:22
.=
(3 * 3) mod p
by A1, EC_PF_1:18
.=
g9
;
A10: g3 |^ 3 =
g3 |^ (2 + 1)
.=
g9 * g3
by A9, EC_PF_1:24
.=
(9 * 3) mod p
by A1, EC_PF_1:18
.=
g27
;
assume A11:
((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) = 0
; contradiction
(((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p)
by Th35;
then
((P `2_3) |^ 2) * (P `3_3) = (((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3))
by VECTSP_1:19;
then
g3 * ((((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p)
by A6;
then
(g3 * (((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2)))) + (g3 * ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p)
by VECTSP_1:def 7;
then
((g3 * ((P `1_3) |^ 3)) + (g3 * (((z `1) * (P `1_3)) * ((P `3_3) |^ 2)))) + (g3 * ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p)
by VECTSP_1:def 7;
then
((g3 * ((P `1_3) |^ (2 + 1))) + (g3 * ((z `1) * ((P `1_3) * ((P `3_3) |^ 2))))) + (g3 * ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p)
by GROUP_1:def 3;
then
((g3 * ((P `1_3) |^ (2 + 1))) + ((g3 * (z `1)) * ((P `1_3) * ((P `3_3) |^ 2)))) + (g3 * ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p)
by GROUP_1:def 3;
then
((g3 * ((P `1_3) |^ (2 + 1))) + (((g3 * (z `1)) * (P `1_3)) * ((P `3_3) |^ 2))) + (g3 * ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p)
by GROUP_1:def 3;
then
((g3 * ((P `1_3) |^ (2 + 1))) + (((g3 * (z `1)) * (P `1_3)) * ((P `3_3) |^ 2))) + ((g3 * (z `2)) * ((P `3_3) |^ 3)) = 0. (GF p)
by GROUP_1:def 3;
then
((g3 * (((P `1_3) |^ 2) * (P `1_3))) + (((g3 * (z `1)) * (P `1_3)) * ((P `3_3) |^ 2))) + ((g3 * (z `2)) * ((P `3_3) |^ (2 + 1))) = 0. (GF p)
by EC_PF_1:24;
then
((g3 * (((P `1_3) |^ 2) * (P `1_3))) + (((g3 * (z `1)) * (P `1_3)) * ((P `3_3) |^ 2))) + ((g3 * (z `2)) * (((P `3_3) |^ 2) * (P `3_3))) = 0. (GF p)
by EC_PF_1:24;
then
(((g3 * ((P `1_3) |^ 2)) * (P `1_3)) + (((g3 * (z `1)) * (P `1_3)) * ((P `3_3) |^ 2))) + ((g3 * (z `2)) * ((P `3_3) * ((P `3_3) |^ 2))) = 0. (GF p)
by GROUP_1:def 3;
then
(((g3 * ((P `1_3) |^ 2)) * (P `1_3)) + (((g3 * (z `1)) * (P `1_3)) * ((P `3_3) |^ 2))) + (((g3 * (z `2)) * (P `3_3)) * ((P `3_3) |^ 2)) = 0. (GF p)
by GROUP_1:def 3;
then
((g3 * ((P `1_3) |^ 2)) * (P `1_3)) + ((((P `3_3) |^ 2) * ((g3 * (z `1)) * (P `1_3))) + (((P `3_3) |^ 2) * ((g3 * (z `2)) * (P `3_3)))) = 0. (GF p)
by ALGSTR_1:7;
then A12:
((g3 * ((P `1_3) |^ 2)) * (P `1_3)) + (((P `3_3) |^ 2) * (((g3 * (z `1)) * (P `1_3)) + ((g3 * (z `2)) * (P `3_3)))) = 0. (GF p)
by VECTSP_1:def 7;
A13:
((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) = 0. (GF p)
by A11, EC_PF_1:11;
then
((- ((z `1) * ((P `3_3) |^ 2))) * (P `1_3)) + (((P `3_3) |^ 2) * (((g3 * (z `1)) * (P `1_3)) + ((g3 * (z `2)) * (P `3_3)))) = 0. (GF p)
by A12, VECTSP_1:16;
then
(((- (z `1)) * ((P `3_3) |^ 2)) * (P `1_3)) + (((P `3_3) |^ 2) * (((g3 * (z `1)) * (P `1_3)) + ((g3 * (z `2)) * (P `3_3)))) = 0. (GF p)
by VECTSP_1:9;
then
(((P `3_3) |^ 2) * ((- (z `1)) * (P `1_3))) + (((P `3_3) |^ 2) * (((g3 * (z `1)) * (P `1_3)) + ((g3 * (z `2)) * (P `3_3)))) = 0. (GF p)
by GROUP_1:def 3;
then
((P `3_3) |^ 2) * (((- (z `1)) * (P `1_3)) + (((g3 * (z `1)) * (P `1_3)) + ((g3 * (z `2)) * (P `3_3)))) = 0. (GF p)
by VECTSP_1:def 7;
then
((- (z `1)) * (P `1_3)) + (((g3 * (z `1)) * (P `1_3)) + ((g3 * (z `2)) * (P `3_3))) = 0. (GF p)
by A5, VECTSP_1:12;
then
(((- (z `1)) * (P `1_3)) + ((g3 * (z `1)) * (P `1_3))) + ((g3 * (z `2)) * (P `3_3)) = 0. (GF p)
by ALGSTR_1:7;
then
((- ((z `1) * (P `1_3))) + ((g3 * (z `1)) * (P `1_3))) + ((g3 * (z `2)) * (P `3_3)) = 0. (GF p)
by VECTSP_1:9;
then
((g3 * ((z `1) * (P `1_3))) - ((z `1) * (P `1_3))) + ((g3 * (z `2)) * (P `3_3)) = 0. (GF p)
by GROUP_1:def 3;
then
(g2 * ((z `1) * (P `1_3))) + ((g3 * (z `2)) * (P `3_3)) = 0. (GF p)
by A1, A7, Th23;
then
g2 * ((z `1) * (P `1_3)) = - ((g3 * (z `2)) * (P `3_3))
by VECTSP_1:16;
then
(g2 * ((z `1) * (P `1_3))) |^ 2 = ((g3 * (z `2)) * (P `3_3)) |^ 2
by Th1;
then
(g2 |^ 2) * (((z `1) * (P `1_3)) |^ 2) = ((g3 * (z `2)) * (P `3_3)) |^ 2
by BINOM:9;
then
(g2 |^ 2) * (((z `1) * (P `1_3)) |^ 2) = (g3 * ((z `2) * (P `3_3))) |^ 2
by GROUP_1:def 3;
then
(g2 |^ 2) * (((z `1) |^ 2) * ((P `1_3) |^ 2)) = (g3 * ((z `2) * (P `3_3))) |^ 2
by BINOM:9;
then
(g2 |^ 2) * (((z `1) |^ 2) * ((P `1_3) |^ 2)) = (g3 |^ 2) * (((z `2) * (P `3_3)) |^ 2)
by BINOM:9;
then
(g2 |^ 2) * (((z `1) |^ 2) * ((P `1_3) |^ 2)) = (g3 |^ 2) * (((z `2) |^ 2) * ((P `3_3) |^ 2))
by BINOM:9;
then
((g2 |^ 2) * ((z `1) |^ 2)) * ((P `1_3) |^ 2) = (g3 |^ 2) * (((z `2) |^ 2) * ((P `3_3) |^ 2))
by GROUP_1:def 3;
then A14:
((g2 |^ 2) * ((z `1) |^ 2)) * ((P `1_3) |^ 2) = ((g3 |^ 2) * ((z `2) |^ 2)) * ((P `3_3) |^ 2)
by GROUP_1:def 3;
((g2 |^ 2) * ((z `1) |^ 2)) * (((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) = 0. (GF p)
by A13;
then
(((g2 |^ 2) * ((z `1) |^ 2)) * ((z `1) * ((P `3_3) |^ 2))) + (((g2 |^ 2) * ((z `1) |^ 2)) * (g3 * ((P `1_3) |^ 2))) = 0. (GF p)
by VECTSP_1:def 7;
then
((g2 |^ 2) * (((z `1) |^ 2) * ((z `1) * ((P `3_3) |^ 2)))) + (((g2 |^ 2) * ((z `1) |^ 2)) * (g3 * ((P `1_3) |^ 2))) = 0. (GF p)
by GROUP_1:def 3;
then
((g2 |^ 2) * ((((z `1) |^ 2) * (z `1)) * ((P `3_3) |^ 2))) + (((g2 |^ 2) * ((z `1) |^ 2)) * (g3 * ((P `1_3) |^ 2))) = 0. (GF p)
by GROUP_1:def 3;
then
((g2 |^ 2) * (((z `1) |^ (2 + 1)) * ((P `3_3) |^ 2))) + ((g3 * ((P `1_3) |^ 2)) * ((g2 |^ 2) * ((z `1) |^ 2))) = 0. (GF p)
by EC_PF_1:24;
then
((g2 |^ 2) * (((z `1) |^ 3) * ((P `3_3) |^ 2))) + (g3 * (((P `1_3) |^ 2) * ((g2 |^ 2) * ((z `1) |^ 2)))) = 0. (GF p)
by GROUP_1:def 3;
then
(((g2 |^ 2) * ((z `1) |^ 3)) * ((P `3_3) |^ 2)) + (g3 * (((g3 |^ 2) * ((z `2) |^ 2)) * ((P `3_3) |^ 2))) = 0. (GF p)
by A14, GROUP_1:def 3;
then
(((g2 |^ 2) * ((z `1) |^ 3)) * ((P `3_3) |^ 2)) + (g3 * ((g3 |^ 2) * (((z `2) |^ 2) * ((P `3_3) |^ 2)))) = 0. (GF p)
by GROUP_1:def 3;
then
(((g2 |^ 2) * ((z `1) |^ 3)) * ((P `3_3) |^ 2)) + ((g3 * (g3 |^ 2)) * (((z `2) |^ 2) * ((P `3_3) |^ 2))) = 0. (GF p)
by GROUP_1:def 3;
then
(((P `3_3) |^ 2) * ((g2 |^ 2) * ((z `1) |^ 3))) + ((g3 |^ (2 + 1)) * (((z `2) |^ 2) * ((P `3_3) |^ 2))) = 0. (GF p)
by EC_PF_1:24;
then
(((P `3_3) |^ 2) * ((g2 |^ 2) * ((z `1) |^ 3))) + (((g3 |^ 3) * ((z `2) |^ 2)) * ((P `3_3) |^ 2)) = 0. (GF p)
by GROUP_1:def 3;
then
((P `3_3) |^ 2) * (((g2 |^ 2) * ((z `1) |^ 3)) + ((g3 |^ 3) * ((z `2) |^ 2))) = 0. (GF p)
by VECTSP_1:def 7;
then
(g4 * ((z `1) |^ 3)) + (g27 * ((z `2) |^ 2)) = 0. (GF p)
by A5, A8, A10, VECTSP_1:12;
hence
contradiction
by A4, EC_PF_1:def 7; verum