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)
.= ((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;