Step |
Hyp |
Ref |
Expression |
1 |
|
tru |
|- T. |
2 |
|
fveq2 |
|- ( x = y -> ( exp ` x ) = ( exp ` y ) ) |
3 |
|
fveq2 |
|- ( x = A -> ( exp ` x ) = ( exp ` A ) ) |
4 |
|
fveq2 |
|- ( x = B -> ( exp ` x ) = ( exp ` B ) ) |
5 |
|
ssid |
|- RR C_ RR |
6 |
|
reefcl |
|- ( x e. RR -> ( exp ` x ) e. RR ) |
7 |
6
|
adantl |
|- ( ( T. /\ x e. RR ) -> ( exp ` x ) e. RR ) |
8 |
|
simp2 |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> y e. RR ) |
9 |
|
simp1 |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> x e. RR ) |
10 |
8 9
|
resubcld |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( y - x ) e. RR ) |
11 |
|
posdif |
|- ( ( x e. RR /\ y e. RR ) -> ( x < y <-> 0 < ( y - x ) ) ) |
12 |
11
|
biimp3a |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> 0 < ( y - x ) ) |
13 |
10 12
|
elrpd |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( y - x ) e. RR+ ) |
14 |
|
efgt1 |
|- ( ( y - x ) e. RR+ -> 1 < ( exp ` ( y - x ) ) ) |
15 |
13 14
|
syl |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> 1 < ( exp ` ( y - x ) ) ) |
16 |
9
|
reefcld |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( exp ` x ) e. RR ) |
17 |
10
|
reefcld |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( exp ` ( y - x ) ) e. RR ) |
18 |
|
efgt0 |
|- ( x e. RR -> 0 < ( exp ` x ) ) |
19 |
9 18
|
syl |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> 0 < ( exp ` x ) ) |
20 |
|
ltmulgt11 |
|- ( ( ( exp ` x ) e. RR /\ ( exp ` ( y - x ) ) e. RR /\ 0 < ( exp ` x ) ) -> ( 1 < ( exp ` ( y - x ) ) <-> ( exp ` x ) < ( ( exp ` x ) x. ( exp ` ( y - x ) ) ) ) ) |
21 |
16 17 19 20
|
syl3anc |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( 1 < ( exp ` ( y - x ) ) <-> ( exp ` x ) < ( ( exp ` x ) x. ( exp ` ( y - x ) ) ) ) ) |
22 |
15 21
|
mpbid |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( exp ` x ) < ( ( exp ` x ) x. ( exp ` ( y - x ) ) ) ) |
23 |
9
|
recnd |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> x e. CC ) |
24 |
10
|
recnd |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( y - x ) e. CC ) |
25 |
|
efadd |
|- ( ( x e. CC /\ ( y - x ) e. CC ) -> ( exp ` ( x + ( y - x ) ) ) = ( ( exp ` x ) x. ( exp ` ( y - x ) ) ) ) |
26 |
23 24 25
|
syl2anc |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( exp ` ( x + ( y - x ) ) ) = ( ( exp ` x ) x. ( exp ` ( y - x ) ) ) ) |
27 |
8
|
recnd |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> y e. CC ) |
28 |
23 27
|
pncan3d |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( x + ( y - x ) ) = y ) |
29 |
28
|
fveq2d |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( exp ` ( x + ( y - x ) ) ) = ( exp ` y ) ) |
30 |
26 29
|
eqtr3d |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( ( exp ` x ) x. ( exp ` ( y - x ) ) ) = ( exp ` y ) ) |
31 |
22 30
|
breqtrd |
|- ( ( x e. RR /\ y e. RR /\ x < y ) -> ( exp ` x ) < ( exp ` y ) ) |
32 |
31
|
3expia |
|- ( ( x e. RR /\ y e. RR ) -> ( x < y -> ( exp ` x ) < ( exp ` y ) ) ) |
33 |
32
|
adantl |
|- ( ( T. /\ ( x e. RR /\ y e. RR ) ) -> ( x < y -> ( exp ` x ) < ( exp ` y ) ) ) |
34 |
2 3 4 5 7 33
|
ltord1 |
|- ( ( T. /\ ( A e. RR /\ B e. RR ) ) -> ( A < B <-> ( exp ` A ) < ( exp ` B ) ) ) |
35 |
1 34
|
mpan |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( exp ` A ) < ( exp ` B ) ) ) |