# Metamath Proof Explorer

## Theorem icopnfcnv

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

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

### Proof

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