let m be Nat; :: thesis: for n0 being non zero Nat st m divides n0 & n0 <> m & m <> 1 holds
(1 + m) + n0 <= sigma n0
let n0 be non zero Nat; :: 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 A1, A2, WSIERP_1:15; :: thesis: verum

end;

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

reconsider X2 = {m,n0} as finite Subset of NAT by Th5;
set X1 = {1};

now :: thesis: for x being object holds not x in {1} /\ X2

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

end;

then {1} /\ X2 = {} by XBOOLE_0:def 1;
then A7: {1} misses X2 by XBOOLE_0:def 7;
reconsider X4 = {n0} as finite Subset of NAT by Th4;
reconsider X3 = {m} as finite Subset of NAT by Th4;
reconsider X = {1,m,n0} as finite Subset of NAT by Lm2;
set Y = (NatDivisors n0) \ X;
A8: 0 + (Sum ((EXP 1) | X)) <= (Sum ((EXP 1) | ((NatDivisors n0) \ X))) + (Sum ((EXP 1) | X)) by XREAL_1:7;
for x being object st x in X holds
x in NatDivisors n0

proof

let x be object ; :: thesis: ( x in X implies x in NatDivisors n0 )
assume A9: x in X ; :: thesis: x in NatDivisors n0
then reconsider x9 = x as Element of NAT ;
( x = 1 or x = m or x = n0 ) by A9, ENUMSET1:def 1;
then ( x9 <> 0 & x9 divides n0 ) by A1, INT_2:3, NAT_D:6;
hence x in NatDivisors n0 ; :: thesis: verum

end;

then X c= NatDivisors n0 ;
then NatDivisors n0 = X \/ ((NatDivisors n0) \ X) by XBOOLE_1:45;
then A10: sigma n0 = Sum ((EXP 1) | (X \/ ((NatDivisors n0) \ X))) by Def2
.= (Sum ((EXP 1) | X)) + (Sum ((EXP 1) | ((NatDivisors n0) \ X))) by Th26, XBOOLE_1:79 ;

now :: thesis: for x being object holds not x in X3 /\ X4

let x be object ; :: thesis: not x in X3 /\ X4
assume A11: x in X3 /\ X4 ; :: thesis: contradiction
then x in X3 by XBOOLE_0:def 4;
then A12: x = m by TARSKI:def 1;
x in X4 by A11, XBOOLE_0:def 4;
hence contradiction by A2, A12, TARSKI:def 1; :: thesis: verum

end;

then X3 /\ X4 = {} by XBOOLE_0:def 1;
then A13: ( X2 = X3 \/ X4 & X3 misses X4 ) by ENUMSET1:1, XBOOLE_0:def 7;
X = {1} \/ X2 by ENUMSET1:2;
then Sum ((EXP 1) | X) = (Sum ((EXP 1) | {1})) + (Sum ((EXP 1) | X2)) by A7, Th26
.= ((EXP 1) . 1) + (Sum ((EXP 1) | X2)) by Th27
.= ((EXP 1) . 1) + ((Sum ((EXP 1) | X3)) + (Sum ((EXP 1) | X4))) by A13, 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)
.= (1 + m) + (n0 |^ 1)
.= (1 + m) + n0 ;
hence (1 + m) + n0 <= sigma n0 by A10, A8; :: thesis: verum

end;

end;