let p be Nat; :: thesis: for a being Integer holds ((a * p) + 1) mod p = 1 mod p
let a be Integer; :: thesis: ((a * p) + 1) mod p = 1 mod p
per cases ( p <> 0 or p = 0 ) ;
suppose A1: p <> 0 ; :: thesis: ((a * p) + 1) mod p = 1 mod p
reconsider p = p as Integer ;
((a * p) + 1) mod p = ((a * p) + 1) - ((((a * p) + 1) div p) * p) by A1, INT_1:def 10
.= ((a * p) + 1) - ([\(((a * p) / p) + (1 / p))/] * p) by XCMPLX_1:62
.= ((a * p) + 1) - ([\(a + (1 / p))/] * p) by A1, XCMPLX_1:89
.= ((a * p) + 1) - ((a + [\(1 / p)/]) * p) by INT_1:28
.= 1 - ((1 div p) * p) ;
hence ((a * p) + 1) mod p = 1 mod p by A1, INT_1:def 10; :: thesis: verum
end;
suppose p = 0 ; :: thesis: ((a * p) + 1) mod p = 1 mod p
hence ((a * p) + 1) mod p = 1 mod p ; :: thesis: verum
end;
end;