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

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

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

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

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 ;

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

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

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

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

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

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