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+ )