let i be Integer; :: thesis: for p being Prime
for a being Element of (GF p) st a = i mod p holds
- a = (p - i) mod p
let p be Prime; :: thesis: for a being Element of (GF p) st a = i mod p holds
- a = (p - i) mod p
let a be Element of (GF p); :: thesis: ( a = i mod p implies - a = (p - i) mod p )
assume AS: a = i mod p ; :: thesis: - a = (p - i) mod p
consider b being Element of (GF p) such that
P2: b = (p - i) mod p by GF2;
a + b = (i + (p - i)) mod p by AS, P2, GF3
.= 0 by INT_1:50
.= 0. (GF p) by XLm2 ;
hence - a = (p - i) mod p by P2, VECTSP_1:16; :: thesis: verum