let n, k be Nat; :: thesis: for a, b being non trivial Nat st a,b are_congruent_mod k holds
Px (a,n), Px (b,n) are_congruent_mod k
let a, b be non trivial Nat; :: thesis: ( a,b are_congruent_mod k implies Px (a,n), Px (b,n) are_congruent_mod k )
assume a,b are_congruent_mod k ; :: thesis: Px (a,n), Px (b,n) are_congruent_mod k
then consider x being Integer such that
A1: k * x = a - b by INT_1:def 5;
consider p being Integer such that
A2: (a - b) * p = (Px (a,n)) - (Px (b,n)) by HILB10_1:25, INT_1:def 5;
p * (a - b) = p * (x * k) by A1
.= (p * x) * k ;
hence Px (a,n), Px (b,n) are_congruent_mod k by A2, INT_1:def 5; :: thesis: verum