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

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

suppose n0 = 1 ; :: thesis: (1 + m) + n0 <= sigma n0

hence (1 + m) + n0 <= sigma n0 by A2, A1, WSIERP_1:20; :: thesis: verum

end;

suppose A4: n0 <> 1 ; :: thesis: (1 + m) + n0 <= sigma n0

reconsider X = {1,m,n0} as finite Subset of NAT by Lm2;
for x being set st x in X holds
x in NatDivisors n0

proof

let x be set ; :: thesis: ( x in X implies x in NatDivisors n0 )
assume A5: x in X ; :: thesis: x in NatDivisors n0
then A6: ( x = 1 or x = m or x = n0 ) by ENUMSET1:def 1;
reconsider x' = x as Element of NAT by A5;
A7: x' <> 0 by A6, A1, INT_2:10;
x' divides n0 by A6, A1, NAT_D:6;
hence x in NatDivisors n0 by A7; :: thesis: verum

end;

then A8: X c= NatDivisors n0 by TARSKI:def 3;
set Y = (NatDivisors n0) \ X;
A9: NatDivisors n0 = X \/ ((NatDivisors n0) \ X) by A8, XBOOLE_1:45;
A10: sigma n0 = Sum ((EXP 1) | (X \/ ((NatDivisors n0) \ X))) by A9, Def2
.= (Sum ((EXP 1) | X)) + (Sum ((EXP 1) | ((NatDivisors n0) \ X))) by XBOOLE_1:79, Th26 ;
set X1 = {1};
reconsider X2 = {m,n0} as finite Subset of NAT by Th5;
reconsider X3 = {m} as finite Subset of NAT by Th4;
reconsider X4 = {n0} as finite Subset of NAT by Th4;
A11: X2 = X3 \/ X4 by ENUMSET1:41;

now

let x be set ; :: thesis: not x in X3 /\ X4
assume x in X3 /\ X4 ; :: thesis: contradiction
then ( x in X3 & x in X4 ) by XBOOLE_0:def 4;
then ( x = m & x = n0 ) by TARSKI:def 1;
hence contradiction by A2; :: thesis: verum

end;

then X3 /\ X4 = {} by XBOOLE_0:def 1;
then A12: X3 misses X4 by XBOOLE_0:def 7;

now

let x be set ; :: thesis: not x in {1} /\ X2
assume x in {1} /\ X2 ; :: thesis: contradiction
then ( x in {1} & x in X2 ) by XBOOLE_0:def 4;
then ( x = 1 & x in X2 ) by TARSKI:def 1;
hence contradiction by A3, A4, TARSKI:def 2; :: thesis: verum

end;

then {1} /\ X2 = {} by XBOOLE_0:def 1;
then A13: {1} misses X2 by XBOOLE_0:def 7;
X = {1} \/ X2 by ENUMSET1:42;
then A14: Sum ((EXP 1) | X) = (Sum ((EXP 1) | {1})) + (Sum ((EXP 1) | X2)) by A13, Th26
.= ((EXP 1) . 1) + (Sum ((EXP 1) | X2)) by Th27
.= ((EXP 1) . 1) + ((Sum ((EXP 1) | X3)) + (Sum ((EXP 1) | X4))) by A11, A12, Th26
.= ((EXP 1) . 1) + (((EXP 1) . m) + (Sum ((EXP 1) | X4))) by Th27
.= (((EXP 1) . 1) + ((EXP 1) . m)) + (Sum ((EXP 1) | X4))
.= (((EXP 1) . 1) + ((EXP 1) . m)) + ((EXP 1) . n0) by Th27
.= ((1 |^ 1) + ((EXP 1) . m)) + ((EXP 1) . n0) by Def1
.= ((1 |^ 1) + (m |^ 1)) + ((EXP 1) . n0) by Def1
.= ((1 |^ 1) + (m |^ 1)) + (n0 |^ 1) by Def1
.= (1 + (m |^ 1)) + (n0 |^ 1) by NEWTON:10
.= (1 + m) + (n0 |^ 1) by NEWTON:10
.= (1 + m) + n0 by NEWTON:10 ;
0 + (Sum ((EXP 1) | X)) <= (Sum ((EXP 1) | ((NatDivisors n0) \ X))) + (Sum ((EXP 1) | X)) by XREAL_1:9;
hence (1 + m) + n0 <= sigma n0 by A10, A14; :: thesis: verum

end;

end;