Theorem efle

Description: The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		eflt	|- ( ( B e. RR /\ A e. RR ) -> ( B < A <-> ( exp ` B ) < ( exp ` A ) ) )
2	1	ancoms	|- ( ( A e. RR /\ B e. RR ) -> ( B < A <-> ( exp ` B ) < ( exp ` A ) ) )
3	2	notbid	|- ( ( A e. RR /\ B e. RR ) -> ( -. B < A <-> -. ( exp ` B ) < ( exp ` A ) ) )
4		lenlt	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
5		reefcl	|- ( A e. RR -> ( exp ` A ) e. RR )
6		reefcl	|- ( B e. RR -> ( exp ` B ) e. RR )
7		lenlt	|- ( ( ( exp ` A ) e. RR /\ ( exp ` B ) e. RR ) -> ( ( exp ` A ) <_ ( exp ` B ) <-> -. ( exp ` B ) < ( exp ` A ) ) )
8	5 6 7	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( ( exp ` A ) <_ ( exp ` B ) <-> -. ( exp ` B ) < ( exp ` A ) ) )
9	3 4 8	3bitr4d	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( exp ` A ) <_ ( exp ` B ) ) )