let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for a being non zero Element of R
for n being Nat holds
( p divides n iff n * a = 0. R )
let R be commutative p -characteristic Ring; :: thesis: for a being non zero Element of R
for n being Nat holds
( p divides n iff n * a = 0. R )
let a be non zero Element of R; :: thesis: for n being Nat holds
( p divides n iff n * a = 0. R )
let n be Nat; :: thesis: ( p divides n iff n * a = 0. R )

A: now :: thesis: ( p divides n implies n * a = 0. R )

assume p divides n ; :: thesis: n * a = 0. R
then ex x being Nat st p * x = n by NAT_D:def 3;
hence n * a = 0. R by Lm1; :: thesis: verum

end;

now :: thesis: ( n * a = 0. R implies p divides n )

assume AS: n * a = 0. R ; :: thesis: p divides n

now :: thesis: p divides n

assume A: not p divides n ; :: thesis: contradiction
set i = n div p;
set k = n mod p;
B: ( ((n div p) * p) + (n mod p) = n & n mod p < p ) by NAT_D:1, NAT_D:2;
C: (((n div p) * p) + (n mod p)) * a = (((n div p) * p) * a) + ((n mod p) * a) by BINOM:15
.= (0. R) + ((n mod p) * a) by Lm1 ;
n mod p <> 0 by B, A, NAT_D:3;
hence contradiction by AS, B, C, Lm0a; :: thesis: verum

end;

hence p divides n ; :: thesis: verum

end;

hence ( p divides n iff n * a = 0. R ) by A; :: thesis: verum