| Step | Hyp | Ref
| Expression |
| 1 | | inss1 4237 |
. . . . . . . 8
⊢ (𝐵 ∩ (1[,)+∞)) ⊆
𝐵 |
| 2 | | resmpt 6055 |
. . . . . . . 8
⊢ ((𝐵 ∩ (1[,)+∞)) ⊆
𝐵 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
| 3 | 1, 2 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
| 4 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 5 | | 0lt1 11785 |
. . . . . . . . . . 11
⊢ 0 <
1 |
| 6 | | df-ioo 13391 |
. . . . . . . . . . . 12
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
| 7 | | df-ico 13393 |
. . . . . . . . . . . 12
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 8 | | xrltletr 13199 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤)) |
| 9 | 6, 7, 8 | ixxss1 13405 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆
(0(,)+∞)) |
| 10 | 4, 5, 9 | mp2an 692 |
. . . . . . . . . 10
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
| 11 | | ioorp 13465 |
. . . . . . . . . 10
⊢
(0(,)+∞) = ℝ+ |
| 12 | 10, 11 | sseqtri 4032 |
. . . . . . . . 9
⊢
(1[,)+∞) ⊆ ℝ+ |
| 13 | | sslin 4243 |
. . . . . . . . 9
⊢
((1[,)+∞) ⊆ ℝ+ → (𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩
ℝ+)) |
| 14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐵 ∩ (1[,)+∞)) ⊆
(𝐵 ∩
ℝ+) |
| 15 | | resmpt 6055 |
. . . . . . . 8
⊢ ((𝐵 ∩ (1[,)+∞)) ⊆
(𝐵 ∩
ℝ+) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
| 16 | 14, 15 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
| 17 | 3, 16 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞)))) |
| 18 | | resres 6010 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) |
| 19 | | resres 6010 |
. . . . . 6
⊢ (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) |
| 20 | 17, 18, 19 | 3eqtr4g 2802 |
. . . . 5
⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞))) |
| 21 | | rlimcnp2.r |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) |
| 22 | 21 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ 𝑆):𝐵⟶ℂ) |
| 23 | 22 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵) |
| 24 | | fnresdm 6687 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ 𝐵 ↦ 𝑆)) |
| 25 | 23, 24 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ 𝐵 ↦ 𝑆)) |
| 26 | 25 | reseq1d 5996 |
. . . . 5
⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞))) |
| 27 | | elinel1 4201 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐵 ∩ ℝ+) → 𝑦 ∈ 𝐵) |
| 28 | 27, 21 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑆 ∈
ℂ) |
| 29 | 28 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩
ℝ+)⟶ℂ) |
| 30 | | frel 6741 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩ ℝ+)⟶ℂ
→ Rel (𝑦 ∈ (𝐵 ∩ ℝ+)
↦ 𝑆)) |
| 31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Rel (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
| 32 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) |
| 33 | 32, 28 | dmmptd 6713 |
. . . . . . . 8
⊢ (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝐵 ∩
ℝ+)) |
| 34 | | inss1 4237 |
. . . . . . . 8
⊢ (𝐵 ∩ ℝ+)
⊆ 𝐵 |
| 35 | 33, 34 | eqsstrdi 4028 |
. . . . . . 7
⊢ (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵) |
| 36 | | relssres 6040 |
. . . . . . 7
⊢ ((Rel
(𝑦 ∈ (𝐵 ∩ ℝ+)
↦ 𝑆) ∧ dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
| 37 | 31, 35, 36 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
| 38 | 37 | reseq1d 5996 |
. . . . 5
⊢ (𝜑 → (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾
(1[,)+∞))) |
| 39 | 20, 26, 38 | 3eqtr3d 2785 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾
(1[,)+∞))) |
| 40 | 39 | breq1d 5153 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶)) |
| 41 | | rlimcnp2.b |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
| 42 | | 1red 11262 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
| 43 | 22, 41, 42 | rlimresb 15601 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶)) |
| 44 | 34, 41 | sstrid 3995 |
. . . 4
⊢ (𝜑 → (𝐵 ∩ ℝ+) ⊆
ℝ) |
| 45 | 29, 44, 42 | rlimresb 15601 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟
𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶)) |
| 46 | 40, 43, 45 | 3bitr4d 311 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟
𝐶)) |
| 47 | | inss2 4238 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ ℝ+)
⊆ ℝ+ |
| 48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∩ ℝ+) ⊆
ℝ+) |
| 49 | 48 | sselda 3983 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑦 ∈
ℝ+) |
| 50 | 49 | rpreccld 13087 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 /
𝑦) ∈
ℝ+) |
| 51 | 50 | rpne0d 13082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 /
𝑦) ≠ 0) |
| 52 | 51 | neneqd 2945 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → ¬ (1
/ 𝑦) = 0) |
| 53 | 52 | iffalsed 4536 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅) = ⦋(1 / 𝑦) / 𝑥⦌𝑅) |
| 54 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = (1 / 𝑦) → (1 / 𝑥) = (1 / (1 / 𝑦))) |
| 55 | | rpcnne0 13053 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ+
→ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
| 56 | | recrec 11964 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / (1 / 𝑦)) = 𝑦) |
| 57 | 49, 55, 56 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / (1
/ 𝑦)) = 𝑦) |
| 58 | 54, 57 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → (1 / 𝑥) = 𝑦) |
| 59 | 58 | eqcomd 2743 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑦 = (1 / 𝑥)) |
| 60 | | rlimcnp2.s |
. . . . . . . 8
⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅) |
| 61 | 59, 60 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑆 = 𝑅) |
| 62 | 61 | eqcomd 2743 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑅 = 𝑆) |
| 63 | 50, 62 | csbied 3935 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) →
⦋(1 / 𝑦) /
𝑥⦌𝑅 = 𝑆) |
| 64 | 53, 63 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅) = 𝑆) |
| 65 | 64 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
| 66 | 65 | breq1d 5153 |
. 2
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟
𝐶)) |
| 67 | | rlimcnp2.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) |
| 68 | | rlimcnp2.0 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝐴) |
| 69 | | rlimcnp2.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 70 | 69 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 = 0) → 𝐶 ∈ ℂ) |
| 71 | 67 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ (0[,)+∞)) |
| 72 | | 0re 11263 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
| 73 | | pnfxr 11315 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
| 74 | | elico2 13451 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑤 ∈ (0[,)+∞) ↔
(𝑤 ∈ ℝ ∧ 0
≤ 𝑤 ∧ 𝑤 <
+∞))) |
| 75 | 72, 73, 74 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (0[,)+∞) ↔
(𝑤 ∈ ℝ ∧ 0
≤ 𝑤 ∧ 𝑤 <
+∞)) |
| 76 | 71, 75 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < +∞)) |
| 77 | 76 | simp1d 1143 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ) |
| 78 | 77 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ) |
| 79 | 76 | simp2d 1144 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 0 ≤ 𝑤) |
| 80 | | leloe 11347 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 𝑤
∈ ℝ) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤))) |
| 81 | 72, 77, 80 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤))) |
| 82 | 79, 81 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (0 < 𝑤 ∨ 0 = 𝑤)) |
| 83 | 82 | ord 865 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 0 < 𝑤 → 0 = 𝑤)) |
| 84 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ (0 =
𝑤 ↔ 𝑤 = 0) |
| 85 | 83, 84 | imbitrdi 251 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 0 < 𝑤 → 𝑤 = 0)) |
| 86 | 85 | con1d 145 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 𝑤 = 0 → 0 < 𝑤)) |
| 87 | 86 | imp 406 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 0 < 𝑤) |
| 88 | 78, 87 | elrpd 13074 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ+) |
| 89 | | rpcnne0 13053 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℝ+
→ (𝑤 ∈ ℂ
∧ 𝑤 ≠
0)) |
| 90 | | recrec 11964 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) → (1 / (1 / 𝑤)) = 𝑤) |
| 91 | 89, 90 | syl 17 |
. . . . . . . 8
⊢ (𝑤 ∈ ℝ+
→ (1 / (1 / 𝑤)) =
𝑤) |
| 92 | 88, 91 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) = 𝑤) |
| 93 | 92 | csbeq1d 3903 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅 = ⦋𝑤 / 𝑥⦌𝑅) |
| 94 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑦 = (1 / 𝑤) → (1 / 𝑦) = (1 / (1 / 𝑤))) |
| 95 | 94 | csbeq1d 3903 |
. . . . . . . 8
⊢ (𝑦 = (1 / 𝑤) → ⦋(1 / 𝑦) / 𝑥⦌𝑅 = ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅) |
| 96 | 95 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑦 = (1 / 𝑤) → (⦋(1 / 𝑦) / 𝑥⦌𝑅 ∈ ℂ ↔ ⦋(1 /
(1 / 𝑤)) / 𝑥⦌𝑅 ∈ ℂ)) |
| 97 | 63, 28 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) →
⦋(1 / 𝑦) /
𝑥⦌𝑅 ∈
ℂ) |
| 98 | 97 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (𝐵 ∩ ℝ+)⦋(1
/ 𝑦) / 𝑥⦌𝑅 ∈ ℂ) |
| 99 | 98 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ∀𝑦 ∈ (𝐵 ∩ ℝ+)⦋(1
/ 𝑦) / 𝑥⦌𝑅 ∈ ℂ) |
| 100 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ 𝐴) |
| 101 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝜑) |
| 102 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 / 𝑤) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑤) ∈ 𝐵)) |
| 103 | 94 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 / 𝑤) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑤)) ∈ 𝐴)) |
| 104 | 102, 103 | bibi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑦 = (1 / 𝑤) → ((𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴) ↔ ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))) |
| 105 | | rlimcnp2.d |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) |
| 106 | 105 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) |
| 107 | 106 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∀𝑦 ∈
ℝ+ (𝑦
∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) |
| 108 | | rpreccl 13061 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℝ+
→ (1 / 𝑤) ∈
ℝ+) |
| 109 | 108 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (1 /
𝑤) ∈
ℝ+) |
| 110 | 104, 107,
109 | rspcdva 3623 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((1 /
𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴)) |
| 111 | 91 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (1 / (1 /
𝑤)) = 𝑤) |
| 112 | 111 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((1 / (1
/ 𝑤)) ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
| 113 | 110, 112 | bitr2d 280 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ 𝐵)) |
| 114 | 101, 88, 113 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ 𝐵)) |
| 115 | 100, 114 | mpbid 232 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ 𝐵) |
| 116 | 88 | rpreccld 13087 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈
ℝ+) |
| 117 | 115, 116 | elind 4200 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ (𝐵 ∩
ℝ+)) |
| 118 | 96, 99, 117 | rspcdva 3623 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅 ∈ ℂ) |
| 119 | 93, 118 | eqeltrrd 2842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋𝑤 / 𝑥⦌𝑅 ∈ ℂ) |
| 120 | 70, 119 | ifclda 4561 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) ∈ ℂ) |
| 121 | 109 | biantrud 531 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((1 /
𝑤) ∈ 𝐵 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈
ℝ+))) |
| 122 | 113, 121 | bitrd 279 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈
ℝ+))) |
| 123 | | elin 3967 |
. . . . 5
⊢ ((1 /
𝑤) ∈ (𝐵 ∩ ℝ+)
↔ ((1 / 𝑤) ∈
𝐵 ∧ (1 / 𝑤) ∈
ℝ+)) |
| 124 | 122, 123 | bitr4di 289 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ (𝐵 ∩
ℝ+))) |
| 125 | | iftrue 4531 |
. . . 4
⊢ (𝑤 = 0 → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) = 𝐶) |
| 126 | | eqeq1 2741 |
. . . . 5
⊢ (𝑤 = (1 / 𝑦) → (𝑤 = 0 ↔ (1 / 𝑦) = 0)) |
| 127 | | csbeq1 3902 |
. . . . 5
⊢ (𝑤 = (1 / 𝑦) → ⦋𝑤 / 𝑥⦌𝑅 = ⦋(1 / 𝑦) / 𝑥⦌𝑅) |
| 128 | 126, 127 | ifbieq2d 4552 |
. . . 4
⊢ (𝑤 = (1 / 𝑦) → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) = if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) |
| 129 | | rlimcnp2.j |
. . . 4
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 130 | | rlimcnp2.k |
. . . 4
⊢ 𝐾 = (𝐽 ↾t 𝐴) |
| 131 | 67, 68, 48, 120, 124, 125, 128, 129, 130 | rlimcnp 27008 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝𝑟 𝐶 ↔ (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) |
| 132 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑤if(𝑥 = 0, 𝐶, 𝑅) |
| 133 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑥 𝑤 = 0 |
| 134 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥𝐶 |
| 135 | | nfcsb1v 3923 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑅 |
| 136 | 133, 134,
135 | nfif 4556 |
. . . . 5
⊢
Ⅎ𝑥if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) |
| 137 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (𝑥 = 0 ↔ 𝑤 = 0)) |
| 138 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑥 = 𝑤 → 𝑅 = ⦋𝑤 / 𝑥⦌𝑅) |
| 139 | 137, 138 | ifbieq2d 4552 |
. . . . 5
⊢ (𝑥 = 𝑤 → if(𝑥 = 0, 𝐶, 𝑅) = if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) |
| 140 | 132, 136,
139 | cbvmpt 5253 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) = (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) |
| 141 | 140 | eleq1i 2832 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)) |
| 142 | 131, 141 | bitr4di 289 |
. 2
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) |
| 143 | 46, 66, 142 | 3bitr2d 307 |
1
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) |