let m be Nat; :: thesis: for n0 being non zero Nat st sigma n0 = n0 + m & m divides n0 & n0 <> m holds
( m = 1 & n0 is prime )
let n0 be non zero Nat; :: thesis: ( sigma n0 = n0 + m & m divides n0 & n0 <> m implies ( m = 1 & n0 is prime ) )
assume A1: sigma n0 = n0 + m ; :: thesis: ( not m divides n0 or not n0 <> m or ( m = 1 & n0 is prime ) )
assume A2: m divides n0 ; :: thesis: ( not n0 <> m or ( m = 1 & n0 is prime ) )
assume A3: n0 <> m ; :: thesis: ( m = 1 & n0 is prime )

per cases ( n0 = 1 or n0 <> 1 ) ;

suppose n0 = 1 ; :: thesis: ( m = 1 & n0 is prime )

then 1 = 1 + m by A1, Th29;
hence ( m = 1 & n0 is prime ) by A2, INT_2:3; :: thesis: verum

end;

suppose A4: n0 <> 1 ; :: thesis: ( m = 1 & n0 is prime )

consider k being Nat such that
A5: n0 = m * k by A2, NAT_D:def 3;
A6: k <> m

proof

assume k = m ; :: thesis: contradiction
then m <> 1 by A4, A5;
then (1 + m) + n0 <= sigma n0 by A2, A3, Th31;
then ((1 + m) + n0) - (m + n0) <= (n0 + m) - (m + n0) by A1, XREAL_1:9;
hence contradiction ; :: thesis: verum

end;

k = n0

proof

A7: ( k divides n0 & k <> 1 ) by A3, A5, NAT_D:def 3;
assume A8: k <> n0 ; :: thesis: contradiction
then m <> 1 by A5;
then ((1 + m) + k) + n0 <= sigma n0 by A2, A3, A6, A8, A7, Th32;
then (((1 + m) + k) + n0) - (m + n0) <= (n0 + m) - (m + n0) by A1, XREAL_1:9;
then 1 + k <= 0 ;
hence contradiction ; :: thesis: verum

end;

then n0 / n0 = m by A5, XCMPLX_1:89;
hence A9: m = 1 by XCMPLX_1:60; :: thesis: n0 is prime
A10: for k being Nat holds
( not k divides n0 or k = 1 or k = n0 )

proof

let k be Nat; :: thesis: ( not k divides n0 or k = 1 or k = n0 )
assume that
A11: k divides n0 and
A12: k <> 1 ; :: thesis: k = n0
assume k <> n0 ; :: thesis: contradiction
then (1 + k) + n0 <= n0 + 1 by A1, A9, A11, A12, Th31;
then ((1 + k) + n0) - (1 + n0) <= (n0 + 1) - (1 + n0) by XREAL_1:9;
then k = 0 ;
hence contradiction by A11, INT_2:3; :: thesis: verum

end;

n0 > 1 by A4, NAT_1:25;
hence n0 is prime by A10, INT_2:def 4; :: thesis: verum

end;

end;