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=x∈01⟼x1−x
Assertion icopnfcnv ⊢F:01⟶1-1 onto0+∞∧F-1=y∈0+∞⟼y1+y

Proof

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