Description: The exponential of a positive real number is greater than 1. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 30-Apr-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | efgt1 | |- ( A e. RR+ -> 1 < ( exp ` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1red | |- ( A e. RR+ -> 1 e. RR ) |
|
| 2 | 1re | |- 1 e. RR |
|
| 3 | rpre | |- ( A e. RR+ -> A e. RR ) |
|
| 4 | readdcl | |- ( ( 1 e. RR /\ A e. RR ) -> ( 1 + A ) e. RR ) |
|
| 5 | 2 3 4 | sylancr | |- ( A e. RR+ -> ( 1 + A ) e. RR ) |
| 6 | 3 | reefcld | |- ( A e. RR+ -> ( exp ` A ) e. RR ) |
| 7 | ltaddrp | |- ( ( 1 e. RR /\ A e. RR+ ) -> 1 < ( 1 + A ) ) |
|
| 8 | 2 7 | mpan | |- ( A e. RR+ -> 1 < ( 1 + A ) ) |
| 9 | efgt1p | |- ( A e. RR+ -> ( 1 + A ) < ( exp ` A ) ) |
|
| 10 | 1 5 6 8 9 | lttrd | |- ( A e. RR+ -> 1 < ( exp ` A ) ) |