Step | Hyp | Ref
| Expression |
1 | | inss1 3795 |
. . . . . . . 8
⊢ (𝐵 ∩ (1[,)+∞)) ⊆
𝐵 |
2 | | resmpt 5369 |
. . . . . . . 8
⊢ ((𝐵 ∩ (1[,)+∞)) ⊆
𝐵 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
3 | 1, 2 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
4 | | 0xr 9965 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
5 | | 0lt1 10429 |
. . . . . . . . . . 11
⊢ 0 <
1 |
6 | | df-ioo 12050 |
. . . . . . . . . . . 12
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
7 | | df-ico 12052 |
. . . . . . . . . . . 12
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
8 | | xrltletr 11864 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤)) |
9 | 6, 7, 8 | ixxss1 12064 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆
(0(,)+∞)) |
10 | 4, 5, 9 | mp2an 704 |
. . . . . . . . . 10
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
11 | | ioorp 12122 |
. . . . . . . . . 10
⊢
(0(,)+∞) = ℝ+ |
12 | 10, 11 | sseqtri 3600 |
. . . . . . . . 9
⊢
(1[,)+∞) ⊆ ℝ+ |
13 | | sslin 3801 |
. . . . . . . . 9
⊢
((1[,)+∞) ⊆ ℝ+ → (𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩
ℝ+)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐵 ∩ (1[,)+∞)) ⊆
(𝐵 ∩
ℝ+) |
15 | | resmpt 5369 |
. . . . . . . 8
⊢ ((𝐵 ∩ (1[,)+∞)) ⊆
(𝐵 ∩
ℝ+) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
16 | 14, 15 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆)) |
17 | 3, 16 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞)))) |
18 | | resres 5329 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) |
19 | | resres 5329 |
. . . . . 6
⊢ (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) |
20 | 17, 18, 19 | 3eqtr4g 2669 |
. . . . 5
⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞))) |
21 | | rlimcnp2.r |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) |
22 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = (𝑦 ∈ 𝐵 ↦ 𝑆) |
23 | 21, 22 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ 𝑆):𝐵⟶ℂ) |
24 | | ffn 5958 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ↦ 𝑆):𝐵⟶ℂ → (𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵) |
26 | | fnresdm 5914 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ 𝐵 ↦ 𝑆)) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ 𝐵 ↦ 𝑆)) |
28 | 27 | reseq1d 5316 |
. . . . 5
⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞))) |
29 | | inss1 3795 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ ℝ+)
⊆ 𝐵 |
30 | 29 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐵 ∩ ℝ+) → 𝑦 ∈ 𝐵) |
31 | 30, 21 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑆 ∈
ℂ) |
32 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) |
33 | 31, 32 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩
ℝ+)⟶ℂ) |
34 | | frel 5963 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩ ℝ+)⟶ℂ
→ Rel (𝑦 ∈ (𝐵 ∩ ℝ+)
↦ 𝑆)) |
35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Rel (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
36 | 32, 31 | dmmptd 5937 |
. . . . . . . 8
⊢ (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝐵 ∩
ℝ+)) |
37 | 36, 29 | syl6eqss 3618 |
. . . . . . 7
⊢ (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵) |
38 | | relssres 5357 |
. . . . . . 7
⊢ ((Rel
(𝑦 ∈ (𝐵 ∩ ℝ+)
↦ 𝑆) ∧ dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
39 | 35, 37, 38 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
40 | 39 | reseq1d 5316 |
. . . . 5
⊢ (𝜑 → (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾
(1[,)+∞))) |
41 | 20, 28, 40 | 3eqtr3d 2652 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾
(1[,)+∞))) |
42 | 41 | breq1d 4593 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶)) |
43 | | rlimcnp2.b |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
44 | | 1red 9934 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
45 | 23, 43, 44 | rlimresb 14144 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶)) |
46 | 29, 43 | syl5ss 3579 |
. . . 4
⊢ (𝜑 → (𝐵 ∩ ℝ+) ⊆
ℝ) |
47 | 33, 46, 44 | rlimresb 14144 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟
𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞))
⇝𝑟 𝐶)) |
48 | 42, 45, 47 | 3bitr4d 299 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟
𝐶)) |
49 | | inss2 3796 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ ℝ+)
⊆ ℝ+ |
50 | 49 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∩ ℝ+) ⊆
ℝ+) |
51 | 50 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑦 ∈
ℝ+) |
52 | 51 | rpreccld 11758 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 /
𝑦) ∈
ℝ+) |
53 | 52 | rpne0d 11753 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 /
𝑦) ≠ 0) |
54 | 53 | neneqd 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → ¬ (1
/ 𝑦) = 0) |
55 | 54 | iffalsed 4047 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅) = ⦋(1 / 𝑦) / 𝑥⦌𝑅) |
56 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = (1 / 𝑦) → (1 / 𝑥) = (1 / (1 / 𝑦))) |
57 | | rpcnne0 11726 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ+
→ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
58 | | recrec 10601 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / (1 / 𝑦)) = 𝑦) |
59 | 51, 57, 58 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / (1
/ 𝑦)) = 𝑦) |
60 | 56, 59 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → (1 / 𝑥) = 𝑦) |
61 | 60 | eqcomd 2616 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑦 = (1 / 𝑥)) |
62 | | rlimcnp2.s |
. . . . . . . 8
⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅) |
63 | 61, 62 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑆 = 𝑅) |
64 | 63 | eqcomd 2616 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑅 = 𝑆) |
65 | 52, 64 | csbied 3526 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) →
⦋(1 / 𝑦) /
𝑥⦌𝑅 = 𝑆) |
66 | 55, 65 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) → if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅) = 𝑆) |
67 | 66 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)) |
68 | 67 | breq1d 4593 |
. 2
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟
𝐶)) |
69 | | rlimcnp2.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) |
70 | | rlimcnp2.0 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝐴) |
71 | | rlimcnp2.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
72 | 71 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 = 0) → 𝐶 ∈ ℂ) |
73 | 69 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ (0[,)+∞)) |
74 | | 0re 9919 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
75 | | pnfxr 9971 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
76 | | elico2 12108 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑤 ∈ (0[,)+∞) ↔
(𝑤 ∈ ℝ ∧ 0
≤ 𝑤 ∧ 𝑤 <
+∞))) |
77 | 74, 75, 76 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (0[,)+∞) ↔
(𝑤 ∈ ℝ ∧ 0
≤ 𝑤 ∧ 𝑤 <
+∞)) |
78 | 73, 77 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < +∞)) |
79 | 78 | simp1d 1066 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ) |
80 | 79 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ) |
81 | 78 | simp2d 1067 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 0 ≤ 𝑤) |
82 | | leloe 10003 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 𝑤
∈ ℝ) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤))) |
83 | 74, 79, 82 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤))) |
84 | 81, 83 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (0 < 𝑤 ∨ 0 = 𝑤)) |
85 | 84 | ord 391 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 0 < 𝑤 → 0 = 𝑤)) |
86 | | eqcom 2617 |
. . . . . . . . . . . 12
⊢ (0 =
𝑤 ↔ 𝑤 = 0) |
87 | 85, 86 | syl6ib 240 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 0 < 𝑤 → 𝑤 = 0)) |
88 | 87 | con1d 138 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 𝑤 = 0 → 0 < 𝑤)) |
89 | 88 | imp 444 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 0 < 𝑤) |
90 | 80, 89 | elrpd 11745 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ+) |
91 | | rpcnne0 11726 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℝ+
→ (𝑤 ∈ ℂ
∧ 𝑤 ≠
0)) |
92 | | recrec 10601 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) → (1 / (1 / 𝑤)) = 𝑤) |
93 | 91, 92 | syl 17 |
. . . . . . . 8
⊢ (𝑤 ∈ ℝ+
→ (1 / (1 / 𝑤)) =
𝑤) |
94 | 90, 93 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) = 𝑤) |
95 | 94 | csbeq1d 3506 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅 = ⦋𝑤 / 𝑥⦌𝑅) |
96 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ 𝐴) |
97 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝜑) |
98 | | rpreccl 11733 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℝ+
→ (1 / 𝑤) ∈
ℝ+) |
99 | 98 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (1 /
𝑤) ∈
ℝ+) |
100 | | rlimcnp2.d |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) |
101 | 100 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) |
102 | 101 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∀𝑦 ∈
ℝ+ (𝑦
∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) |
103 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (1 / 𝑤) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑤) ∈ 𝐵)) |
104 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (1 / 𝑤) → (1 / 𝑦) = (1 / (1 / 𝑤))) |
105 | 104 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (1 / 𝑤) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑤)) ∈ 𝐴)) |
106 | 103, 105 | bibi12d 334 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 / 𝑤) → ((𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴) ↔ ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))) |
107 | 106 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ ((1 /
𝑤) ∈
ℝ+ → (∀𝑦 ∈ ℝ+ (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴) → ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))) |
108 | 99, 102, 107 | sylc 63 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((1 /
𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴)) |
109 | 93 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (1 / (1 /
𝑤)) = 𝑤) |
110 | 109 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((1 / (1
/ 𝑤)) ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
111 | 108, 110 | bitr2d 268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ 𝐵)) |
112 | 97, 90, 111 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ 𝐵)) |
113 | 96, 112 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ 𝐵) |
114 | 90 | rpreccld 11758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈
ℝ+) |
115 | 113, 114 | elind 3760 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ (𝐵 ∩
ℝ+)) |
116 | 65, 31 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ+)) →
⦋(1 / 𝑦) /
𝑥⦌𝑅 ∈
ℂ) |
117 | 116 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (𝐵 ∩ ℝ+)⦋(1
/ 𝑦) / 𝑥⦌𝑅 ∈ ℂ) |
118 | 117 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ∀𝑦 ∈ (𝐵 ∩ ℝ+)⦋(1
/ 𝑦) / 𝑥⦌𝑅 ∈ ℂ) |
119 | 104 | csbeq1d 3506 |
. . . . . . . . 9
⊢ (𝑦 = (1 / 𝑤) → ⦋(1 / 𝑦) / 𝑥⦌𝑅 = ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅) |
120 | 119 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑦 = (1 / 𝑤) → (⦋(1 / 𝑦) / 𝑥⦌𝑅 ∈ ℂ ↔ ⦋(1 /
(1 / 𝑤)) / 𝑥⦌𝑅 ∈ ℂ)) |
121 | 120 | rspcv 3278 |
. . . . . . 7
⊢ ((1 /
𝑤) ∈ (𝐵 ∩ ℝ+)
→ (∀𝑦 ∈
(𝐵 ∩
ℝ+)⦋(1 / 𝑦) / 𝑥⦌𝑅 ∈ ℂ → ⦋(1 /
(1 / 𝑤)) / 𝑥⦌𝑅 ∈ ℂ)) |
122 | 115, 118,
121 | sylc 63 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅 ∈ ℂ) |
123 | 95, 122 | eqeltrrd 2689 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋𝑤 / 𝑥⦌𝑅 ∈ ℂ) |
124 | 72, 123 | ifclda 4070 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) ∈ ℂ) |
125 | 99 | biantrud 527 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((1 /
𝑤) ∈ 𝐵 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈
ℝ+))) |
126 | 111, 125 | bitrd 267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈
ℝ+))) |
127 | | elin 3758 |
. . . . 5
⊢ ((1 /
𝑤) ∈ (𝐵 ∩ ℝ+)
↔ ((1 / 𝑤) ∈
𝐵 ∧ (1 / 𝑤) ∈
ℝ+)) |
128 | 126, 127 | syl6bbr 277 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ (𝐵 ∩
ℝ+))) |
129 | | iftrue 4042 |
. . . 4
⊢ (𝑤 = 0 → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) = 𝐶) |
130 | | eqeq1 2614 |
. . . . 5
⊢ (𝑤 = (1 / 𝑦) → (𝑤 = 0 ↔ (1 / 𝑦) = 0)) |
131 | | csbeq1 3502 |
. . . . 5
⊢ (𝑤 = (1 / 𝑦) → ⦋𝑤 / 𝑥⦌𝑅 = ⦋(1 / 𝑦) / 𝑥⦌𝑅) |
132 | 130, 131 | ifbieq2d 4061 |
. . . 4
⊢ (𝑤 = (1 / 𝑦) → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) = if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) |
133 | | rlimcnp2.j |
. . . 4
⊢ 𝐽 =
(TopOpen‘ℂfld) |
134 | | rlimcnp2.k |
. . . 4
⊢ 𝐾 = (𝐽 ↾t 𝐴) |
135 | 69, 70, 50, 124, 128, 129, 132, 133, 134 | rlimcnp 24492 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝𝑟 𝐶 ↔ (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) |
136 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑤if(𝑥 = 0, 𝐶, 𝑅) |
137 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑥 𝑤 = 0 |
138 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥𝐶 |
139 | | nfcsb1v 3515 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑅 |
140 | 137, 138,
139 | nfif 4065 |
. . . . 5
⊢
Ⅎ𝑥if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) |
141 | | eqeq1 2614 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (𝑥 = 0 ↔ 𝑤 = 0)) |
142 | | csbeq1a 3508 |
. . . . . 6
⊢ (𝑥 = 𝑤 → 𝑅 = ⦋𝑤 / 𝑥⦌𝑅) |
143 | 141, 142 | ifbieq2d 4061 |
. . . . 5
⊢ (𝑥 = 𝑤 → if(𝑥 = 0, 𝐶, 𝑅) = if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) |
144 | 136, 140,
143 | cbvmpt 4677 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) = (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) |
145 | 144 | eleq1i 2679 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)) |
146 | 135, 145 | syl6bbr 277 |
. 2
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 /
𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) |
147 | 48, 68, 146 | 3bitr2d 295 |
1
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) |