Step |
Hyp |
Ref |
Expression |
1 |
|
rpcn |
|- ( A e. RR+ -> A e. CC ) |
2 |
|
1cnd |
|- ( A e. RR+ -> 1 e. CC ) |
3 |
|
rpne0 |
|- ( A e. RR+ -> A =/= 0 ) |
4 |
1 2 1 3
|
divdird |
|- ( A e. RR+ -> ( ( A + 1 ) / A ) = ( ( A / A ) + ( 1 / A ) ) ) |
5 |
1 3
|
dividd |
|- ( A e. RR+ -> ( A / A ) = 1 ) |
6 |
5
|
oveq1d |
|- ( A e. RR+ -> ( ( A / A ) + ( 1 / A ) ) = ( 1 + ( 1 / A ) ) ) |
7 |
4 6
|
eqtr2d |
|- ( A e. RR+ -> ( 1 + ( 1 / A ) ) = ( ( A + 1 ) / A ) ) |
8 |
7
|
fveq2d |
|- ( A e. RR+ -> ( log ` ( 1 + ( 1 / A ) ) ) = ( log ` ( ( A + 1 ) / A ) ) ) |
9 |
|
1rp |
|- 1 e. RR+ |
10 |
|
rpaddcl |
|- ( ( A e. RR+ /\ 1 e. RR+ ) -> ( A + 1 ) e. RR+ ) |
11 |
9 10
|
mpan2 |
|- ( A e. RR+ -> ( A + 1 ) e. RR+ ) |
12 |
|
relogdiv |
|- ( ( ( A + 1 ) e. RR+ /\ A e. RR+ ) -> ( log ` ( ( A + 1 ) / A ) ) = ( ( log ` ( A + 1 ) ) - ( log ` A ) ) ) |
13 |
11 12
|
mpancom |
|- ( A e. RR+ -> ( log ` ( ( A + 1 ) / A ) ) = ( ( log ` ( A + 1 ) ) - ( log ` A ) ) ) |
14 |
8 13
|
eqtrd |
|- ( A e. RR+ -> ( log ` ( 1 + ( 1 / A ) ) ) = ( ( log ` ( A + 1 ) ) - ( log ` A ) ) ) |
15 |
|
rpreccl |
|- ( A e. RR+ -> ( 1 / A ) e. RR+ ) |
16 |
|
rpaddcl |
|- ( ( 1 e. RR+ /\ ( 1 / A ) e. RR+ ) -> ( 1 + ( 1 / A ) ) e. RR+ ) |
17 |
9 15 16
|
sylancr |
|- ( A e. RR+ -> ( 1 + ( 1 / A ) ) e. RR+ ) |
18 |
17
|
reeflogd |
|- ( A e. RR+ -> ( exp ` ( log ` ( 1 + ( 1 / A ) ) ) ) = ( 1 + ( 1 / A ) ) ) |
19 |
17
|
rpred |
|- ( A e. RR+ -> ( 1 + ( 1 / A ) ) e. RR ) |
20 |
15
|
rpred |
|- ( A e. RR+ -> ( 1 / A ) e. RR ) |
21 |
20
|
reefcld |
|- ( A e. RR+ -> ( exp ` ( 1 / A ) ) e. RR ) |
22 |
|
efgt1p |
|- ( ( 1 / A ) e. RR+ -> ( 1 + ( 1 / A ) ) < ( exp ` ( 1 / A ) ) ) |
23 |
15 22
|
syl |
|- ( A e. RR+ -> ( 1 + ( 1 / A ) ) < ( exp ` ( 1 / A ) ) ) |
24 |
19 21 23
|
ltled |
|- ( A e. RR+ -> ( 1 + ( 1 / A ) ) <_ ( exp ` ( 1 / A ) ) ) |
25 |
18 24
|
eqbrtrd |
|- ( A e. RR+ -> ( exp ` ( log ` ( 1 + ( 1 / A ) ) ) ) <_ ( exp ` ( 1 / A ) ) ) |
26 |
|
relogcl |
|- ( ( A + 1 ) e. RR+ -> ( log ` ( A + 1 ) ) e. RR ) |
27 |
11 26
|
syl |
|- ( A e. RR+ -> ( log ` ( A + 1 ) ) e. RR ) |
28 |
|
relogcl |
|- ( A e. RR+ -> ( log ` A ) e. RR ) |
29 |
27 28
|
resubcld |
|- ( A e. RR+ -> ( ( log ` ( A + 1 ) ) - ( log ` A ) ) e. RR ) |
30 |
14 29
|
eqeltrd |
|- ( A e. RR+ -> ( log ` ( 1 + ( 1 / A ) ) ) e. RR ) |
31 |
|
efle |
|- ( ( ( log ` ( 1 + ( 1 / A ) ) ) e. RR /\ ( 1 / A ) e. RR ) -> ( ( log ` ( 1 + ( 1 / A ) ) ) <_ ( 1 / A ) <-> ( exp ` ( log ` ( 1 + ( 1 / A ) ) ) ) <_ ( exp ` ( 1 / A ) ) ) ) |
32 |
30 20 31
|
syl2anc |
|- ( A e. RR+ -> ( ( log ` ( 1 + ( 1 / A ) ) ) <_ ( 1 / A ) <-> ( exp ` ( log ` ( 1 + ( 1 / A ) ) ) ) <_ ( exp ` ( 1 / A ) ) ) ) |
33 |
25 32
|
mpbird |
|- ( A e. RR+ -> ( log ` ( 1 + ( 1 / A ) ) ) <_ ( 1 / A ) ) |
34 |
14 33
|
eqbrtrrd |
|- ( A e. RR+ -> ( ( log ` ( A + 1 ) ) - ( log ` A ) ) <_ ( 1 / A ) ) |