Metamath Proof Explorer

Theorem eflt

Description: The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion eflt 
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( exp ` A ) < ( exp ` B ) ) )

Proof

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