let n, p be Nat; :: thesis: ( p is prime implies sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1) )

defpred S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A17, A1);

hence ( p is prime implies sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1) ) ; :: thesis: verum

defpred S

sigma (p |^ $1) = ((p |^ ($1 + 1)) - 1) / (p - 1);

A1: for k being Nat st S

S

proof

A17:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A2: S

thus S

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;

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

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

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

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

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

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

assume A14:
x in (NatDivisors (p |^ k)) \/ {(p |^ (k + 1))}
; :: thesis: 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 ;

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

end;

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

end;

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

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

proof

for k being Nat holds S
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;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

hence ( p is prime implies sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1) ) ; :: thesis: verum