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 A1: a = i mod p ; :: thesis: - a = (p - i) mod p
reconsider b = (p - i) mod p as Element of (GF p) by Th14;
a + b = (i + (p - i)) mod p by A1, Th15
.= 0 by INT_1:50
.= 0. (GF p) by Th11 ;
hence - a = (p - i) mod p by VECTSP_1:16; :: thesis: verum