Metamath Proof Explorer

Theorem pntrlog2bndlem6a

Description: Lemma for pntrlog2bndlem6 . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses pntsval.1 
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
pntrlog2bnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntrlog2bnd.t 
|- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )
pntrlog2bndlem5.1 
|- ( ph -> B e. RR+ )
pntrlog2bndlem5.2 
|- ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
pntrlog2bndlem6.1 
|- ( ph -> A e. RR )
pntrlog2bndlem6.2 
|- ( ph -> 1 <_ A )
Assertion pntrlog2bndlem6a 
|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( ( 1 ... ( |_ ` ( x / A ) ) ) u. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 pntsval.1 
 |-  S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
2 pntrlog2bnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
3 pntrlog2bnd.t 
 |-  T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )
4 pntrlog2bndlem5.1 
 |-  ( ph -> B e. RR+ )
5 pntrlog2bndlem5.2 
 |-  ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
6 pntrlog2bndlem6.1 
 |-  ( ph -> A e. RR )
7 pntrlog2bndlem6.2 
 |-  ( ph -> 1 <_ A )
8 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
9 8 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
10 1rp 
 |-  1 e. RR+
11 10 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
12 11 rpred 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
13 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
14 13 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
15 14 simpld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
16 12 9 15 ltled 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
17 9 11 16 rpgecld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
18 10 a1i 
 |-  ( ph -> 1 e. RR+ )
19 6 18 7 rpgecld 
 |-  ( ph -> A e. RR+ )
20 19 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR+ )
21 17 20 rpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / A ) e. RR+ )
22 21 rprege0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( x / A ) e. RR /\ 0 <_ ( x / A ) ) )
23 flge0nn0 
 |-  ( ( ( x / A ) e. RR /\ 0 <_ ( x / A ) ) -> ( |_ ` ( x / A ) ) e. NN0 )
24 nn0p1nn 
 |-  ( ( |_ ` ( x / A ) ) e. NN0 -> ( ( |_ ` ( x / A ) ) + 1 ) e. NN )
25 22 23 24 3syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` ( x / A ) ) + 1 ) e. NN )
26 nnuz 
 |-  NN = ( ZZ>= ` 1 )
27 25 26 eleqtrdi 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` ( x / A ) ) + 1 ) e. ( ZZ>= ` 1 ) )
28 21 rpred 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / A ) e. RR )
29 17 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ x )
30 7 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ A )
31 11 20 9 29 30 lediv2ad 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / A ) <_ ( x / 1 ) )
32 9 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
33 32 div1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / 1 ) = x )
34 31 33 breqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / A ) <_ x )
35 flword2 
 |-  ( ( ( x / A ) e. RR /\ x e. RR /\ ( x / A ) <_ x ) -> ( |_ ` x ) e. ( ZZ>= ` ( |_ ` ( x / A ) ) ) )
36 28 9 34 35 syl3anc 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. ( ZZ>= ` ( |_ ` ( x / A ) ) ) )
37 fzsplit2 
 |-  ( ( ( ( |_ ` ( x / A ) ) + 1 ) e. ( ZZ>= ` 1 ) /\ ( |_ ` x ) e. ( ZZ>= ` ( |_ ` ( x / A ) ) ) ) -> ( 1 ... ( |_ ` x ) ) = ( ( 1 ... ( |_ ` ( x / A ) ) ) u. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) )
38 27 36 37 syl2anc 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( ( 1 ... ( |_ ` ( x / A ) ) ) u. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) )