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 AS: ( 2 < p & x + x = 0. (GF p) ) ; :: thesis: x = 0. (GF p)
x in Segm p ;
then reconsider Ix = x as Element of NAT ;
A1: 1 = 1. (GF p) by XLm3;
B1: 1 + 1 < p by AS;
A2: (1. (GF p)) + (1. (GF p)) = 2 by A1, B1, INT_3:7;
set d = (1. (GF p)) + (1. (GF p));
A3: ((1. (GF p)) + (1. (GF p))) * x = (2 * Ix) mod p by A2, INT_3:def 10;
x + x = ((1. (GF p)) * x) + x by VECTSP_1:def 6
.= ((1. (GF p)) * x) + ((1. (GF p)) * x) by VECTSP_1:def 6
.= (2 * Ix) mod p by A3, VECTSP_1:def 7 ;
then (2 * Ix) mod p = 0 by AS, XLm2;
then (2 * Ix) - (((2 * Ix) div p) * p) = 0 by INT_1:def 10;
then D6: p divides 2 * Ix by INT_1:def 3;
p divides Ix by AS, D6, 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 D3: Ix mod p = 0 by INT_1:def 10;
Ix < p by NAT_1:44;
then Ix = 0 by D3, NAT_D:63;
hence x = 0. (GF p) by XLm2; :: thesis: verum