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 )

( 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 )
;

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

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 )

hence n0 is prime by A10, INT_2:def 4; :: thesis: verum

end;A5: n0 = m * k by A2, NAT_D:def 3;

A6: k <> m

proof

k = n0
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;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

proof

then
n0 / n0 = m
by A5, XCMPLX_1:89;
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;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

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

n0 > 1
by A4, NAT_1:25;
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;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

hence n0 is prime by A10, INT_2:def 4; :: thesis: verum