icopnfcnv

Description: Define a bijection from [ 0 , 1 ) to [ 0 , +oo ) . (Contributed by Mario Carneiro, 9-Sep-2015)

		Ref	Expression
	Hypothesis	icopnfhmeo.f	$⊢ F = (x \in [0, 1) ⟼ \frac{x}{1 - x})$
	Assertion	icopnfcnv	$⊢ (F : [0, 1) \underset{1-1 onto}{⟶} [0, +∞) \land F^{-1} = (y \in [0, +∞) ⟼ \frac{y}{1 + y}))$

Proof

Step	Hyp	Ref	Expression
1		icopnfhmeo.f	$⊢ F = (x \in [0, 1) ⟼ \frac{x}{1 - x})$
2		0re	$⊢ 0 \in ℝ$
3		1xr	$⊢ 1 \in ℝ^{*}$
4		elico2	$⊢ (0 \in ℝ \land 1 \in ℝ^{*}) \to (x \in [0, 1) \leftrightarrow (x \in ℝ \land 0 \leq x \land x < 1))$
5	2 3 4	mp2an	$⊢ x \in [0, 1) \leftrightarrow (x \in ℝ \land 0 \leq x \land x < 1)$
6	5	simp1bi	$⊢ x \in [0, 1) \to x \in ℝ$
7	5	simp3bi	$⊢ x \in [0, 1) \to x < 1$
8		1re	$⊢ 1 \in ℝ$
9		difrp	$⊢ (x \in ℝ \land 1 \in ℝ) \to (x < 1 \leftrightarrow 1 - x \in ℝ^{+})$
10	6 8 9	sylancl	$⊢ x \in [0, 1) \to (x < 1 \leftrightarrow 1 - x \in ℝ^{+})$
11	7 10	mpbid	$⊢ x \in [0, 1) \to 1 - x \in ℝ^{+}$
12	6 11	rerpdivcld	$⊢ x \in [0, 1) \to \frac{x}{1 - x} \in ℝ$
13	5	simp2bi	$⊢ x \in [0, 1) \to 0 \leq x$
14	6 11 13	divge0d	$⊢ x \in [0, 1) \to 0 \leq \frac{x}{1 - x}$
15		elrege0	$⊢ \frac{x}{1 - x} \in [0, +∞) \leftrightarrow (\frac{x}{1 - x} \in ℝ \land 0 \leq \frac{x}{1 - x})$
16	12 14 15	sylanbrc	$⊢ x \in [0, 1) \to \frac{x}{1 - x} \in [0, +∞)$
17	16	adantl	$⊢ (⊤ \land x \in [0, 1)) \to \frac{x}{1 - x} \in [0, +∞)$
18		elrege0	$⊢ y \in [0, +∞) \leftrightarrow (y \in ℝ \land 0 \leq y)$
19	18	simplbi	$⊢ y \in [0, +∞) \to y \in ℝ$
20		readdcl	$⊢ (1 \in ℝ \land y \in ℝ) \to 1 + y \in ℝ$
21	8 19 20	sylancr	$⊢ y \in [0, +∞) \to 1 + y \in ℝ$
22	2	a1i	$⊢ y \in [0, +∞) \to 0 \in ℝ$
23	18	simprbi	$⊢ y \in [0, +∞) \to 0 \leq y$
24	19	ltp1d	$⊢ y \in [0, +∞) \to y < y + 1$
25		ax-1cn	$⊢ 1 \in ℂ$
26	19	recnd	$⊢ y \in [0, +∞) \to y \in ℂ$
27		addcom	$⊢ (1 \in ℂ \land y \in ℂ) \to 1 + y = y + 1$
28	25 26 27	sylancr	$⊢ y \in [0, +∞) \to 1 + y = y + 1$
29	24 28	breqtrrd	$⊢ y \in [0, +∞) \to y < 1 + y$
30	22 19 21 23 29	lelttrd	$⊢ y \in [0, +∞) \to 0 < 1 + y$
31	21 30	elrpd	$⊢ y \in [0, +∞) \to 1 + y \in ℝ^{+}$
32	19 31	rerpdivcld	$⊢ y \in [0, +∞) \to \frac{y}{1 + y} \in ℝ$
33		divge0	$⊢ ((y \in ℝ \land 0 \leq y) \land (1 + y \in ℝ \land 0 < 1 + y)) \to 0 \leq \frac{y}{1 + y}$
34	19 23 21 30 33	syl22anc	$⊢ y \in [0, +∞) \to 0 \leq \frac{y}{1 + y}$
35	21	recnd	$⊢ y \in [0, +∞) \to 1 + y \in ℂ$
36	35	mulid1d	$⊢ y \in [0, +∞) \to (1 + y) \cdot 1 = 1 + y$
37	29 36	breqtrrd	$⊢ y \in [0, +∞) \to y < (1 + y) \cdot 1$
38	8	a1i	$⊢ y \in [0, +∞) \to 1 \in ℝ$
39		ltdivmul	$⊢ (y \in ℝ \land 1 \in ℝ \land (1 + y \in ℝ \land 0 < 1 + y)) \to (\frac{y}{1 + y} < 1 \leftrightarrow y < (1 + y) \cdot 1)$
40	19 38 21 30 39	syl112anc	$⊢ y \in [0, +∞) \to (\frac{y}{1 + y} < 1 \leftrightarrow y < (1 + y) \cdot 1)$
41	37 40	mpbird	$⊢ y \in [0, +∞) \to \frac{y}{1 + y} < 1$
42		elico2	$⊢ (0 \in ℝ \land 1 \in ℝ^{*}) \to (\frac{y}{1 + y} \in [0, 1) \leftrightarrow (\frac{y}{1 + y} \in ℝ \land 0 \leq \frac{y}{1 + y} \land \frac{y}{1 + y} < 1))$
43	2 3 42	mp2an	$⊢ \frac{y}{1 + y} \in [0, 1) \leftrightarrow (\frac{y}{1 + y} \in ℝ \land 0 \leq \frac{y}{1 + y} \land \frac{y}{1 + y} < 1)$
44	32 34 41 43	syl3anbrc	$⊢ y \in [0, +∞) \to \frac{y}{1 + y} \in [0, 1)$
45	44	adantl	$⊢ (⊤ \land y \in [0, +∞)) \to \frac{y}{1 + y} \in [0, 1)$
46	26	adantl	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to y \in ℂ$
47	6	adantr	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to x \in ℝ$
48	47	recnd	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to x \in ℂ$
49	48 46	mulcld	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to x y \in ℂ$
50	46 49 48	subadd2d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (y - x y = x \leftrightarrow x + x y = y)$
51		1cnd	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to 1 \in ℂ$
52	51 48 46	subdird	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (1 - x) y = 1 y - x y$
53	46	mulid2d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to 1 y = y$
54	53	oveq1d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to 1 y - x y = y - x y$
55	52 54	eqtrd	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (1 - x) y = y - x y$
56	55	eqeq1d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to ((1 - x) y = x \leftrightarrow y - x y = x)$
57	48 51 46	adddid	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to x (1 + y) = x \cdot 1 + x y$
58	48	mulid1d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to x \cdot 1 = x$
59	58	oveq1d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to x \cdot 1 + x y = x + x y$
60	57 59	eqtrd	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to x (1 + y) = x + x y$
61	60	eqeq1d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (x (1 + y) = y \leftrightarrow x + x y = y)$
62	50 56 61	3bitr4rd	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (x (1 + y) = y \leftrightarrow (1 - x) y = x)$
63		eqcom	$⊢ y = x (1 + y) \leftrightarrow x (1 + y) = y$
64		eqcom	$⊢ x = (1 - x) y \leftrightarrow (1 - x) y = x$
65	62 63 64	3bitr4g	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (y = x (1 + y) \leftrightarrow x = (1 - x) y)$
66	35	adantl	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to 1 + y \in ℂ$
67	31	adantl	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to 1 + y \in ℝ^{+}$
68	67	rpne0d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to 1 + y \neq 0$
69	46 48 66 68	divmul3d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (\frac{y}{1 + y} = x \leftrightarrow y = x (1 + y))$
70	11	adantr	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to 1 - x \in ℝ^{+}$
71	70	rpcnd	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to 1 - x \in ℂ$
72	70	rpne0d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to 1 - x \neq 0$
73	48 46 71 72	divmul2d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (\frac{x}{1 - x} = y \leftrightarrow x = (1 - x) y)$
74	65 69 73	3bitr4d	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (\frac{y}{1 + y} = x \leftrightarrow \frac{x}{1 - x} = y)$
75		eqcom	$⊢ x = \frac{y}{1 + y} \leftrightarrow \frac{y}{1 + y} = x$
76		eqcom	$⊢ y = \frac{x}{1 - x} \leftrightarrow \frac{x}{1 - x} = y$
77	74 75 76	3bitr4g	$⊢ (x \in [0, 1) \land y \in [0, +∞)) \to (x = \frac{y}{1 + y} \leftrightarrow y = \frac{x}{1 - x})$
78	77	adantl	$⊢ (⊤ \land (x \in [0, 1) \land y \in [0, +∞))) \to (x = \frac{y}{1 + y} \leftrightarrow y = \frac{x}{1 - x})$
79	1 17 45 78	f1ocnv2d	$⊢ ⊤ \to (F : [0, 1) \underset{1-1 onto}{⟶} [0, +∞) \land F^{-1} = (y \in [0, +∞) ⟼ \frac{y}{1 + y}))$
80	79	mptru	$⊢ (F : [0, 1) \underset{1-1 onto}{⟶} [0, +∞) \land F^{-1} = (y \in [0, +∞) ⟼ \frac{y}{1 + y}))$

Metamath Proof Explorer

Theorem icopnfcnv

Proof