Metamath Proof Explorer

Theorem chpo1ub

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

Ref Expression
Assertion chpo1ub 
|- ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 elicopnf 
 |-  ( 2 e. RR -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) ) )
3 1 2 ax-mp 
 |-  ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
4 chtrpcl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( theta ` x ) e. RR+ )
5 3 4 sylbi 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) e. RR+ )
6 5 rpcnne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) )
7 3 simplbi 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR )
8 0red 
 |-  ( x e. ( 2 [,) +oo ) -> 0 e. RR )
9 1 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 2 e. RR )
10 2pos 
 |-  0 < 2
11 10 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < 2 )
12 3 simprbi 
 |-  ( x e. ( 2 [,) +oo ) -> 2 <_ x )
13 8 9 7 11 12 ltletrd 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < x )
14 7 13 elrpd 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR+ )
15 14 rpcnne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( x e. CC /\ x =/= 0 ) )
16 rpre 
 |-  ( x e. RR+ -> x e. RR )
17 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
18 16 17 syl 
 |-  ( x e. RR+ -> ( psi ` x ) e. RR )
19 18 recnd 
 |-  ( x e. RR+ -> ( psi ` x ) e. CC )
20 14 19 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( psi ` x ) e. CC )
21 dmdcan 
 |-  ( ( ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) /\ ( x e. CC /\ x =/= 0 ) /\ ( psi ` x ) e. CC ) -> ( ( ( theta ` x ) / x ) x. ( ( psi ` x ) / ( theta ` x ) ) ) = ( ( psi ` x ) / x ) )
22 6 15 20 21 syl3anc 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( theta ` x ) / x ) x. ( ( psi ` x ) / ( theta ` x ) ) ) = ( ( psi ` x ) / x ) )
23 22 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( theta ` x ) / x ) x. ( ( psi ` x ) / ( theta ` x ) ) ) = ( ( psi ` x ) / x ) )
24 23 mpteq2dva 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( ( theta ` x ) / x ) x. ( ( psi ` x ) / ( theta ` x ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / x ) ) )
25 ovexd 
 |-  ( T. -> ( 2 [,) +oo ) e. _V )
26 ovexd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / x ) e. _V )
27 ovexd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( psi ` x ) / ( theta ` x ) ) e. _V )
28 eqidd 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) )
29 eqidd 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) )
30 25 26 27 28 29 offval2 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ( theta ` x ) / x ) x. ( ( psi ` x ) / ( theta ` x ) ) ) ) )
31 14 ssriv 
 |-  ( 2 [,) +oo ) C_ RR+
32 resmpt 
 |-  ( ( 2 [,) +oo ) C_ RR+ -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) |` ( 2 [,) +oo ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / x ) ) )
33 31 32 mp1i 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) |` ( 2 [,) +oo ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / x ) ) )
34 24 30 33 3eqtr4rd 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) |` ( 2 [,) +oo ) ) = ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ) )
35 31 a1i 
 |-  ( T. -> ( 2 [,) +oo ) C_ RR+ )
36 chto1ub 
 |-  ( x e. RR+ |-> ( ( theta ` x ) / x ) ) e. O(1)
37 36 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( theta ` x ) / x ) ) e. O(1) )
38 35 37 o1res2 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) e. O(1) )
39 chpchtlim 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ~~>r 1
40 rlimo1 
 |-  ( ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ~~>r 1 -> ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) e. O(1) )
41 39 40 ax-mp 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) e. O(1)
42 o1mul 
 |-  ( ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) e. O(1) /\ ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) e. O(1) ) -> ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ) e. O(1) )
43 38 41 42 sylancl 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ) e. O(1) )
44 34 43 eqeltrd 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) |` ( 2 [,) +oo ) ) e. O(1) )
45 rerpdivcl 
 |-  ( ( ( psi ` x ) e. RR /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. RR )
46 18 45 mpancom 
 |-  ( x e. RR+ -> ( ( psi ` x ) / x ) e. RR )
47 46 recnd 
 |-  ( x e. RR+ -> ( ( psi ` x ) / x ) e. CC )
48 47 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. CC )
49 48 fmpttd 
 |-  ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) : RR+ --> CC )
50 rpssre 
 |-  RR+ C_ RR
51 50 a1i 
 |-  ( T. -> RR+ C_ RR )
52 1 a1i 
 |-  ( T. -> 2 e. RR )
53 49 51 52 o1resb 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) <-> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) |` ( 2 [,) +oo ) ) e. O(1) ) )
54 44 53 mpbird 
 |-  ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) )
55 54 mptru 
 |-  ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1)