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

proof

let p be natural number ; :: 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 5;
then A2: p - 1 > 1 - 1 by XREAL_1:16;
thus sigma (p |^ 0 ) = sigma 1 by NEWTON:9
.= 1 by Th29
.= (p - 1) / (p - 1) by A2, XCMPLX_1:60
.= ((p |^ (0 + 1)) - 1) / (p - 1) by NEWTON:10 ; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

proof

let p be natural number ; :: thesis: ( p is prime implies sigma (p |^ (k + 1)) = ((p |^ ((k + 1) + 1)) - 1) / (p - 1) )
assume A5: p is prime ; :: thesis: sigma (p |^ (k + 1)) = ((p |^ ((k + 1) + 1)) - 1) / (p - 1)
then A6: p > 1 by INT_2:def 5;
then A7: p - 1 > 1 - 1 by XREAL_1:16;
reconsider m = p |^ (k + 1) as non zero natural number by A5;
reconsider m' = p |^ k as non zero natural number by A5;
reconsider k' = k + 1, p' = p as Element of NAT by ORDINAL1:def 13;
for x being set holds
( x in NatDivisors (p |^ (k + 1)) iff x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} )

proof

let x be set ; :: 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 A5, Th19;
then consider t being Element of NAT such that
A8: ( x = p |^ t & 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 |^ t') where t' is Element of NAT : t' <= k } by A8;
then x in NatDivisors (p |^ k) by A5, 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 A8, XXREAL_0:1;
then x in {(p |^ (k + 1))} by A8, TARSKI:def 1;
hence x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume A9: 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 A9, 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 A5, Th19;
then consider t being Element of NAT such that
A10: ( x = p |^ t & t <= k ) ;
0 + k <= 1 + k by XREAL_1:9;
then t <= k + 1 by A10, XXREAL_0:2;
then x in { (p |^ t') where t' is Element of NAT : t' <= k + 1 } by A10;
hence x in NatDivisors (p |^ (k + 1)) by A5, Th19; :: thesis: verum

end;

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

then ( x = p |^ k' & k' <= k + 1 ) 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 A5, Th19; :: thesis: verum

end;

end;

end;

then A11: NatDivisors (p |^ (k + 1)) = (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))} by TARSKI:2;
reconsider J = NatDivisors (p |^ k) as finite Subset of NAT by A5;
p' |^ k' in NAT ;
then reconsider K = {(p |^ (k + 1))} as finite Subset of NAT by ZFMISC_1:37;

now

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

end;

then J /\ K = {} by XBOOLE_0:def 1;
then A14: J misses K by XBOOLE_0:def 7;
A15: sigma 1,m = Sum ((EXP 1) | (J \/ K)) by Def2, A11
.= (Sum ((EXP 1) | J)) + (Sum ((EXP 1) | K)) by A14, Th26
.= (Sum ((EXP 1) | J)) + ((EXP 1) . (p |^ (k + 1))) by Th27 ;
A16: (EXP 1) . (p |^ (k + 1)) = (p |^ (k + 1)) |^ 1 by Def1
.= p |^ ((k + 1) * 1) by NEWTON:14
.= p |^ (k + 1) ;
A17: Sum ((EXP 1) | J) = sigma 1,m' by Def2
.= sigma (p |^ k)
.= ((p |^ (k + 1)) - 1) / (p - 1) by A4, A5 ;
thus sigma (p |^ (k + 1)) = (((p |^ (k + 1)) - 1) / (p - 1)) + (((p |^ (k + 1)) * (p - 1)) / (p - 1)) by A15, A16, A17, A7, XCMPLX_1:90
.= (((p |^ (k + 1)) - 1) + ((p |^ (k + 1)) * (p - 1))) / (p - 1) by XCMPLX_1:63
.= (((p |^ (k + 1)) * p) - 1) / (p - 1)
.= ((p |^ ((k + 1) + 1)) - 1) / (p - 1) by NEWTON:11 ; :: thesis: verum

end;

end;

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