reeff1o

Description: The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 10-Nov-2013)

		Ref	Expression
	Assertion	reeff1o	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1 onto}{⟶} ℝ^{+}$

Proof

Step	Hyp	Ref	Expression
1		reeff1	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1}{⟶} ℝ^{+}$
2		f1f	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1}{⟶} ℝ^{+} \to ({\exp ↾}_{ℝ}) : ℝ ⟶ ℝ^{+}$
3		ffn	$⊢ ({\exp ↾}_{ℝ}) : ℝ ⟶ ℝ^{+} \to ({\exp ↾}_{ℝ}) Fn ℝ$
4	1 2 3	mp2b	$⊢ ({\exp ↾}_{ℝ}) Fn ℝ$
5		frn	$⊢ ({\exp ↾}_{ℝ}) : ℝ ⟶ ℝ^{+} \to ran ({\exp ↾}_{ℝ}) \subseteq ℝ^{+}$
6	1 2 5	mp2b	$⊢ ran ({\exp ↾}_{ℝ}) \subseteq ℝ^{+}$
7		elrp	$⊢ z \in ℝ^{+} \leftrightarrow (z \in ℝ \land 0 < z)$
8		reclt1	$⊢ (z \in ℝ \land 0 < z) \to (z < 1 \leftrightarrow 1 < \frac{1}{z})$
9	7 8	sylbi	$⊢ z \in ℝ^{+} \to (z < 1 \leftrightarrow 1 < \frac{1}{z})$
10		rpre	$⊢ z \in ℝ^{+} \to z \in ℝ$
11		rpne0	$⊢ z \in ℝ^{+} \to z \neq 0$
12	10 11	rereccld	$⊢ z \in ℝ^{+} \to \frac{1}{z} \in ℝ$
13		reeff1olem	$⊢ (\frac{1}{z} \in ℝ \land 1 < \frac{1}{z}) \to \exists y \in ℝ e^{y} = \frac{1}{z}$
14	12 13	sylan	$⊢ (z \in ℝ^{+} \land 1 < \frac{1}{z}) \to \exists y \in ℝ e^{y} = \frac{1}{z}$
15		eqcom	$⊢ \frac{1}{z} = e^{y} \leftrightarrow e^{y} = \frac{1}{z}$
16		rpcnne0	$⊢ z \in ℝ^{+} \to (z \in ℂ \land z \neq 0)$
17		recn	$⊢ y \in ℝ \to y \in ℂ$
18		efcl	$⊢ y \in ℂ \to e^{y} \in ℂ$
19	17 18	syl	$⊢ y \in ℝ \to e^{y} \in ℂ$
20		efne0	$⊢ y \in ℂ \to e^{y} \neq 0$
21	17 20	syl	$⊢ y \in ℝ \to e^{y} \neq 0$
22	19 21	jca	$⊢ y \in ℝ \to (e^{y} \in ℂ \land e^{y} \neq 0)$
23		rec11r	$⊢ ((z \in ℂ \land z \neq 0) \land (e^{y} \in ℂ \land e^{y} \neq 0)) \to (\frac{1}{z} = e^{y} \leftrightarrow \frac{1}{e^{y}} = z)$
24	16 22 23	syl2an	$⊢ (z \in ℝ^{+} \land y \in ℝ) \to (\frac{1}{z} = e^{y} \leftrightarrow \frac{1}{e^{y}} = z)$
25		efcan	$⊢ y \in ℂ \to e^{y} e^{- y} = 1$
26	25	eqcomd	$⊢ y \in ℂ \to 1 = e^{y} e^{- y}$
27		negcl	$⊢ y \in ℂ \to - y \in ℂ$
28		efcl	$⊢ - y \in ℂ \to e^{- y} \in ℂ$
29	27 28	syl	$⊢ y \in ℂ \to e^{- y} \in ℂ$
30		ax-1cn	$⊢ 1 \in ℂ$
31		divmul2	$⊢ (1 \in ℂ \land e^{- y} \in ℂ \land (e^{y} \in ℂ \land e^{y} \neq 0)) \to (\frac{1}{e^{y}} = e^{- y} \leftrightarrow 1 = e^{y} e^{- y})$
32	30 31	mp3an1	$⊢ (e^{- y} \in ℂ \land (e^{y} \in ℂ \land e^{y} \neq 0)) \to (\frac{1}{e^{y}} = e^{- y} \leftrightarrow 1 = e^{y} e^{- y})$
33	29 18 20 32	syl12anc	$⊢ y \in ℂ \to (\frac{1}{e^{y}} = e^{- y} \leftrightarrow 1 = e^{y} e^{- y})$
34	26 33	mpbird	$⊢ y \in ℂ \to \frac{1}{e^{y}} = e^{- y}$
35	17 34	syl	$⊢ y \in ℝ \to \frac{1}{e^{y}} = e^{- y}$
36	35	eqeq1d	$⊢ y \in ℝ \to (\frac{1}{e^{y}} = z \leftrightarrow e^{- y} = z)$
37	36	adantl	$⊢ (z \in ℝ^{+} \land y \in ℝ) \to (\frac{1}{e^{y}} = z \leftrightarrow e^{- y} = z)$
38	24 37	bitrd	$⊢ (z \in ℝ^{+} \land y \in ℝ) \to (\frac{1}{z} = e^{y} \leftrightarrow e^{- y} = z)$
39	15 38	bitr3id	$⊢ (z \in ℝ^{+} \land y \in ℝ) \to (e^{y} = \frac{1}{z} \leftrightarrow e^{- y} = z)$
40	39	biimpd	$⊢ (z \in ℝ^{+} \land y \in ℝ) \to (e^{y} = \frac{1}{z} \to e^{- y} = z)$
41	40	reximdva	$⊢ z \in ℝ^{+} \to (\exists y \in ℝ e^{y} = \frac{1}{z} \to \exists y \in ℝ e^{- y} = z)$
42	41	adantr	$⊢ (z \in ℝ^{+} \land 1 < \frac{1}{z}) \to (\exists y \in ℝ e^{y} = \frac{1}{z} \to \exists y \in ℝ e^{- y} = z)$
43	14 42	mpd	$⊢ (z \in ℝ^{+} \land 1 < \frac{1}{z}) \to \exists y \in ℝ e^{- y} = z$
44		renegcl	$⊢ y \in ℝ \to - y \in ℝ$
45		infm3lem	$⊢ x \in ℝ \to \exists y \in ℝ x = - y$
46		fveqeq2	$⊢ x = - y \to (e^{x} = z \leftrightarrow e^{- y} = z)$
47	44 45 46	rexxfr	$⊢ \exists x \in ℝ e^{x} = z \leftrightarrow \exists y \in ℝ e^{- y} = z$
48	43 47	sylibr	$⊢ (z \in ℝ^{+} \land 1 < \frac{1}{z}) \to \exists x \in ℝ e^{x} = z$
49	48	ex	$⊢ z \in ℝ^{+} \to (1 < \frac{1}{z} \to \exists x \in ℝ e^{x} = z)$
50	9 49	sylbid	$⊢ z \in ℝ^{+} \to (z < 1 \to \exists x \in ℝ e^{x} = z)$
51	50	imp	$⊢ (z \in ℝ^{+} \land z < 1) \to \exists x \in ℝ e^{x} = z$
52		ef0	$⊢ e^{0} = 1$
53	52	eqeq2i	$⊢ z = e^{0} \leftrightarrow z = 1$
54		0re	$⊢ 0 \in ℝ$
55		fveqeq2	$⊢ x = 0 \to (e^{x} = z \leftrightarrow e^{0} = z)$
56	55	rspcev	$⊢ (0 \in ℝ \land e^{0} = z) \to \exists x \in ℝ e^{x} = z$
57	54 56	mpan	$⊢ e^{0} = z \to \exists x \in ℝ e^{x} = z$
58	57	eqcoms	$⊢ z = e^{0} \to \exists x \in ℝ e^{x} = z$
59	53 58	sylbir	$⊢ z = 1 \to \exists x \in ℝ e^{x} = z$
60	59	adantl	$⊢ (z \in ℝ^{+} \land z = 1) \to \exists x \in ℝ e^{x} = z$
61		reeff1olem	$⊢ (z \in ℝ \land 1 < z) \to \exists x \in ℝ e^{x} = z$
62	10 61	sylan	$⊢ (z \in ℝ^{+} \land 1 < z) \to \exists x \in ℝ e^{x} = z$
63		1re	$⊢ 1 \in ℝ$
64		lttri4	$⊢ (z \in ℝ \land 1 \in ℝ) \to (z < 1 \lor z = 1 \lor 1 < z)$
65	10 63 64	sylancl	$⊢ z \in ℝ^{+} \to (z < 1 \lor z = 1 \lor 1 < z)$
66	51 60 62 65	mpjao3dan	$⊢ z \in ℝ^{+} \to \exists x \in ℝ e^{x} = z$
67		fvres	$⊢ x \in ℝ \to ({\exp ↾}_{ℝ}) (x) = e^{x}$
68	67	eqeq1d	$⊢ x \in ℝ \to (({\exp ↾}_{ℝ}) (x) = z \leftrightarrow e^{x} = z)$
69	68	rexbiia	$⊢ \exists x \in ℝ ({\exp ↾}_{ℝ}) (x) = z \leftrightarrow \exists x \in ℝ e^{x} = z$
70	66 69	sylibr	$⊢ z \in ℝ^{+} \to \exists x \in ℝ ({\exp ↾}_{ℝ}) (x) = z$
71		fvelrnb	$⊢ ({\exp ↾}_{ℝ}) Fn ℝ \to (z \in ran ({\exp ↾}_{ℝ}) \leftrightarrow \exists x \in ℝ ({\exp ↾}_{ℝ}) (x) = z)$
72	4 71	ax-mp	$⊢ z \in ran ({\exp ↾}_{ℝ}) \leftrightarrow \exists x \in ℝ ({\exp ↾}_{ℝ}) (x) = z$
73	70 72	sylibr	$⊢ z \in ℝ^{+} \to z \in ran ({\exp ↾}_{ℝ})$
74	73	ssriv	$⊢ ℝ^{+} \subseteq ran ({\exp ↾}_{ℝ})$
75	6 74	eqssi	$⊢ ran ({\exp ↾}_{ℝ}) = ℝ^{+}$
76		df-fo	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{onto}{⟶} ℝ^{+} \leftrightarrow (({\exp ↾}_{ℝ}) Fn ℝ \land ran ({\exp ↾}_{ℝ}) = ℝ^{+})$
77	4 75 76	mpbir2an	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{onto}{⟶} ℝ^{+}$
78		df-f1o	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1 onto}{⟶} ℝ^{+} \leftrightarrow (({\exp ↾}_{ℝ}) : ℝ \underset{1-1}{⟶} ℝ^{+} \land ({\exp ↾}_{ℝ}) : ℝ \underset{onto}{⟶} ℝ^{+})$
79	1 77 78	mpbir2an	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1 onto}{⟶} ℝ^{+}$

Metamath Proof Explorer

Theorem reeff1o

Proof