let i, j be Integer; :: thesis: for p being Prime
for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a - b = (i - j) mod p
let p be Prime; :: thesis: for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a - b = (i - j) mod p
let a, b be Element of (GF p); :: thesis: ( a = i mod p & b = j mod p implies a - b = (i - j) mod p )
assume A1: ( a = i mod p & b = j mod p ) ; :: thesis: a - b = (i - j) mod p
then - b = (p - j) mod p by Th16;
then a - b = (i + (p - j)) mod p by A1, Th15
.= ((i - j) + (1 * p)) mod p ;
hence a - b = (i - j) mod p by NAT_D:61; :: thesis: verum