let p be 5 _or_greater Prime; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ; :: thesis: ((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 ; :: thesis: 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; :: thesis: verum