Metamath Proof Explorer

Theorem pntibndlem2a

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

Ref Expression
Hypotheses pntibnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntibndlem1.1 
|- ( ph -> A e. RR+ )
pntibndlem1.l 
|- L = ( ( 1 / 4 ) / ( A + 3 ) )
pntibndlem3.2 
|- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
pntibndlem3.3 
|- ( ph -> B e. RR+ )
pntibndlem3.k 
|- K = ( exp ` ( B / ( E / 2 ) ) )
pntibndlem3.c 
|- C = ( ( 2 x. B ) + ( log ` 2 ) )
pntibndlem3.4 
|- ( ph -> E e. ( 0 (,) 1 ) )
pntibndlem3.6 
|- ( ph -> Z e. RR+ )
pntibndlem2.10 
|- ( ph -> N e. NN )
Assertion pntibndlem2a 
|- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u e. RR /\ N <_ u /\ u <_ ( ( 1 + ( L x. E ) ) x. N ) ) )

Proof

Step Hyp Ref Expression
1 pntibnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntibndlem1.1 
 |-  ( ph -> A e. RR+ )
3 pntibndlem1.l 
 |-  L = ( ( 1 / 4 ) / ( A + 3 ) )
4 pntibndlem3.2 
 |-  ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
5 pntibndlem3.3 
 |-  ( ph -> B e. RR+ )
6 pntibndlem3.k 
 |-  K = ( exp ` ( B / ( E / 2 ) ) )
7 pntibndlem3.c 
 |-  C = ( ( 2 x. B ) + ( log ` 2 ) )
8 pntibndlem3.4 
 |-  ( ph -> E e. ( 0 (,) 1 ) )
9 pntibndlem3.6 
 |-  ( ph -> Z e. RR+ )
10 pntibndlem2.10 
 |-  ( ph -> N e. NN )
11 10 nnred 
 |-  ( ph -> N e. RR )
12 1red 
 |-  ( ph -> 1 e. RR )
13 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
14 1 2 3 pntibndlem1 
 |-  ( ph -> L e. ( 0 (,) 1 ) )
15 13 14 sselid 
 |-  ( ph -> L e. RR )
16 13 8 sselid 
 |-  ( ph -> E e. RR )
17 15 16 remulcld 
 |-  ( ph -> ( L x. E ) e. RR )
18 12 17 readdcld 
 |-  ( ph -> ( 1 + ( L x. E ) ) e. RR )
19 18 11 remulcld 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. N ) e. RR )
20 elicc2 
 |-  ( ( N e. RR /\ ( ( 1 + ( L x. E ) ) x. N ) e. RR ) -> ( u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) <-> ( u e. RR /\ N <_ u /\ u <_ ( ( 1 + ( L x. E ) ) x. N ) ) ) )
21 11 19 20 syl2anc 
 |-  ( ph -> ( u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) <-> ( u e. RR /\ N <_ u /\ u <_ ( ( 1 + ( L x. E ) ) x. N ) ) ) )
22 21 biimpa 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u e. RR /\ N <_ u /\ u <_ ( ( 1 + ( L x. E ) ) x. N ) ) )