let n, r be Element of NAT ; 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; 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 ; ( 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
; ( 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
assume A4:
2 * n < p |^ (r + 1)
; ( 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
; ( 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))/])
; 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 ;
( k in dom f implies f . k <= ((r |-> 1) ^ (((2 * n) -' r) |-> 0)) . k )
assume A9:
k in dom f
;
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)
;
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;
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; verum