let R be domRing; ( Char R = 0 or Char R is prime )
set n = Char R;
now ( Char R <> 0 implies Char R is prime )assume A1:
Char R <> 0
;
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 A3:
Char R > 1
;
Char R is prime now Char R is prime assume
not
Char R is
prime
;
contradictionthen 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;
then
u < Char R
by A8, XXREAL_0:1;
hence
contradiction
by A7, A6, Def5;
verum end; hence
Char R is
prime
;
verum end; end; end;
hence
( Char R = 0 or Char R is prime )
; verum