Step | Hyp | Ref
| Expression |
1 | | inss1 3981 |
. . . . . . . 8
⊢ (𝐵 ∩ (1[,)+∞)) ⊆
𝐵 |
2 | | resmpt 5590 |
. . . . . . . 8
⊢ ((𝐵 ∩ (1[,)+∞)) ⊆
𝐵 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
3 | 1, 2 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
4 | | 0xr 10288 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
5 | | 0lt1 10752 |
. . . . . . . . . . 11
⊢ 0 <
1 |
6 | | df-ioo 12384 |
. . . . . . . . . . . 12
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
7 | | df-ico 12386 |
. . . . . . . . . . . 12
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
8 | | xrltletr 12193 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤)) |
9 | 6, 7, 8 | ixxss1 12398 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆
(0(,)+∞)) |
10 | 4, 5, 9 | mp2an 672 |
. . . . . . . . . 10
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
11 | | ioorp 12456 |
. . . . . . . . . 10
⊢
(0(,)+∞) = ℝ+ |
12 | 10, 11 | sseqtri 3786 |
. . . . . . . . 9
⊢
(1[,)+∞) ⊆ ℝ+ |
13 | | sslin 3987 |
. . . . . . . . 9
⊢
((1[,)+∞) ⊆ ℝ+ → (𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩
ℝ+)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐵 ∩ (1[,)+∞)) ⊆
(𝐵 ∩
ℝ+) |
15 | | resmpt 5590 |
. . . . . . . 8
⊢ ((𝐵 ∩ (1[,)+∞)) ⊆
(𝐵 ∩
ℝ+) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
16 | 14, 15 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
17 | 3, 16 | eqtr4d 2808 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞)))) |
18 | | resres 5550 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) |
19 | | resres 5550 |
. . . . . 6
⊢ (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) |
20 | 17, 18, 19 | 3eqtr4g 2830 |
. . . . 5
⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞))) |
21 | | rlimcnp2.r |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) |
22 | | eqid 2771 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = (𝑦 ∈ 𝐵 ↦ 𝑆) |
23 | 21, 22 | fmptd 6527 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ 𝑆):𝐵⟶ℂ) |
24 | | ffn 6185 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ↦ 𝑆):𝐵⟶ℂ → (𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵) |
26 | | fnresdm 6140 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ 𝐵 ↦ 𝑆)) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ 𝐵 ↦ 𝑆)) |
28 | 27 | reseq1d 5533 |
. . . . 5
⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞))) |
29 | | inss1 3981 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ ℝ+)
⊆ 𝐵 |
30 | 29 | sseli 3748 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐵 ∩ ℝ+) → 𝑦 ∈ 𝐵) |
31 | 30, 21 | sylan2 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑆 ∈
ℂ) |
32 | | eqid 2771 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) |
33 | 31, 32 | fmptd 6527 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩
ℝ+)⟶ℂ) |
34 | | frel 6190 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩ ℝ+)⟶ℂ
→ Rel (𝑦 ∈ (𝐵 ∩ ℝ+)
↦ 𝑆)) |
35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Rel (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
36 | 32, 31 | dmmptd 6164 |
. . . . . . . 8
⊢ (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝐵 ∩
ℝ+)) |
37 | 36, 29 | syl6eqss 3804 |
. . . . . . 7
⊢ (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵) |
38 | | relssres 5578 |
. . . . . . 7
⊢ ((Rel
(𝑦 ∈ (𝐵 ∩ ℝ+)
↦ 𝑆) ∧ dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
39 | 35, 37, 38 | syl2anc 573 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
40 | 39 | reseq1d 5533 |
. . . . 5
⊢ (𝜑 → (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾
(1[,)+∞))) |
41 | 20, 28, 40 | 3eqtr3d 2813 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾
(1[,)+∞))) |
42 | 41 | breq1d 4796 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶)) |
43 | | rlimcnp2.b |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
44 | | 1red 10257 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
45 | 23, 43, 44 | rlimresb 14504 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶)) |
46 | 29, 43 | syl5ss 3763 |
. . . 4
⊢ (𝜑 → (𝐵 ∩ ℝ+) ⊆
ℝ) |
47 | 33, 46, 44 | rlimresb 14504 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟
𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶)) |
48 | 42, 45, 47 | 3bitr4d 300 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟
𝐶)) |
49 | | inss2 3982 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ ℝ+)
⊆ ℝ+ |
50 | 49 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∩ ℝ+) ⊆
ℝ+) |
51 | 50 | sselda 3752 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑦 ∈
ℝ+) |
52 | 51 | rpreccld 12085 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 /
𝑦) ∈
ℝ+) |
53 | 52 | rpne0d 12080 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 /
𝑦) ≠ 0) |
54 | 53 | neneqd 2948 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → ¬ (1
/ 𝑦) = 0) |
55 | 54 | iffalsed 4236 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅) = ⦋(1 / 𝑦) / 𝑥⦌𝑅) |
56 | | oveq2 6801 |
. . . . . . . . . 10
⊢ (𝑥 = (1 / 𝑦) → (1 / 𝑥) = (1 / (1 / 𝑦))) |
57 | | rpcnne0 12053 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ+
→ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
58 | | recrec 10924 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / (1 / 𝑦)) = 𝑦) |
59 | 51, 57, 58 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / (1
/ 𝑦)) = 𝑦) |
60 | 56, 59 | sylan9eqr 2827 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → (1 / 𝑥) = 𝑦) |
61 | 60 | eqcomd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑦 = (1 / 𝑥)) |
62 | | rlimcnp2.s |
. . . . . . . 8
⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅) |
63 | 61, 62 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑆 = 𝑅) |
64 | 63 | eqcomd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑅 = 𝑆) |
65 | 52, 64 | csbied 3709 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) →
⦋(1 / 𝑦) /
𝑥⦌𝑅 = 𝑆) |
66 | 55, 65 | eqtrd 2805 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅) = 𝑆) |
67 | 66 | mpteq2dva 4878 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
68 | 67 | breq1d 4796 |
. 2
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟
𝐶)) |
69 | | rlimcnp2.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) |
70 | | rlimcnp2.0 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝐴) |
71 | | rlimcnp2.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
72 | 71 | ad2antrr 705 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 = 0) → 𝐶 ∈ ℂ) |
73 | 69 | sselda 3752 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ (0[,)+∞)) |
74 | | 0re 10242 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
75 | | pnfxr 10294 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
76 | | elico2 12442 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑤 ∈ (0[,)+∞) ↔
(𝑤 ∈ ℝ ∧ 0
≤ 𝑤 ∧ 𝑤 <
+∞))) |
77 | 74, 75, 76 | mp2an 672 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (0[,)+∞) ↔
(𝑤 ∈ ℝ ∧ 0
≤ 𝑤 ∧ 𝑤 <
+∞)) |
78 | 73, 77 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < +∞)) |
79 | 78 | simp1d 1136 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ) |
80 | 79 | adantr 466 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ) |
81 | 78 | simp2d 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 0 ≤ 𝑤) |
82 | | leloe 10326 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 𝑤
∈ ℝ) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤))) |
83 | 74, 79, 82 | sylancr 575 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤))) |
84 | 81, 83 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (0 < 𝑤 ∨ 0 = 𝑤)) |
85 | 84 | ord 853 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 0 < 𝑤 → 0 = 𝑤)) |
86 | | eqcom 2778 |
. . . . . . . . . . . 12
⊢ (0 =
𝑤 ↔ 𝑤 = 0) |
87 | 85, 86 | syl6ib 241 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 0 < 𝑤 → 𝑤 = 0)) |
88 | 87 | con1d 141 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 𝑤 = 0 → 0 < 𝑤)) |
89 | 88 | imp 393 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 0 < 𝑤) |
90 | 80, 89 | elrpd 12072 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ+) |
91 | | rpcnne0 12053 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℝ+
→ (𝑤 ∈ ℂ
∧ 𝑤 ≠
0)) |
92 | | recrec 10924 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) → (1 / (1 / 𝑤)) = 𝑤) |
93 | 91, 92 | syl 17 |
. . . . . . . 8
⊢ (𝑤 ∈ ℝ+
→ (1 / (1 / 𝑤)) =
𝑤) |
94 | 90, 93 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) = 𝑤) |
95 | 94 | csbeq1d 3689 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅 = ⦋𝑤 / 𝑥⦌𝑅) |
96 | | oveq2 6801 |
. . . . . . . . 9
⊢ (𝑦 = (1 / 𝑤) → (1 / 𝑦) = (1 / (1 / 𝑤))) |
97 | 96 | csbeq1d 3689 |
. . . . . . . 8
⊢ (𝑦 = (1 / 𝑤) → ⦋(1 / 𝑦) / 𝑥⦌𝑅 = ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅) |
98 | 97 | eleq1d 2835 |
. . . . . . 7
⊢ (𝑦 = (1 / 𝑤) → (⦋(1 / 𝑦) / 𝑥⦌𝑅 ∈ ℂ ↔ ⦋(1 /
(1 / 𝑤)) / 𝑥⦌𝑅 ∈ ℂ)) |
99 | 65, 31 | eqeltrd 2850 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) →
⦋(1 / 𝑦) /
𝑥⦌𝑅 ∈
ℂ) |
100 | 99 | ralrimiva 3115 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (𝐵 ∩ ℝ+)⦋(1
/ 𝑦) / 𝑥⦌𝑅 ∈ ℂ) |
101 | 100 | ad2antrr 705 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ∀𝑦 ∈ (𝐵 ∩ ℝ+)⦋(1
/ 𝑦) / 𝑥⦌𝑅 ∈ ℂ) |
102 | | simplr 752 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ 𝐴) |
103 | | simpll 750 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝜑) |
104 | | eleq1 2838 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 / 𝑤) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑤) ∈ 𝐵)) |
105 | 96 | eleq1d 2835 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 / 𝑤) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑤)) ∈ 𝐴)) |
106 | 104, 105 | bibi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑦 = (1 / 𝑤) → ((𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴) ↔ ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))) |
107 | | rlimcnp2.d |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) |
108 | 107 | ralrimiva 3115 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) |
109 | 108 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∀𝑦 ∈
ℝ+ (𝑦
∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) |
110 | | rpreccl 12060 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℝ+
→ (1 / 𝑤) ∈
ℝ+) |
111 | 110 | adantl 467 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (1 /
𝑤) ∈
ℝ+) |
112 | 106, 109,
111 | rspcdva 3466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((1 /
𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴)) |
113 | 93 | adantl 467 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (1 / (1 /
𝑤)) = 𝑤) |
114 | 113 | eleq1d 2835 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((1 / (1
/ 𝑤)) ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
115 | 112, 114 | bitr2d 269 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ 𝐵)) |
116 | 103, 90, 115 | syl2anc 573 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ 𝐵)) |
117 | 102, 116 | mpbid 222 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ 𝐵) |
118 | 90 | rpreccld 12085 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈
ℝ+) |
119 | 117, 118 | elind 3949 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ (𝐵 ∩
ℝ+)) |
120 | 98, 101, 119 | rspcdva 3466 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅 ∈ ℂ) |
121 | 95, 120 | eqeltrrd 2851 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋𝑤 / 𝑥⦌𝑅 ∈ ℂ) |
122 | 72, 121 | ifclda 4259 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) ∈ ℂ) |
123 | 111 | biantrud 521 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((1 /
𝑤) ∈ 𝐵 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈
ℝ+))) |
124 | 115, 123 | bitrd 268 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈
ℝ+))) |
125 | | elin 3947 |
. . . . 5
⊢ ((1 /
𝑤) ∈ (𝐵 ∩ ℝ+)
↔ ((1 / 𝑤) ∈
𝐵 ∧ (1 / 𝑤) ∈
ℝ+)) |
126 | 124, 125 | syl6bbr 278 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ (𝐵 ∩
ℝ+))) |
127 | | iftrue 4231 |
. . . 4
⊢ (𝑤 = 0 → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) = 𝐶) |
128 | | eqeq1 2775 |
. . . . 5
⊢ (𝑤 = (1 / 𝑦) → (𝑤 = 0 ↔ (1 / 𝑦) = 0)) |
129 | | csbeq1 3685 |
. . . . 5
⊢ (𝑤 = (1 / 𝑦) → ⦋𝑤 / 𝑥⦌𝑅 = ⦋(1 / 𝑦) / 𝑥⦌𝑅) |
130 | 128, 129 | ifbieq2d 4250 |
. . . 4
⊢ (𝑤 = (1 / 𝑦) → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) = if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) |
131 | | rlimcnp2.j |
. . . 4
⊢ 𝐽 =
(TopOpen‘ℂfld) |
132 | | rlimcnp2.k |
. . . 4
⊢ 𝐾 = (𝐽 ↾t 𝐴) |
133 | 69, 70, 50, 122, 126, 127, 130, 131, 132 | rlimcnp 24913 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝𝑟 𝐶 ↔ (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) |
134 | | nfcv 2913 |
. . . . 5
⊢
Ⅎ𝑤if(𝑥 = 0, 𝐶, 𝑅) |
135 | | nfv 1995 |
. . . . . 6
⊢
Ⅎ𝑥 𝑤 = 0 |
136 | | nfcv 2913 |
. . . . . 6
⊢
Ⅎ𝑥𝐶 |
137 | | nfcsb1v 3698 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑅 |
138 | 135, 136,
137 | nfif 4254 |
. . . . 5
⊢
Ⅎ𝑥if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) |
139 | | eqeq1 2775 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (𝑥 = 0 ↔ 𝑤 = 0)) |
140 | | csbeq1a 3691 |
. . . . . 6
⊢ (𝑥 = 𝑤 → 𝑅 = ⦋𝑤 / 𝑥⦌𝑅) |
141 | 139, 140 | ifbieq2d 4250 |
. . . . 5
⊢ (𝑥 = 𝑤 → if(𝑥 = 0, 𝐶, 𝑅) = if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) |
142 | 134, 138,
141 | cbvmpt 4883 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) = (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) |
143 | 142 | eleq1i 2841 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)) |
144 | 133, 143 | syl6bbr 278 |
. 2
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) |
145 | 48, 68, 144 | 3bitr2d 296 |
1
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) |