let R be domRing; :: thesis: ( Char R = 0 or Char R is prime )
set n = Char R;
now :: thesis: ( Char R <> 0 implies Char R is prime )
assume A1: Char R <> 0 ; :: thesis: Char R is prime
then A2: ( (Char R) '*' (1. R) = 0. R & Char R <> 0 & ( for m being positive Nat st m < Char R holds
m '*' (1. R) <> 0. R ) ) by Def5;
per cases ( Char R = 1 or Char R > 1 ) by A1, NAT_1:25;
suppose Char R = 1 ; :: thesis: Char R is prime
hence Char R is prime by A2, Th59; :: thesis: verum
end;
suppose A3: Char R > 1 ; :: thesis: Char R is prime
now :: thesis: Char R is prime
assume not Char R is prime ; :: thesis: contradiction
then consider m being Nat such that
A4: ( m divides Char R & not m = 1 & not m = Char R ) by A3, INT_2:def 4;
consider u being Integer such that
A5: m * u = Char R by A4;
u > 0 by A5, A3;
then u in NAT by INT_1:3;
then reconsider u = u as positive Nat by A5, A3;
m <> 0 by A5, A3;
then reconsider m = m as positive Nat ;
0. R = (m * u) '*' (1. R) by A5, Def5
.= (m '*' (1. R)) * (u '*' (1. R)) by Th66 ;
then A6: ( m '*' (1. R) = 0. R or u '*' (1. R) = 0. R ) by VECTSP_2:def 1;
m <= Char R by A3, A4, INT_2:27;
then A7: m < Char R by A4, XXREAL_0:1;
A8: u <= Char R by A3, INT_2:27, A5, INT_1:def 3;
now :: thesis: not u = Char R
assume u = Char R ; :: thesis: contradiction
then (Char R) / (Char R) = (m * (Char R)) / (Char R) by A5
.= m * ((Char R) / (Char R))
.= m * 1 by A1, XCMPLX_1:60 ;
hence contradiction by A4, A3, XCMPLX_1:60; :: thesis: verum
end;
then u < Char R by A8, XXREAL_0:1;
hence contradiction by A7, A6, Def5; :: thesis: verum
end;
hence Char R is prime ; :: thesis: verum
end;
end;
end;
hence ( Char R = 0 or Char R is prime ) ; :: thesis: verum