Theorem reef11

Description: The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008) (Revised by Mario Carneiro, 11-Mar-2014)

	Ref	Expression
Assertion	reef11	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left({\mathrm{e}}^A={\mathrm{e}}^B\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		efle	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\leftrightarrow {\mathrm{e}}^A\le {\mathrm{e}}^B\right)$$
2		efle	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(B\le A\leftrightarrow {\mathrm{e}}^B\le {\mathrm{e}}^A\right)$$
3	2	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B\le A\leftrightarrow {\mathrm{e}}^B\le {\mathrm{e}}^A\right)$$
4	1 3	anbi12d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(A\le B\wedge B\le A\right)\leftrightarrow \left({\mathrm{e}}^A\le {\mathrm{e}}^B\wedge {\mathrm{e}}^B\le {\mathrm{e}}^A\right)\right)$$
5		letri3	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A=B\leftrightarrow \left(A\le B\wedge B\le A\right)\right)$$
6		reefcl	$$⊢A\in ℝ\to {\mathrm{e}}^A\in ℝ$$
7		reefcl	$$⊢B\in ℝ\to {\mathrm{e}}^B\in ℝ$$
8		letri3	$$⊢\left({\mathrm{e}}^A\in ℝ\wedge {\mathrm{e}}^B\in ℝ\right)\to \left({\mathrm{e}}^A={\mathrm{e}}^B\leftrightarrow \left({\mathrm{e}}^A\le {\mathrm{e}}^B\wedge {\mathrm{e}}^B\le {\mathrm{e}}^A\right)\right)$$
9	6 7 8	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left({\mathrm{e}}^A={\mathrm{e}}^B\leftrightarrow \left({\mathrm{e}}^A\le {\mathrm{e}}^B\wedge {\mathrm{e}}^B\le {\mathrm{e}}^A\right)\right)$$
10	4 5 9	3bitr4rd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left({\mathrm{e}}^A={\mathrm{e}}^B\leftrightarrow A=B\right)$$