Proof of Theorem icopnfcnv
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | icopnfhmeo.f | . . 3
⊢ 𝐹 = (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) | 
| 2 |  | 0re 11264 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 3 |  | 1xr 11321 | . . . . . . . 8
⊢ 1 ∈
ℝ* | 
| 4 |  | elico2 13452 | . . . . . . . 8
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ*) → (𝑥 ∈ (0[,)1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < 1))) | 
| 5 | 2, 3, 4 | mp2an 692 | . . . . . . 7
⊢ (𝑥 ∈ (0[,)1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 < 1)) | 
| 6 | 5 | simp1bi 1145 | . . . . . 6
⊢ (𝑥 ∈ (0[,)1) → 𝑥 ∈
ℝ) | 
| 7 | 5 | simp3bi 1147 | . . . . . . 7
⊢ (𝑥 ∈ (0[,)1) → 𝑥 < 1) | 
| 8 |  | 1re 11262 | . . . . . . . 8
⊢ 1 ∈
ℝ | 
| 9 |  | difrp 13074 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑥 < 1
↔ (1 − 𝑥) ∈
ℝ+)) | 
| 10 | 6, 8, 9 | sylancl 586 | . . . . . . 7
⊢ (𝑥 ∈ (0[,)1) → (𝑥 < 1 ↔ (1 − 𝑥) ∈
ℝ+)) | 
| 11 | 7, 10 | mpbid 232 | . . . . . 6
⊢ (𝑥 ∈ (0[,)1) → (1
− 𝑥) ∈
ℝ+) | 
| 12 | 6, 11 | rerpdivcld 13109 | . . . . 5
⊢ (𝑥 ∈ (0[,)1) → (𝑥 / (1 − 𝑥)) ∈ ℝ) | 
| 13 | 5 | simp2bi 1146 | . . . . . 6
⊢ (𝑥 ∈ (0[,)1) → 0 ≤
𝑥) | 
| 14 | 6, 11, 13 | divge0d 13118 | . . . . 5
⊢ (𝑥 ∈ (0[,)1) → 0 ≤
(𝑥 / (1 − 𝑥))) | 
| 15 |  | elrege0 13495 | . . . . 5
⊢ ((𝑥 / (1 − 𝑥)) ∈ (0[,)+∞) ↔ ((𝑥 / (1 − 𝑥)) ∈ ℝ ∧ 0 ≤ (𝑥 / (1 − 𝑥)))) | 
| 16 | 12, 14, 15 | sylanbrc 583 | . . . 4
⊢ (𝑥 ∈ (0[,)1) → (𝑥 / (1 − 𝑥)) ∈ (0[,)+∞)) | 
| 17 | 16 | adantl 481 | . . 3
⊢
((⊤ ∧ 𝑥
∈ (0[,)1)) → (𝑥 /
(1 − 𝑥)) ∈
(0[,)+∞)) | 
| 18 |  | elrege0 13495 | . . . . . . 7
⊢ (𝑦 ∈ (0[,)+∞) ↔
(𝑦 ∈ ℝ ∧ 0
≤ 𝑦)) | 
| 19 | 18 | simplbi 497 | . . . . . 6
⊢ (𝑦 ∈ (0[,)+∞) →
𝑦 ∈
ℝ) | 
| 20 |  | readdcl 11239 | . . . . . . . 8
⊢ ((1
∈ ℝ ∧ 𝑦
∈ ℝ) → (1 + 𝑦) ∈ ℝ) | 
| 21 | 8, 19, 20 | sylancr 587 | . . . . . . 7
⊢ (𝑦 ∈ (0[,)+∞) → (1
+ 𝑦) ∈
ℝ) | 
| 22 | 2 | a1i 11 | . . . . . . . 8
⊢ (𝑦 ∈ (0[,)+∞) → 0
∈ ℝ) | 
| 23 | 18 | simprbi 496 | . . . . . . . 8
⊢ (𝑦 ∈ (0[,)+∞) → 0
≤ 𝑦) | 
| 24 | 19 | ltp1d 12199 | . . . . . . . . 9
⊢ (𝑦 ∈ (0[,)+∞) →
𝑦 < (𝑦 + 1)) | 
| 25 |  | ax-1cn 11214 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 26 | 19 | recnd 11290 | . . . . . . . . . 10
⊢ (𝑦 ∈ (0[,)+∞) →
𝑦 ∈
ℂ) | 
| 27 |  | addcom 11448 | . . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → (1 + 𝑦) = (𝑦 + 1)) | 
| 28 | 25, 26, 27 | sylancr 587 | . . . . . . . . 9
⊢ (𝑦 ∈ (0[,)+∞) → (1
+ 𝑦) = (𝑦 + 1)) | 
| 29 | 24, 28 | breqtrrd 5170 | . . . . . . . 8
⊢ (𝑦 ∈ (0[,)+∞) →
𝑦 < (1 + 𝑦)) | 
| 30 | 22, 19, 21, 23, 29 | lelttrd 11420 | . . . . . . 7
⊢ (𝑦 ∈ (0[,)+∞) → 0
< (1 + 𝑦)) | 
| 31 | 21, 30 | elrpd 13075 | . . . . . 6
⊢ (𝑦 ∈ (0[,)+∞) → (1
+ 𝑦) ∈
ℝ+) | 
| 32 | 19, 31 | rerpdivcld 13109 | . . . . 5
⊢ (𝑦 ∈ (0[,)+∞) →
(𝑦 / (1 + 𝑦)) ∈
ℝ) | 
| 33 |  | divge0 12138 | . . . . . 6
⊢ (((𝑦 ∈ ℝ ∧ 0 ≤
𝑦) ∧ ((1 + 𝑦) ∈ ℝ ∧ 0 < (1
+ 𝑦))) → 0 ≤ (𝑦 / (1 + 𝑦))) | 
| 34 | 19, 23, 21, 30, 33 | syl22anc 838 | . . . . 5
⊢ (𝑦 ∈ (0[,)+∞) → 0
≤ (𝑦 / (1 + 𝑦))) | 
| 35 | 21 | recnd 11290 | . . . . . . . 8
⊢ (𝑦 ∈ (0[,)+∞) → (1
+ 𝑦) ∈
ℂ) | 
| 36 | 35 | mulridd 11279 | . . . . . . 7
⊢ (𝑦 ∈ (0[,)+∞) →
((1 + 𝑦) · 1) = (1 +
𝑦)) | 
| 37 | 29, 36 | breqtrrd 5170 | . . . . . 6
⊢ (𝑦 ∈ (0[,)+∞) →
𝑦 < ((1 + 𝑦) · 1)) | 
| 38 | 8 | a1i 11 | . . . . . . 7
⊢ (𝑦 ∈ (0[,)+∞) → 1
∈ ℝ) | 
| 39 |  | ltdivmul 12144 | . . . . . . 7
⊢ ((𝑦 ∈ ℝ ∧ 1 ∈
ℝ ∧ ((1 + 𝑦)
∈ ℝ ∧ 0 < (1 + 𝑦))) → ((𝑦 / (1 + 𝑦)) < 1 ↔ 𝑦 < ((1 + 𝑦) · 1))) | 
| 40 | 19, 38, 21, 30, 39 | syl112anc 1375 | . . . . . 6
⊢ (𝑦 ∈ (0[,)+∞) →
((𝑦 / (1 + 𝑦)) < 1 ↔ 𝑦 < ((1 + 𝑦) · 1))) | 
| 41 | 37, 40 | mpbird 257 | . . . . 5
⊢ (𝑦 ∈ (0[,)+∞) →
(𝑦 / (1 + 𝑦)) < 1) | 
| 42 |  | elico2 13452 | . . . . . 6
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ*) → ((𝑦 / (1 + 𝑦)) ∈ (0[,)1) ↔ ((𝑦 / (1 + 𝑦)) ∈ ℝ ∧ 0 ≤ (𝑦 / (1 + 𝑦)) ∧ (𝑦 / (1 + 𝑦)) < 1))) | 
| 43 | 2, 3, 42 | mp2an 692 | . . . . 5
⊢ ((𝑦 / (1 + 𝑦)) ∈ (0[,)1) ↔ ((𝑦 / (1 + 𝑦)) ∈ ℝ ∧ 0 ≤ (𝑦 / (1 + 𝑦)) ∧ (𝑦 / (1 + 𝑦)) < 1)) | 
| 44 | 32, 34, 41, 43 | syl3anbrc 1343 | . . . 4
⊢ (𝑦 ∈ (0[,)+∞) →
(𝑦 / (1 + 𝑦)) ∈
(0[,)1)) | 
| 45 | 44 | adantl 481 | . . 3
⊢
((⊤ ∧ 𝑦
∈ (0[,)+∞)) → (𝑦 / (1 + 𝑦)) ∈ (0[,)1)) | 
| 46 | 26 | adantl 481 | . . . . . . . . 9
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
𝑦 ∈
ℂ) | 
| 47 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
𝑥 ∈
ℝ) | 
| 48 | 47 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
𝑥 ∈
ℂ) | 
| 49 | 48, 46 | mulcld 11282 | . . . . . . . . 9
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(𝑥 · 𝑦) ∈
ℂ) | 
| 50 | 46, 49, 48 | subadd2d 11640 | . . . . . . . 8
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((𝑦 − (𝑥 · 𝑦)) = 𝑥 ↔ (𝑥 + (𝑥 · 𝑦)) = 𝑦)) | 
| 51 |  | 1cnd 11257 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → 1
∈ ℂ) | 
| 52 | 51, 48, 46 | subdird 11721 | . . . . . . . . . 10
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((1 − 𝑥) ·
𝑦) = ((1 · 𝑦) − (𝑥 · 𝑦))) | 
| 53 | 46 | mullidd 11280 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(1 · 𝑦) = 𝑦) | 
| 54 | 53 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((1 · 𝑦) −
(𝑥 · 𝑦)) = (𝑦 − (𝑥 · 𝑦))) | 
| 55 | 52, 54 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((1 − 𝑥) ·
𝑦) = (𝑦 − (𝑥 · 𝑦))) | 
| 56 | 55 | eqeq1d 2738 | . . . . . . . 8
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(((1 − 𝑥) ·
𝑦) = 𝑥 ↔ (𝑦 − (𝑥 · 𝑦)) = 𝑥)) | 
| 57 | 48, 51, 46 | adddid 11286 | . . . . . . . . . 10
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(𝑥 · (1 + 𝑦)) = ((𝑥 · 1) + (𝑥 · 𝑦))) | 
| 58 | 48 | mulridd 11279 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(𝑥 · 1) = 𝑥) | 
| 59 | 58 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((𝑥 · 1) + (𝑥 · 𝑦)) = (𝑥 + (𝑥 · 𝑦))) | 
| 60 | 57, 59 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(𝑥 · (1 + 𝑦)) = (𝑥 + (𝑥 · 𝑦))) | 
| 61 | 60 | eqeq1d 2738 | . . . . . . . 8
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((𝑥 · (1 + 𝑦)) = 𝑦 ↔ (𝑥 + (𝑥 · 𝑦)) = 𝑦)) | 
| 62 | 50, 56, 61 | 3bitr4rd 312 | . . . . . . 7
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((𝑥 · (1 + 𝑦)) = 𝑦 ↔ ((1 − 𝑥) · 𝑦) = 𝑥)) | 
| 63 |  | eqcom 2743 | . . . . . . 7
⊢ (𝑦 = (𝑥 · (1 + 𝑦)) ↔ (𝑥 · (1 + 𝑦)) = 𝑦) | 
| 64 |  | eqcom 2743 | . . . . . . 7
⊢ (𝑥 = ((1 − 𝑥) · 𝑦) ↔ ((1 − 𝑥) · 𝑦) = 𝑥) | 
| 65 | 62, 63, 64 | 3bitr4g 314 | . . . . . 6
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(𝑦 = (𝑥 · (1 + 𝑦)) ↔ 𝑥 = ((1 − 𝑥) · 𝑦))) | 
| 66 | 35 | adantl 481 | . . . . . . 7
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(1 + 𝑦) ∈
ℂ) | 
| 67 | 31 | adantl 481 | . . . . . . . 8
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(1 + 𝑦) ∈
ℝ+) | 
| 68 | 67 | rpne0d 13083 | . . . . . . 7
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(1 + 𝑦) ≠
0) | 
| 69 | 46, 48, 66, 68 | divmul3d 12078 | . . . . . 6
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((𝑦 / (1 + 𝑦)) = 𝑥 ↔ 𝑦 = (𝑥 · (1 + 𝑦)))) | 
| 70 | 11 | adantr 480 | . . . . . . . 8
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(1 − 𝑥) ∈
ℝ+) | 
| 71 | 70 | rpcnd 13080 | . . . . . . 7
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(1 − 𝑥) ∈
ℂ) | 
| 72 | 70 | rpne0d 13083 | . . . . . . 7
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(1 − 𝑥) ≠
0) | 
| 73 | 48, 46, 71, 72 | divmul2d 12077 | . . . . . 6
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((𝑥 / (1 − 𝑥)) = 𝑦 ↔ 𝑥 = ((1 − 𝑥) · 𝑦))) | 
| 74 | 65, 69, 73 | 3bitr4d 311 | . . . . 5
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
((𝑦 / (1 + 𝑦)) = 𝑥 ↔ (𝑥 / (1 − 𝑥)) = 𝑦)) | 
| 75 |  | eqcom 2743 | . . . . 5
⊢ (𝑥 = (𝑦 / (1 + 𝑦)) ↔ (𝑦 / (1 + 𝑦)) = 𝑥) | 
| 76 |  | eqcom 2743 | . . . . 5
⊢ (𝑦 = (𝑥 / (1 − 𝑥)) ↔ (𝑥 / (1 − 𝑥)) = 𝑦) | 
| 77 | 74, 75, 76 | 3bitr4g 314 | . . . 4
⊢ ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) →
(𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = (𝑥 / (1 − 𝑥)))) | 
| 78 | 77 | adantl 481 | . . 3
⊢
((⊤ ∧ (𝑥
∈ (0[,)1) ∧ 𝑦
∈ (0[,)+∞))) → (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = (𝑥 / (1 − 𝑥)))) | 
| 79 | 1, 17, 45, 78 | f1ocnv2d 7687 | . 2
⊢ (⊤
→ (𝐹:(0[,)1)–1-1-onto→(0[,)+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,)+∞) ↦ (𝑦 / (1 + 𝑦))))) | 
| 80 | 79 | mptru 1546 | 1
⊢ (𝐹:(0[,)1)–1-1-onto→(0[,)+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,)+∞) ↦ (𝑦 / (1 + 𝑦)))) |