let k, m be Nat; :: thesis: for n0 being non zero Nat st m divides n0 & k divides n0 & n0 <> m & n0 <> k & m <> 1 & k <> 1 & m <> k holds
((1 + m) + k) + n0 <= sigma n0
let n0 be non zero Nat; :: thesis: ( m divides n0 & k divides n0 & n0 <> m & n0 <> k & m <> 1 & k <> 1 & m <> k implies ((1 + m) + k) + n0 <= sigma n0 )
assume that
A1: m divides n0 and
A2: k divides n0 and
A3: n0 <> m and
A4: n0 <> k and
A5: m <> 1 and
A6: k <> 1 and
A7: m <> k ; :: thesis: ((1 + m) + k) + n0 <= sigma n0

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

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

hence ((1 + m) + k) + n0 <= sigma n0 by A1, A3, WSIERP_1:15; :: thesis: verum

end;

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

reconsider X2 = {m,k,n0} as finite Subset of NAT by Lm2;
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 A9: x in {1} /\ X2 ; :: thesis: contradiction
then x in {1} by XBOOLE_0:def 4;
then A10: x = 1 by TARSKI:def 1;
x in X2 by A9, XBOOLE_0:def 4;
hence contradiction by A5, A6, A8, A10, ENUMSET1:def 1; :: thesis: verum

end;

then {1} /\ X2 = {} by XBOOLE_0:def 1;
then A11: {1} misses X2 by XBOOLE_0:def 7;
reconsider X5 = {m} as finite Subset of NAT by Th4;
reconsider X4 = {n0} as finite Subset of NAT by Th4;
reconsider X6 = {k} as finite Subset of NAT by Th4;
reconsider X3 = {m,k} as finite Subset of NAT by Th5;
reconsider X = {1,m,k,n0} as finite Subset of NAT by Lm3;
set Y = (NatDivisors n0) \ X;
A12: 0 + (Sum ((EXP 1) | X)) <= (Sum ((EXP 1) | ((NatDivisors n0) \ X))) + (Sum ((EXP 1) | X)) by XREAL_1:7;

now :: thesis: for x being object holds not x in X5 /\ X6

let x be object ; :: thesis: not x in X5 /\ X6
assume A13: x in X5 /\ X6 ; :: thesis: contradiction
then x in X5 by XBOOLE_0:def 4;
then A14: x = m by TARSKI:def 1;
x in X6 by A13, XBOOLE_0:def 4;
hence contradiction by A7, A14, TARSKI:def 1; :: thesis: verum

end;

then X5 /\ X6 = {} by XBOOLE_0:def 1;
then A15: ( X3 = X5 \/ X6 & X5 misses X6 ) by ENUMSET1:1, XBOOLE_0:def 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 A16: x in X ; :: thesis: x in NatDivisors n0
then reconsider x9 = x as Element of NAT ;
( x = 1 or x = m or x = k or x = n0 ) by A16, ENUMSET1:def 2;
then ( x9 <> 0 & x9 divides n0 ) by A1, A2, 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 A17: 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 A18: x in X3 /\ X4 ; :: thesis: contradiction
then x in X4 by XBOOLE_0:def 4;
then A19: x = n0 by TARSKI:def 1;
x in X3 by A18, XBOOLE_0:def 4;
hence contradiction by A3, A4, A19, TARSKI:def 2; :: thesis: verum

end;

then X3 /\ X4 = {} by XBOOLE_0:def 1;
then A20: ( X2 = X3 \/ X4 & X3 misses X4 ) by ENUMSET1:3, XBOOLE_0:def 7;
X = {1} \/ X2 by ENUMSET1:4;
then Sum ((EXP 1) | X) = (Sum ((EXP 1) | {1})) + (Sum ((EXP 1) | X2)) by A11, Th26
.= ((EXP 1) . 1) + (Sum ((EXP 1) | X2)) by Th27
.= ((EXP 1) . 1) + ((Sum ((EXP 1) | X3)) + (Sum ((EXP 1) | X4))) by A20, Th26
.= ((EXP 1) . 1) + (((Sum ((EXP 1) | X5)) + (Sum ((EXP 1) | X6))) + (Sum ((EXP 1) | X4))) by A15, Th26
.= ((EXP 1) . 1) + ((((EXP 1) . m) + (Sum ((EXP 1) | X6))) + (Sum ((EXP 1) | X4))) by Th27
.= (((EXP 1) . 1) + ((EXP 1) . m)) + ((Sum ((EXP 1) | X6)) + (Sum ((EXP 1) | X4)))
.= (((EXP 1) . 1) + ((EXP 1) . m)) + (((EXP 1) . k) + (Sum ((EXP 1) | X4))) by Th27
.= ((((EXP 1) . 1) + ((EXP 1) . m)) + ((EXP 1) . k)) + (Sum ((EXP 1) | X4))
.= ((((EXP 1) . 1) + ((EXP 1) . m)) + ((EXP 1) . k)) + ((EXP 1) . n0) by Th27
.= (((1 |^ 1) + ((EXP 1) . m)) + ((EXP 1) . k)) + ((EXP 1) . n0) by Def1
.= (((1 |^ 1) + (m |^ 1)) + ((EXP 1) . k)) + ((EXP 1) . n0) by Def1
.= (((1 |^ 1) + (m |^ 1)) + (k |^ 1)) + ((EXP 1) . n0) by Def1
.= (((1 |^ 1) + (m |^ 1)) + (k |^ 1)) + (n0 |^ 1) by Def1
.= ((1 + (m |^ 1)) + (k |^ 1)) + (n0 |^ 1)
.= ((1 + m) + (k |^ 1)) + (n0 |^ 1)
.= ((1 + m) + k) + (n0 |^ 1)
.= ((1 + m) + k) + n0 ;
hence ((1 + m) + k) + n0 <= sigma n0 by A17, A12; :: thesis: verum

end;

end;