let n, p be Nat; :: thesis: ( p is prime implies sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1) )
defpred S₁[ Nat] means for p being Nat st p is prime holds
sigma (p |^ $1) = ((p |^ ($1 + 1)) - 1) / (p - 1);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let p be Nat; :: thesis: ( p is prime implies sigma (p |^ (k + 1)) = ((p |^ ((k + 1) + 1)) - 1) / (p - 1) )
reconsider k9 = k + 1, p9 = p as Element of NAT by ORDINAL1:def 12;
assume A3: p is prime ; :: thesis: sigma (p |^ (k + 1)) = ((p |^ ((k + 1) + 1)) - 1) / (p - 1)
then reconsider J = NatDivisors (p |^ k) as finite Subset of NAT ;
reconsider m9 = p |^ k as non zero Nat by A3;
A4: Sum ((EXP 1) | J) = sigma (1,m9) by Def2
.= sigma (p |^ k)
.= ((p |^ (k + 1)) - 1) / (p - 1) by A2, A3 ;
p9 |^ k9 in NAT ;
then reconsider K = {(p |^ (k + 1))} as finite Subset of NAT by ZFMISC_1:31;
A5: p > 1 by A3, INT_2:def 4;
then A6: p - 1 > 1 - 1 by XREAL_1:14;

now :: thesis: for x being object holds not x in J /\ K

let x be object ; :: thesis: not x in J /\ K
assume A7: x in J /\ K ; :: thesis: contradiction
then x in J by XBOOLE_0:def 4;
then x in { (p |^ t) where t is Element of NAT : t <= k } by A3, Th19;
then consider t being Element of NAT such that
A8: x = p |^ t and
A9: t <= k ;
x in K by A7, XBOOLE_0:def 4;
then p |^ (k + 1) = p |^ t by A8, TARSKI:def 1;
then p |-count (p |^ (k + 1)) = t by A5, NAT_3:25;
then k + 1 = t by A5, NAT_3:25;
then (k + 1) - k <= k - k by A9, XREAL_1:9;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum

end;

then J /\ K = {} by XBOOLE_0:def 1;
then A10: J misses K by XBOOLE_0:def 7;
reconsider m = p |^ (k + 1) as non zero Nat by A3;
A11: (EXP 1) . (p |^ (k + 1)) = (p |^ (k + 1)) |^ 1 by Def1
.= p |^ ((k + 1) * 1)
.= p |^ (k + 1) ;
for x being object holds
( x in NatDivisors (p |^ (k + 1)) iff x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} )

proof

let x be object ; :: thesis: ( x in NatDivisors (p |^ (k + 1)) iff x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} )

hereby :: thesis: ( x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} implies x in NatDivisors (p |^ (k + 1)) )

assume x in NatDivisors (p |^ (k + 1)) ; :: thesis: x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))}
then x in { (p |^ t) where t is Element of NAT : t <= k + 1 } by A3, Th19;
then consider t being Element of NAT such that
A12: x = p |^ t and
A13: t <= k + 1 ;

per cases ( t <= k or t > k ) ;

suppose t <= k ; :: thesis: x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))}

then x in { (p |^ t9) where t9 is Element of NAT : t9 <= k } by A12;
then x in NatDivisors (p |^ k) by A3, Th19;
hence x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose t > k ; :: thesis: x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))}

then t >= k + 1 by NAT_1:13;
then t = k + 1 by A13, XXREAL_0:1;
then x in {(p |^ (k + 1))} by A12, TARSKI:def 1;
hence x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume A14: x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} ; :: thesis: x in NatDivisors (p |^ (k + 1))

per cases ( x in NatDivisors (p |^ k) or x in {(p |^ (k + 1))} ) by A14, XBOOLE_0:def 3;

suppose x in NatDivisors (p |^ k) ; :: thesis: x in NatDivisors (p |^ (k + 1))

then x in { (p |^ t) where t is Element of NAT : t <= k } by A3, Th19;
then consider t being Element of NAT such that
A15: x = p |^ t and
A16: t <= k ;
0 + k <= 1 + k by XREAL_1:7;
then t <= k + 1 by A16, XXREAL_0:2;
then x in { (p |^ t9) where t9 is Element of NAT : t9 <= k + 1 } by A15;
hence x in NatDivisors (p |^ (k + 1)) by A3, Th19; :: thesis: verum

end;

suppose x in {(p |^ (k + 1))} ; :: thesis: x in NatDivisors (p |^ (k + 1))

then x = p |^ k9 by TARSKI:def 1;
then x in { (p |^ t) where t is Element of NAT : t <= k + 1 } ;
hence x in NatDivisors (p |^ (k + 1)) by A3, Th19; :: thesis: verum

end;

end;

end;

then NatDivisors (p |^ (k + 1)) = (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} by TARSKI:2;
then sigma (1,m) = Sum ((EXP 1) | (J \/ K)) by Def2
.= (Sum ((EXP 1) | J)) + (Sum ((EXP 1) | K)) by A10, Th26
.= (Sum ((EXP 1) | J)) + ((EXP 1) . (p |^ (k + 1))) by Th27 ;
hence sigma (p |^ (k + 1)) = (((p |^ (k + 1)) - 1) / (p - 1)) + (((p |^ (k + 1)) * (p - 1)) / (p - 1)) by A6, A11, A4, XCMPLX_1:89
.= (((p |^ (k + 1)) - 1) + ((p |^ (k + 1)) * (p - 1))) / (p - 1) by XCMPLX_1:62
.= (((p |^ (k + 1)) * p) - 1) / (p - 1)
.= ((p |^ ((k + 1) + 1)) - 1) / (p - 1) by NEWTON:6 ;
:: thesis: verum

end;

end;

A17: S₁[ 0 ]

proof

let p be Nat; :: thesis: ( p is prime implies sigma (p |^ 0) = ((p |^ (0 + 1)) - 1) / (p - 1) )
assume p is prime ; :: thesis: sigma (p |^ 0) = ((p |^ (0 + 1)) - 1) / (p - 1)
then p > 1 by INT_2:def 4;
then A18: p - 1 > 1 - 1 by XREAL_1:14;
thus sigma (p |^ 0) = sigma 1 by NEWTON:4
.= 1 by Th29
.= (p - 1) / (p - 1) by A18, XCMPLX_1:60
.= ((p |^ (0 + 1)) - 1) / (p - 1) ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A17, A1);
hence ( p is prime implies sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1) ) ; :: thesis: verum