MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rlimcnp2 Structured version   Visualization version   GIF version

Theorem rlimcnp2 26918
Description: Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.)
Hypotheses
Ref Expression
rlimcnp2.a (𝜑𝐴 ⊆ (0[,)+∞))
rlimcnp2.0 (𝜑 → 0 ∈ 𝐴)
rlimcnp2.b (𝜑𝐵 ⊆ ℝ)
rlimcnp2.c (𝜑𝐶 ∈ ℂ)
rlimcnp2.r ((𝜑𝑦𝐵) → 𝑆 ∈ ℂ)
rlimcnp2.d ((𝜑𝑦 ∈ ℝ+) → (𝑦𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
rlimcnp2.s (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅)
rlimcnp2.j 𝐽 = (TopOpen‘ℂfld)
rlimcnp2.k 𝐾 = (𝐽t 𝐴)
Assertion
Ref Expression
rlimcnp2 (𝜑 → ((𝑦𝐵𝑆) ⇝𝑟 𝐶 ↔ (𝑥𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝜑,𝑥,𝑦   𝑦,𝑅   𝑥,𝑆
Allowed substitution hints:   𝑅(𝑥)   𝑆(𝑦)   𝐽(𝑥,𝑦)   𝐾(𝑥,𝑦)

Proof of Theorem rlimcnp2
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 4231 . . . . . . . 8 (𝐵 ∩ (1[,)+∞)) ⊆ 𝐵
2 resmpt 6046 . . . . . . . 8 ((𝐵 ∩ (1[,)+∞)) ⊆ 𝐵 → ((𝑦𝐵𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
31, 2mp1i 13 . . . . . . 7 (𝜑 → ((𝑦𝐵𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
4 0xr 11299 . . . . . . . . . . 11 0 ∈ ℝ*
5 0lt1 11774 . . . . . . . . . . 11 0 < 1
6 df-ioo 13368 . . . . . . . . . . . 12 (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
7 df-ico 13370 . . . . . . . . . . . 12 [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
8 xrltletr 13176 . . . . . . . . . . . 12 ((0 ∈ ℝ* ∧ 1 ∈ ℝ*𝑤 ∈ ℝ*) → ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤))
96, 7, 8ixxss1 13382 . . . . . . . . . . 11 ((0 ∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆ (0(,)+∞))
104, 5, 9mp2an 690 . . . . . . . . . 10 (1[,)+∞) ⊆ (0(,)+∞)
11 ioorp 13442 . . . . . . . . . 10 (0(,)+∞) = ℝ+
1210, 11sseqtri 4018 . . . . . . . . 9 (1[,)+∞) ⊆ ℝ+
13 sslin 4237 . . . . . . . . 9 ((1[,)+∞) ⊆ ℝ+ → (𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩ ℝ+))
1412, 13ax-mp 5 . . . . . . . 8 (𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩ ℝ+)
15 resmpt 6046 . . . . . . . 8 ((𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩ ℝ+) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
1614, 15mp1i 13 . . . . . . 7 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
173, 16eqtr4d 2771 . . . . . 6 (𝜑 → ((𝑦𝐵𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))))
18 resres 6002 . . . . . 6 (((𝑦𝐵𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦𝐵𝑆) ↾ (𝐵 ∩ (1[,)+∞)))
19 resres 6002 . . . . . 6 (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞)))
2017, 18, 193eqtr4g 2793 . . . . 5 (𝜑 → (((𝑦𝐵𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)))
21 rlimcnp2.r . . . . . . . . 9 ((𝜑𝑦𝐵) → 𝑆 ∈ ℂ)
2221fmpttd 7130 . . . . . . . 8 (𝜑 → (𝑦𝐵𝑆):𝐵⟶ℂ)
2322ffnd 6728 . . . . . . 7 (𝜑 → (𝑦𝐵𝑆) Fn 𝐵)
24 fnresdm 6679 . . . . . . 7 ((𝑦𝐵𝑆) Fn 𝐵 → ((𝑦𝐵𝑆) ↾ 𝐵) = (𝑦𝐵𝑆))
2523, 24syl 17 . . . . . 6 (𝜑 → ((𝑦𝐵𝑆) ↾ 𝐵) = (𝑦𝐵𝑆))
2625reseq1d 5988 . . . . 5 (𝜑 → (((𝑦𝐵𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦𝐵𝑆) ↾ (1[,)+∞)))
27 elinel1 4197 . . . . . . . . . 10 (𝑦 ∈ (𝐵 ∩ ℝ+) → 𝑦𝐵)
2827, 21sylan2 591 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑆 ∈ ℂ)
2928fmpttd 7130 . . . . . . . 8 (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩ ℝ+)⟶ℂ)
30 frel 6732 . . . . . . . 8 ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩ ℝ+)⟶ℂ → Rel (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
3129, 30syl 17 . . . . . . 7 (𝜑 → Rel (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
32 eqid 2728 . . . . . . . . 9 (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)
3332, 28dmmptd 6705 . . . . . . . 8 (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝐵 ∩ ℝ+))
34 inss1 4231 . . . . . . . 8 (𝐵 ∩ ℝ+) ⊆ 𝐵
3533, 34eqsstrdi 4036 . . . . . . 7 (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵)
36 relssres 6031 . . . . . . 7 ((Rel (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ∧ dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
3731, 35, 36syl2anc 582 . . . . . 6 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
3837reseq1d 5988 . . . . 5 (𝜑 → (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞)))
3920, 26, 383eqtr3d 2776 . . . 4 (𝜑 → ((𝑦𝐵𝑆) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞)))
4039breq1d 5162 . . 3 (𝜑 → (((𝑦𝐵𝑆) ↾ (1[,)+∞)) ⇝𝑟 𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞)) ⇝𝑟 𝐶))
41 rlimcnp2.b . . . 4 (𝜑𝐵 ⊆ ℝ)
42 1red 11253 . . . 4 (𝜑 → 1 ∈ ℝ)
4322, 41, 42rlimresb 15549 . . 3 (𝜑 → ((𝑦𝐵𝑆) ⇝𝑟 𝐶 ↔ ((𝑦𝐵𝑆) ↾ (1[,)+∞)) ⇝𝑟 𝐶))
4434, 41sstrid 3993 . . . 4 (𝜑 → (𝐵 ∩ ℝ+) ⊆ ℝ)
4529, 44, 42rlimresb 15549 . . 3 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟 𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞)) ⇝𝑟 𝐶))
4640, 43, 453bitr4d 310 . 2 (𝜑 → ((𝑦𝐵𝑆) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟 𝐶))
47 inss2 4232 . . . . . . . . . . 11 (𝐵 ∩ ℝ+) ⊆ ℝ+
4847a1i 11 . . . . . . . . . 10 (𝜑 → (𝐵 ∩ ℝ+) ⊆ ℝ+)
4948sselda 3982 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑦 ∈ ℝ+)
5049rpreccld 13066 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / 𝑦) ∈ ℝ+)
5150rpne0d 13061 . . . . . . 7 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / 𝑦) ≠ 0)
5251neneqd 2942 . . . . . 6 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → ¬ (1 / 𝑦) = 0)
5352iffalsed 4543 . . . . 5 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅) = (1 / 𝑦) / 𝑥𝑅)
54 oveq2 7434 . . . . . . . . . 10 (𝑥 = (1 / 𝑦) → (1 / 𝑥) = (1 / (1 / 𝑦)))
55 rpcnne0 13032 . . . . . . . . . . 11 (𝑦 ∈ ℝ+ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
56 recrec 11949 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / (1 / 𝑦)) = 𝑦)
5749, 55, 563syl 18 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / (1 / 𝑦)) = 𝑦)
5854, 57sylan9eqr 2790 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → (1 / 𝑥) = 𝑦)
5958eqcomd 2734 . . . . . . . 8 (((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑦 = (1 / 𝑥))
60 rlimcnp2.s . . . . . . . 8 (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅)
6159, 60syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑆 = 𝑅)
6261eqcomd 2734 . . . . . 6 (((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑅 = 𝑆)
6350, 62csbied 3932 . . . . 5 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / 𝑦) / 𝑥𝑅 = 𝑆)
6453, 63eqtrd 2768 . . . 4 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅) = 𝑆)
6564mpteq2dva 5252 . . 3 (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅)) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
6665breq1d 5162 . 2 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅)) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟 𝐶))
67 rlimcnp2.a . . . 4 (𝜑𝐴 ⊆ (0[,)+∞))
68 rlimcnp2.0 . . . 4 (𝜑 → 0 ∈ 𝐴)
69 rlimcnp2.c . . . . . 6 (𝜑𝐶 ∈ ℂ)
7069ad2antrr 724 . . . . 5 (((𝜑𝑤𝐴) ∧ 𝑤 = 0) → 𝐶 ∈ ℂ)
7167sselda 3982 . . . . . . . . . . . 12 ((𝜑𝑤𝐴) → 𝑤 ∈ (0[,)+∞))
72 0re 11254 . . . . . . . . . . . . 13 0 ∈ ℝ
73 pnfxr 11306 . . . . . . . . . . . . 13 +∞ ∈ ℝ*
74 elico2 13428 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑤 ∈ (0[,)+∞) ↔ (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤𝑤 < +∞)))
7572, 73, 74mp2an 690 . . . . . . . . . . . 12 (𝑤 ∈ (0[,)+∞) ↔ (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤𝑤 < +∞))
7671, 75sylib 217 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤𝑤 < +∞))
7776simp1d 1139 . . . . . . . . . 10 ((𝜑𝑤𝐴) → 𝑤 ∈ ℝ)
7877adantr 479 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ)
7976simp2d 1140 . . . . . . . . . . . . . 14 ((𝜑𝑤𝐴) → 0 ≤ 𝑤)
80 leloe 11338 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝑤 ∈ ℝ) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤)))
8172, 77, 80sylancr 585 . . . . . . . . . . . . . 14 ((𝜑𝑤𝐴) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤)))
8279, 81mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑤𝐴) → (0 < 𝑤 ∨ 0 = 𝑤))
8382ord 862 . . . . . . . . . . . 12 ((𝜑𝑤𝐴) → (¬ 0 < 𝑤 → 0 = 𝑤))
84 eqcom 2735 . . . . . . . . . . . 12 (0 = 𝑤𝑤 = 0)
8583, 84imbitrdi 250 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (¬ 0 < 𝑤𝑤 = 0))
8685con1d 145 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (¬ 𝑤 = 0 → 0 < 𝑤))
8786imp 405 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 0 < 𝑤)
8878, 87elrpd 13053 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ+)
89 rpcnne0 13032 . . . . . . . . 9 (𝑤 ∈ ℝ+ → (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0))
90 recrec 11949 . . . . . . . . 9 ((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) → (1 / (1 / 𝑤)) = 𝑤)
9189, 90syl 17 . . . . . . . 8 (𝑤 ∈ ℝ+ → (1 / (1 / 𝑤)) = 𝑤)
9288, 91syl 17 . . . . . . 7 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) = 𝑤)
9392csbeq1d 3898 . . . . . 6 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) / 𝑥𝑅 = 𝑤 / 𝑥𝑅)
94 oveq2 7434 . . . . . . . . 9 (𝑦 = (1 / 𝑤) → (1 / 𝑦) = (1 / (1 / 𝑤)))
9594csbeq1d 3898 . . . . . . . 8 (𝑦 = (1 / 𝑤) → (1 / 𝑦) / 𝑥𝑅 = (1 / (1 / 𝑤)) / 𝑥𝑅)
9695eleq1d 2814 . . . . . . 7 (𝑦 = (1 / 𝑤) → ((1 / 𝑦) / 𝑥𝑅 ∈ ℂ ↔ (1 / (1 / 𝑤)) / 𝑥𝑅 ∈ ℂ))
9763, 28eqeltrd 2829 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / 𝑦) / 𝑥𝑅 ∈ ℂ)
9897ralrimiva 3143 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (𝐵 ∩ ℝ+)(1 / 𝑦) / 𝑥𝑅 ∈ ℂ)
9998ad2antrr 724 . . . . . . 7 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → ∀𝑦 ∈ (𝐵 ∩ ℝ+)(1 / 𝑦) / 𝑥𝑅 ∈ ℂ)
100 simplr 767 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝑤𝐴)
101 simpll 765 . . . . . . . . . 10 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝜑)
102 eleq1 2817 . . . . . . . . . . . . 13 (𝑦 = (1 / 𝑤) → (𝑦𝐵 ↔ (1 / 𝑤) ∈ 𝐵))
10394eleq1d 2814 . . . . . . . . . . . . 13 (𝑦 = (1 / 𝑤) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))
104102, 103bibi12d 344 . . . . . . . . . . . 12 (𝑦 = (1 / 𝑤) → ((𝑦𝐵 ↔ (1 / 𝑦) ∈ 𝐴) ↔ ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴)))
105 rlimcnp2.d . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ+) → (𝑦𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
106105ralrimiva 3143 . . . . . . . . . . . . 13 (𝜑 → ∀𝑦 ∈ ℝ+ (𝑦𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
107106adantr 479 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → ∀𝑦 ∈ ℝ+ (𝑦𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
108 rpreccl 13040 . . . . . . . . . . . . 13 (𝑤 ∈ ℝ+ → (1 / 𝑤) ∈ ℝ+)
109108adantl 480 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → (1 / 𝑤) ∈ ℝ+)
110104, 107, 109rspcdva 3612 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+) → ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))
11191adantl 480 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → (1 / (1 / 𝑤)) = 𝑤)
112111eleq1d 2814 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+) → ((1 / (1 / 𝑤)) ∈ 𝐴𝑤𝐴))
113110, 112bitr2d 279 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+) → (𝑤𝐴 ↔ (1 / 𝑤) ∈ 𝐵))
114101, 88, 113syl2anc 582 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (𝑤𝐴 ↔ (1 / 𝑤) ∈ 𝐵))
115100, 114mpbid 231 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ 𝐵)
11688rpreccld 13066 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ ℝ+)
117115, 116elind 4196 . . . . . . 7 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ (𝐵 ∩ ℝ+))
11896, 99, 117rspcdva 3612 . . . . . 6 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) / 𝑥𝑅 ∈ ℂ)
11993, 118eqeltrrd 2830 . . . . 5 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 / 𝑥𝑅 ∈ ℂ)
12070, 119ifclda 4567 . . . 4 ((𝜑𝑤𝐴) → if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅) ∈ ℂ)
121109biantrud 530 . . . . . 6 ((𝜑𝑤 ∈ ℝ+) → ((1 / 𝑤) ∈ 𝐵 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈ ℝ+)))
122113, 121bitrd 278 . . . . 5 ((𝜑𝑤 ∈ ℝ+) → (𝑤𝐴 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈ ℝ+)))
123 elin 3965 . . . . 5 ((1 / 𝑤) ∈ (𝐵 ∩ ℝ+) ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈ ℝ+))
124122, 123bitr4di 288 . . . 4 ((𝜑𝑤 ∈ ℝ+) → (𝑤𝐴 ↔ (1 / 𝑤) ∈ (𝐵 ∩ ℝ+)))
125 iftrue 4538 . . . 4 (𝑤 = 0 → if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅) = 𝐶)
126 eqeq1 2732 . . . . 5 (𝑤 = (1 / 𝑦) → (𝑤 = 0 ↔ (1 / 𝑦) = 0))
127 csbeq1 3897 . . . . 5 (𝑤 = (1 / 𝑦) → 𝑤 / 𝑥𝑅 = (1 / 𝑦) / 𝑥𝑅)
128126, 127ifbieq2d 4558 . . . 4 (𝑤 = (1 / 𝑦) → if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅) = if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅))
129 rlimcnp2.j . . . 4 𝐽 = (TopOpen‘ℂfld)
130 rlimcnp2.k . . . 4 𝐾 = (𝐽t 𝐴)
13167, 68, 48, 120, 124, 125, 128, 129, 130rlimcnp 26917 . . 3 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅)) ⇝𝑟 𝐶 ↔ (𝑤𝐴 ↦ if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
132 nfcv 2899 . . . . 5 𝑤if(𝑥 = 0, 𝐶, 𝑅)
133 nfv 1909 . . . . . 6 𝑥 𝑤 = 0
134 nfcv 2899 . . . . . 6 𝑥𝐶
135 nfcsb1v 3919 . . . . . 6 𝑥𝑤 / 𝑥𝑅
136133, 134, 135nfif 4562 . . . . 5 𝑥if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅)
137 eqeq1 2732 . . . . . 6 (𝑥 = 𝑤 → (𝑥 = 0 ↔ 𝑤 = 0))
138 csbeq1a 3908 . . . . . 6 (𝑥 = 𝑤𝑅 = 𝑤 / 𝑥𝑅)
139137, 138ifbieq2d 4558 . . . . 5 (𝑥 = 𝑤 → if(𝑥 = 0, 𝐶, 𝑅) = if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅))
140132, 136, 139cbvmpt 5263 . . . 4 (𝑥𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) = (𝑤𝐴 ↦ if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅))
141140eleq1i 2820 . . 3 ((𝑥𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑤𝐴 ↦ if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))
142131, 141bitr4di 288 . 2 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅)) ⇝𝑟 𝐶 ↔ (𝑥𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
14346, 66, 1423bitr2d 306 1 (𝜑 → ((𝑦𝐵𝑆) ⇝𝑟 𝐶 ↔ (𝑥𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845  w3a 1084   = wceq 1533  wcel 2098  wne 2937  wral 3058  csb 3894  cin 3948  wss 3949  ifcif 4532   class class class wbr 5152  cmpt 5235  dom cdm 5682  cres 5684  Rel wrel 5687   Fn wfn 6548  wf 6549  cfv 6553  (class class class)co 7426  cc 11144  cr 11145  0cc0 11146  1c1 11147  +∞cpnf 11283  *cxr 11285   < clt 11286  cle 11287   / cdiv 11909  +crp 13014  (,)cioo 13364  [,)cico 13366  𝑟 crli 15469  t crest 17409  TopOpenctopn 17410  fldccnfld 21286   CnP ccnp 23149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-er 8731  df-map 8853  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-sup 9473  df-inf 9474  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-ico 13370  df-fz 13525  df-seq 14007  df-exp 14067  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-rlim 15473  df-struct 17123  df-slot 17158  df-ndx 17170  df-base 17188  df-plusg 17253  df-mulr 17254  df-starv 17255  df-tset 17259  df-ple 17260  df-ds 17262  df-unif 17263  df-rest 17411  df-topn 17412  df-topgen 17432  df-psmet 21278  df-xmet 21279  df-met 21280  df-bl 21281  df-mopn 21282  df-cnfld 21287  df-top 22816  df-topon 22833  df-bases 22869  df-cnp 23152
This theorem is referenced by:  rlimcnp3  26919
  Copyright terms: Public domain W3C validator