let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for a being non zero Element of R
for n being non zero Nat st n < p holds
n * a <> 0. R
let R be commutative p -characteristic Ring; :: thesis: for a being non zero Element of R
for n being non zero Nat st n < p holds
n * a <> 0. R
let a be non zero Element of R; :: thesis: for n being non zero Nat st n < p holds
n * a <> 0. R
let n be non zero Nat; :: thesis: ( n < p implies n * a <> 0. R )
assume AS: n < p ; :: thesis: n * a <> 0. R
defpred S₁[ Nat] means ( $1 <> 0 & $1 * a = 0. R );
S₁[p] by Lm0;
then E: ex k being Nat st S₁[k] ;
consider u being Nat such that
D: ( S₁[u] & ( for v being Nat st S₁[v] holds
u <= v ) ) from NAT_1:sch 5(E);
Z: S₁[p] by Lm0;
then Y: u <= p by D;

now :: thesis: not u < p

assume G0: u < p ; :: thesis: contradiction
defpred S₂[ Nat] means $1 * u <= p;
IA: S₂[1] by Z, D;

IS: now :: thesis: for k being Nat st 1 <= k & S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis: ( 1 <= k & S₂[k] implies S₂[k + 1] )
assume 1 <= k ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[k + 1]
then reconsider v = p - (k * u) as Element of NAT by INT_1:5;

G: now :: thesis: not v = 0

assume v = 0 ; :: thesis: contradiction
then u divides p by NAT_D:def 3;
then u = 1 by G0, INT_2:def 4;
hence contradiction by D, BINOM:13; :: thesis: verum

end;

consider m being Nat such that
G4: ( ( v = m & v '*' a = m * a ) or ( v = - m & v '*' a = - (m * a) ) ) by RING_3:def 2;
consider m1 being Nat such that
G5: ( ( u = m1 & u '*' a = m1 * a ) or ( u = - m1 & u '*' a = - (m1 * a) ) ) by RING_3:def 2;
consider m2 being Nat such that
G6: ( ( p = m2 & p '*' a = m2 * a ) or ( p = - m2 & p '*' a = - (m2 * a) ) ) by RING_3:def 2;
v * a = (p '*' a) - ((k * u) '*' a) by G4, G, RING_3:64
.= (p '*' a) - (k '*' (u '*' a)) by RING_3:65
.= (p '*' a) + (- (0. R)) by D, G5, Lm0x
.= 0. R by G6, Lm0 ;
then u + (k * u) <= (p - (k * u)) + (k * u) by G, D, XREAL_1:6;
hence S₂[k + 1] ; :: thesis: verum

end;

I: for k being Nat st k >= 1 holds
S₂[k] from NAT_1:sch 8(IA, IS);
G1: p >= 1 by INT_2:def 4;
u = 1

proof

G2: u >= 0 + 1 by D, INT_1:7;

now :: thesis: not u > 1

assume u > 1 ; :: thesis: contradiction
then u * p > 1 * p by XREAL_1:68;
hence contradiction by G1, I; :: thesis: verum

end;

hence u = 1 by G2, XXREAL_0:1; :: thesis: verum

end;

hence contradiction by D, BINOM:13; :: thesis: verum

end;

then u = p by Y, XXREAL_0:1;
hence n * a <> 0. R by D, AS; :: thesis: verum