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

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

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};

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;

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

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 ;

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;set X1 = {1};

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

then
{1} /\ X2 = {}
by XBOOLE_0:def 1;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;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

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

then
X5 /\ X6 = {}
by XBOOLE_0:def 1;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;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

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

then
X c= NatDivisors n0
;
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;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

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

then
X3 /\ X4 = {}
by XBOOLE_0:def 1;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;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

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