let p be Prime; :: thesis: for x being Element of (GF p) st 2 < p & x + x = 0. (GF p) holds
x = 0. (GF p)
let x be Element of (GF p); :: thesis: ( 2 < p & x + x = 0. (GF p) implies x = 0. (GF p) )
assume A1: ( 2 < p & x + x = 0. (GF p) ) ; :: thesis: 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: ((1. (GF p)) + (1. (GF p))) * 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) ; :: thesis: verum