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 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,) 1 ) ↦ ( 𝑥 / ( 1 − 𝑥 ) ) )
Assertion icopnfcnv ( 𝐹 : ( 0 [,) 1 ) –1-1-onto→ ( 0 [,) +∞ ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 0 [,) +∞ ) ↦ ( 𝑦 / ( 1 + 𝑦 ) ) ) )

Proof

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