let n, r be Element of NAT ; :: thesis: for p being Prime
for f being FinSequence of REAL st p |^ r <= 2 * n & 2 * n < p |^ (r + 1) & len f = 2 * n & ( for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) holds
Sum f <= r
let p be Prime; :: thesis: for f being FinSequence of REAL st p |^ r <= 2 * n & 2 * n < p |^ (r + 1) & len f = 2 * n & ( for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) holds
Sum f <= r
let f be FinSequence of REAL ; :: thesis: ( p |^ r <= 2 * n & 2 * n < p |^ (r + 1) & len f = 2 * n & ( for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) implies Sum f <= r )
set f0 = (r |-> 1) ^ (((2 * n) -' r) |-> 0);
A1: p > 1 by INT_2:def 4;
assume A2: p |^ r <= 2 * n ; :: thesis: ( not 2 * n < p |^ (r + 1) or not len f = 2 * n or ex k being Element of NAT st
( k in dom f & not f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) or Sum f <= r )
A3: 2 * n >= r

proof

assume 2 * n < r ; :: thesis: contradiction
then p to_power (2 * n) < p to_power r by A1, POWER:39;
then p |^ (2 * n) < p to_power r by POWER:41;
then p |^ (2 * n) < p |^ r by POWER:41;
then p |^ (2 * n) < 2 * n by A2, XXREAL_0:2;
hence contradiction by A1, Th3; :: thesis: verum

end;

assume A4: 2 * n < p |^ (r + 1) ; :: thesis: ( not len f = 2 * n or ex k being Element of NAT st
( k in dom f & not f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) or Sum f <= r )
assume A5: len f = 2 * n ; :: thesis: ( ex k being Element of NAT st
( k in dom f & not f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) or Sum f <= r )
A6: len ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) = (len (r |-> 1)) + (len (((2 * n) -' r) |-> 0)) by FINSEQ_1:22
.= r + (len (((2 * n) -' r) |-> 0)) by CARD_1:def 7
.= r + ((2 * n) -' r) by CARD_1:def 7
.= r + ((2 * n) - r) by A3, XREAL_1:233
.= len f by A5 ;
assume A7: for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ; :: thesis: Sum f <= r
A8: for k being Element of NAT st k in dom f holds
f . k <= ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) . k

proof

let k be Element of NAT ; :: thesis: ( k in dom f implies f . k <= ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) . k )
assume A9: k in dom f ; :: thesis: f . k <= ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) . k
then A10: f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) by A7;
k in Seg (2 * n) by A5, A9, FINSEQ_1:def 3;
then A11: k in dom ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) by A5, A6, FINSEQ_1:def 3;

per cases ( k in dom (r |-> 1) or ex n0 being Nat st
( n0 in dom (((2 * n) -' r) |-> 0) & k = (len (r |-> 1)) + n0 ) ) by A11, FINSEQ_1:25;

suppose A12: k in dom (r |-> 1) ; :: thesis: f . k <= ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) . k

[\(n / (p |^ k))/] <= n / (p |^ k) by INT_1:def 6;
then - [\(n / (p |^ k))/] >= - (n / (p |^ k)) by XREAL_1:24;
then ( ((2 * n) / (p |^ k)) - 1 < [\((2 * n) / (p |^ k))/] & (- [\(n / (p |^ k))/]) * 2 >= (- (n / (p |^ k))) * 2 ) by INT_1:def 6, XREAL_1:64;
then (((2 * n) / (p |^ k)) - 1) + (2 * (- (n / (p |^ k)))) < [\((2 * n) / (p |^ k))/] + (- (2 * [\(n / (p |^ k))/])) by XREAL_1:8;
then [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) > ((2 * (n / (p |^ k))) - 1) + (2 * (- (n / (p |^ k)))) by XCMPLX_1:74;
then f . k >= (- 1) + 1 by A10, INT_1:7;
then A13: f . k is Element of NAT by A10, INT_1:3;
(n / (p |^ k)) - 1 < [\(n / (p |^ k))/] by INT_1:def 6;
then - [\(n / (p |^ k))/] < - ((n / (p |^ k)) - 1) by XREAL_1:24;
then ( [\((2 * n) / (p |^ k))/] <= (2 * n) / (p |^ k) & (- [\(n / (p |^ k))/]) * 2 < (- ((n / (p |^ k)) - 1)) * 2 ) by INT_1:def 6, XREAL_1:68;
then ( (2 * n) / (p |^ k) = 2 * (n / (p |^ k)) & (- (2 * [\(n / (p |^ k))/])) + [\((2 * n) / (p |^ k))/] < (2 * ((- (n / (p |^ k))) + 1)) + ((2 * n) / (p |^ k)) ) by XCMPLX_1:74, XREAL_1:8;
then A14: f . k < 1 + 1 by A10;
A15: k in Seg r by A12, FUNCOP_1:13;
((r |-> 1) ^ (((2 * n) -' r) |-> 0)) . k = (r |-> 1) . k by A12, FINSEQ_1:def 7
.= 1 by A15, FUNCOP_1:7 ;
hence f . k <= ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) . k by A13, A14, NAT_1:13; :: thesis: verum

end;

suppose A16: ex n0 being Nat st
( n0 in dom (((2 * n) -' r) |-> 0) & k = (len (r |-> 1)) + n0 ) ; :: thesis: f . k <= ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) . k

reconsider k1 = k as Element of NAT ;
consider n0 being Nat such that
A17: n0 in dom (((2 * n) -' r) |-> 0) and
A18: k = (len (r |-> 1)) + n0 by A16;
n0 in Seg ((2 * n) -' r) by A17, FUNCOP_1:13;
then 1 <= n0 by FINSEQ_1:1;
then A19: 1 + r <= n0 + r by XREAL_1:6;
k = r + n0 by A18, CARD_1:def 7;
then ( r + 1 < k or r + 1 = k ) by A19, XXREAL_0:1;
then p to_power (r + 1) <= p to_power k by A1, POWER:39;
then p |^ (r + 1) <= p to_power k by POWER:41;
then p |^ (r + 1) <= p |^ k1 by POWER:41;
then 2 * n < p |^ k by A4, XXREAL_0:2;
then (2 * n) / (p |^ k) < (p |^ k) / (p |^ k) by XREAL_1:74;
then A20: (2 * n) / (p |^ k) < 1 by XCMPLX_1:60;
then ((2 * n) / (p |^ k)) / 2 < 1 / 2 by XREAL_1:74;
then ((2 * n) / 2) / (p |^ k) < 1 / 2 by XCMPLX_1:48;
then n / (p |^ k) < 1 by XXREAL_0:2;
then (n / (p |^ k)) - 1 < 1 - 1 by XREAL_1:9;
then A21: [\(n / (p |^ k))/] = 0 by INT_1:def 6;
((2 * n) / (p |^ k)) - 1 < 1 - 1 by A20, XREAL_1:9;
hence f . k <= ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) . k by A10, A21, INT_1:def 6; :: thesis: verum

end;

end;

end;

A22: (r |-> 1) ^ (((2 * n) -' r) |-> 0) = (r |-> (In (1,REAL))) ^ (((2 * n) -' r) |-> (In (0,REAL))) ;
Sum ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) = (Sum (r |-> 1)) + (Sum (((2 * n) -' r) |-> 0)) by RVSUM_1:75
.= (r * 1) + (Sum (((2 * n) -' r) |-> 0)) by RVSUM_1:80
.= r + (((2 * n) -' r) * 0) by RVSUM_1:80
.= r ;
hence Sum f <= r by A6, A8, INTEGRA5:3, A22; :: thesis: verum