Step |
Hyp |
Ref |
Expression |
1 |
|
ef0 |
|- ( exp ` 0 ) = 1 |
2 |
|
efvmacl |
|- ( A e. NN -> ( exp ` ( Lam ` A ) ) e. NN ) |
3 |
2
|
nnge1d |
|- ( A e. NN -> 1 <_ ( exp ` ( Lam ` A ) ) ) |
4 |
1 3
|
eqbrtrid |
|- ( A e. NN -> ( exp ` 0 ) <_ ( exp ` ( Lam ` A ) ) ) |
5 |
|
0re |
|- 0 e. RR |
6 |
|
vmacl |
|- ( A e. NN -> ( Lam ` A ) e. RR ) |
7 |
|
efle |
|- ( ( 0 e. RR /\ ( Lam ` A ) e. RR ) -> ( 0 <_ ( Lam ` A ) <-> ( exp ` 0 ) <_ ( exp ` ( Lam ` A ) ) ) ) |
8 |
5 6 7
|
sylancr |
|- ( A e. NN -> ( 0 <_ ( Lam ` A ) <-> ( exp ` 0 ) <_ ( exp ` ( Lam ` A ) ) ) ) |
9 |
4 8
|
mpbird |
|- ( A e. NN -> 0 <_ ( Lam ` A ) ) |