let m be natural number ; :: thesis: for n0 being non zero natural number st sigma n0 = n0 + m & m divides n0 & n0 <> m holds
( m = 1 & n0 is prime )
let n0 be non zero natural number ; :: 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:10; :: thesis: verum

end;

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

consider k being natural number 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 A5, A4;
then (1 + m) + n0 <= sigma n0 by A2, A3, Th31;
then ((1 + m) + n0) - (m + n0) <= (n0 + m) - (m + n0) by A1, XREAL_1:11;
hence contradiction ; :: thesis: verum

end;

k = n0

proof

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

end;

then n0 / n0 = m by A5, XCMPLX_1:90;
hence A10: m = 1 by XCMPLX_1:60; :: thesis: n0 is prime
A11: n0 > 1 by A4, NAT_1:26;
for k being natural number holds
( not k divides n0 or k = 1 or k = n0 )

proof

let k be natural number ; :: thesis: ( not k divides n0 or k = 1 or k = n0 )
assume A12: ( k divides n0 & k <> 1 ) ; :: thesis: k = n0
assume k <> n0 ; :: thesis: contradiction
then (1 + k) + n0 <= n0 + 1 by A1, A10, A12, Th31;
then ((1 + k) + n0) - (1 + n0) <= (n0 + 1) - (1 + n0) by XREAL_1:11;
then k = 0 ;
hence contradiction by A12, INT_2:3; :: thesis: verum

end;

hence n0 is prime by A11, INT_2:def 5; :: thesis: verum

end;

end;