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 mulid1d ( 𝑦 ∈ ( 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 mulid2d ( ( 𝑥 ∈ ( 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 mulid1d ( ( 𝑥 ∈ ( 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 + 𝑦 ) ) ) )