Metamath Proof Explorer

Theorem rplogcl

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

Ref Expression
Assertion rplogcl 
|- ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR+ )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR /\ 1 < A ) -> A e. RR )
2 0red 
 |-  ( ( A e. RR /\ 1 < A ) -> 0 e. RR )
3 1red 
 |-  ( ( A e. RR /\ 1 < A ) -> 1 e. RR )
4 0lt1 
 |-  0 < 1
5 4 a1i 
 |-  ( ( A e. RR /\ 1 < A ) -> 0 < 1 )
6 simpr 
 |-  ( ( A e. RR /\ 1 < A ) -> 1 < A )
7 2 3 1 5 6 lttrd 
 |-  ( ( A e. RR /\ 1 < A ) -> 0 < A )
8 1 7 elrpd 
 |-  ( ( A e. RR /\ 1 < A ) -> A e. RR+ )
9 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
10 8 9 syl 
 |-  ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR )
11 log1 
 |-  ( log ` 1 ) = 0
12 1rp 
 |-  1 e. RR+
13 logltb 
 |-  ( ( 1 e. RR+ /\ A e. RR+ ) -> ( 1 < A <-> ( log ` 1 ) < ( log ` A ) ) )
14 12 8 13 sylancr 
 |-  ( ( A e. RR /\ 1 < A ) -> ( 1 < A <-> ( log ` 1 ) < ( log ` A ) ) )
15 6 14 mpbid 
 |-  ( ( A e. RR /\ 1 < A ) -> ( log ` 1 ) < ( log ` A ) )
16 11 15 eqbrtrrid 
 |-  ( ( A e. RR /\ 1 < A ) -> 0 < ( log ` A ) )
17 10 16 elrpd 
 |-  ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR+ )