Metamath Proof Explorer

Theorem chpo1ubb

Description: The psi function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Assertion chpo1ubb 
|- E. c e. RR+ A. x e. RR+ ( psi ` x ) <_ ( c x. x )

Proof

Step Hyp Ref Expression
1 rpssre 
 |-  RR+ C_ RR
2 1 a1i 
 |-  ( T. -> RR+ C_ RR )
3 1red 
 |-  ( T. -> 1 e. RR )
4 simpr 
 |-  ( ( T. /\ x e. RR+ ) -> x e. RR+ )
5 4 rpred 
 |-  ( ( T. /\ x e. RR+ ) -> x e. RR )
6 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
7 5 6 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( psi ` x ) e. RR )
8 7 4 rerpdivcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. RR )
9 chpo1ub 
 |-  ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1)
10 9 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) )
11 8 10 o1lo1d 
 |-  ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. <_O(1) )
12 chpcl 
 |-  ( y e. RR -> ( psi ` y ) e. RR )
13 12 ad2antrl 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( psi ` y ) e. RR )
14 13 rehalfcld 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( ( psi ` y ) / 2 ) e. RR )
15 5 adantr 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR )
16 chpeq0 
 |-  ( x e. RR -> ( ( psi ` x ) = 0 <-> x < 2 ) )
17 15 16 syl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( psi ` x ) = 0 <-> x < 2 ) )
18 17 biimpar 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ x < 2 ) -> ( psi ` x ) = 0 )
19 18 oveq1d 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ x < 2 ) -> ( ( psi ` x ) / x ) = ( 0 / x ) )
20 4 adantr 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR+ )
21 20 rpcnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. CC )
22 20 rpne0d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x =/= 0 )
23 21 22 div0d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 0 / x ) = 0 )
24 13 ad2ant2r 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( psi ` y ) e. RR )
25 2rp 
 |-  2 e. RR+
26 25 a1i 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 2 e. RR+ )
27 simprll 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR )
28 chpge0 
 |-  ( y e. RR -> 0 <_ ( psi ` y ) )
29 27 28 syl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( psi ` y ) )
30 24 26 29 divge0d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( ( psi ` y ) / 2 ) )
31 23 30 eqbrtrd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 0 / x ) <_ ( ( psi ` y ) / 2 ) )
32 31 adantr 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ x < 2 ) -> ( 0 / x ) <_ ( ( psi ` y ) / 2 ) )
33 19 32 eqbrtrd 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ x < 2 ) -> ( ( psi ` x ) / x ) <_ ( ( psi ` y ) / 2 ) )
34 7 ad2antrr 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> ( psi ` x ) e. RR )
35 24 adantr 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> ( psi ` y ) e. RR )
36 25 a1i 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> 2 e. RR+ )
37 15 adantr 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> x e. RR )
38 chpge0 
 |-  ( x e. RR -> 0 <_ ( psi ` x ) )
39 37 38 syl 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> 0 <_ ( psi ` x ) )
40 27 adantr 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> y e. RR )
41 simprr 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x < y )
42 15 27 41 ltled 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x <_ y )
43 42 adantr 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> x <_ y )
44 chpwordi 
 |-  ( ( x e. RR /\ y e. RR /\ x <_ y ) -> ( psi ` x ) <_ ( psi ` y ) )
45 37 40 43 44 syl3anc 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> ( psi ` x ) <_ ( psi ` y ) )
46 simpr 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> 2 <_ x )
47 34 35 36 37 39 45 46 lediv12ad 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ 2 <_ x ) -> ( ( psi ` x ) / x ) <_ ( ( psi ` y ) / 2 ) )
48 2re 
 |-  2 e. RR
49 48 a1i 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 2 e. RR )
50 33 47 15 49 ltlecasei 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( psi ` x ) / x ) <_ ( ( psi ` y ) / 2 ) )
51 2 3 8 11 14 50 lo1bddrp 
 |-  ( T. -> E. c e. RR+ A. x e. RR+ ( ( psi ` x ) / x ) <_ c )
52 51 mptru 
 |-  E. c e. RR+ A. x e. RR+ ( ( psi ` x ) / x ) <_ c
53 simpr 
 |-  ( ( c e. RR+ /\ x e. RR+ ) -> x e. RR+ )
54 53 rpred 
 |-  ( ( c e. RR+ /\ x e. RR+ ) -> x e. RR )
55 54 6 syl 
 |-  ( ( c e. RR+ /\ x e. RR+ ) -> ( psi ` x ) e. RR )
56 simpl 
 |-  ( ( c e. RR+ /\ x e. RR+ ) -> c e. RR+ )
57 56 rpred 
 |-  ( ( c e. RR+ /\ x e. RR+ ) -> c e. RR )
58 55 57 53 ledivmul2d 
 |-  ( ( c e. RR+ /\ x e. RR+ ) -> ( ( ( psi ` x ) / x ) <_ c <-> ( psi ` x ) <_ ( c x. x ) ) )
59 58 ralbidva 
 |-  ( c e. RR+ -> ( A. x e. RR+ ( ( psi ` x ) / x ) <_ c <-> A. x e. RR+ ( psi ` x ) <_ ( c x. x ) ) )
60 59 rexbiia 
 |-  ( E. c e. RR+ A. x e. RR+ ( ( psi ` x ) / x ) <_ c <-> E. c e. RR+ A. x e. RR+ ( psi ` x ) <_ ( c x. x ) )
61 52 60 mpbi 
 |-  E. c e. RR+ A. x e. RR+ ( psi ` x ) <_ ( c x. x )