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