let p be Prime; :: thesis: for R being p -characteristic Ring
for n being positive Nat holds
( n is Element of CharSet R iff p divides n )
let R be p -characteristic Ring; :: thesis: for n being positive Nat holds
( n is Element of CharSet R iff p divides n )
let j be positive Nat; :: thesis: ( j is Element of CharSet R iff p divides j )
A1: Char R = p by Def6;
then A2: p '*' (1. R) = 0. R by Def5;
A3: now :: thesis: ( j is Element of CharSet R implies p divides j )
assume A4: j is Element of CharSet R ; :: thesis: p divides j
A5: ((j div p) * p) '*' (1. R) = ((j div p) '*' (1. R)) * (p '*' (1. R)) by Th66
.= 0. R by A2 ;
A6: j '*' (1. R) = (((j div p) * p) + (j mod p)) '*' (1. R) by INT_1:59
.= (0. R) + ((j mod p) '*' (1. R)) by A5, Th61
.= (j mod p) '*' (1. R) ;
j in { k where k is positive Nat : k '*' (1. R) = 0. R } by A4;
then consider l being positive Nat such that
A7: ( l = j & l '*' (1. R) = 0. R ) ;
now :: thesis: not j mod p > 0
assume j mod p > 0 ; :: thesis: contradiction
then reconsider l = j mod p as positive Nat ;
A8: l in { k where k is positive Nat : k '*' (1. R) = 0. R } by A7, A6;
p = min (CharSet R) by A1, Th78;
then p <= j mod p by A8, XXREAL_2:def 7;
hence contradiction by INT_1:58; :: thesis: verum
end;
then A9: j mod p = 0 ;
j = ((j div p) * p) + (j mod p) by INT_1:59;
hence p divides j by A9; :: thesis: verum
end;
now :: thesis: ( p divides j implies j is Element of CharSet R )
assume p divides j ; :: thesis: j is Element of CharSet R
then consider i being Integer such that
A10: j = p * i ;
j '*' (1. R) = (p '*' (1. R)) * (i '*' (1. R)) by A10, Th66
.= (0. R) * (i '*' (1. R)) by A1, Def5
.= 0. R ;
then j in { k where k is positive Nat : k '*' (1. R) = 0. R } ;
hence j is Element of CharSet R ; :: thesis: verum
end;
hence ( j is Element of CharSet R iff p divides j ) by A3; :: thesis: verum