This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chtrpcl

Description: Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chtrpcl 
|- ( ( A e. RR /\ 2 <_ A ) -> ( theta ` A ) e. RR+ )

Proof

Step Hyp Ref Expression
1 chtcl 
 |-  ( A e. RR -> ( theta ` A ) e. RR )
2 1 adantr 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( theta ` A ) e. RR )
3 0red 
 |-  ( ( A e. RR /\ 2 <_ A ) -> 0 e. RR )
4 2re 
 |-  2 e. RR
5 1lt2 
 |-  1 < 2
6 rplogcl 
 |-  ( ( 2 e. RR /\ 1 < 2 ) -> ( log ` 2 ) e. RR+ )
7 4 5 6 mp2an 
 |-  ( log ` 2 ) e. RR+
8 rpre 
 |-  ( ( log ` 2 ) e. RR+ -> ( log ` 2 ) e. RR )
9 7 8 mp1i 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( log ` 2 ) e. RR )
10 rpgt0 
 |-  ( ( log ` 2 ) e. RR+ -> 0 < ( log ` 2 ) )
11 7 10 mp1i 
 |-  ( ( A e. RR /\ 2 <_ A ) -> 0 < ( log ` 2 ) )
12 cht2 
 |-  ( theta ` 2 ) = ( log ` 2 )
13 chtwordi 
 |-  ( ( 2 e. RR /\ A e. RR /\ 2 <_ A ) -> ( theta ` 2 ) <_ ( theta ` A ) )
14 4 13 mp3an1 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( theta ` 2 ) <_ ( theta ` A ) )
15 12 14 eqbrtrrid 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( log ` 2 ) <_ ( theta ` A ) )
16 3 9 2 11 15 ltletrd 
 |-  ( ( A e. RR /\ 2 <_ A ) -> 0 < ( theta ` A ) )
17 2 16 elrpd 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( theta ` A ) e. RR+ )