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

Theorem rlimcnp2 24914
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 3981 . . . . . . . 8 (𝐵 ∩ (1[,)+∞)) ⊆ 𝐵
2 resmpt 5590 . . . . . . . 8 ((𝐵 ∩ (1[,)+∞)) ⊆ 𝐵 → ((𝑦𝐵𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
31, 2mp1i 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 < 𝑤))
96, 7, 8ixxss1 12398 . . . . . . . . . . 11 ((0 ∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆ (0(,)+∞))
104, 5, 9mp2an 672 . . . . . . . . . 10 (1[,)+∞) ⊆ (0(,)+∞)
11 ioorp 12456 . . . . . . . . . 10 (0(,)+∞) = ℝ+
1210, 11sseqtri 3786 . . . . . . . . 9 (1[,)+∞) ⊆ ℝ+
13 sslin 3987 . . . . . . . . 9 ((1[,)+∞) ⊆ ℝ+ → (𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩ ℝ+))
1412, 13ax-mp 5 . . . . . . . 8 (𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩ ℝ+)
15 resmpt 5590 . . . . . . . 8 ((𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩ ℝ+) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
1614, 15mp1i 13 . . . . . . 7 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
173, 16eqtr4d 2808 . . . . . 6 (𝜑 → ((𝑦𝐵𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))))
18 resres 5550 . . . . . 6 (((𝑦𝐵𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦𝐵𝑆) ↾ (𝐵 ∩ (1[,)+∞)))
19 resres 5550 . . . . . 6 (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞)))
2017, 18, 193eqtr4g 2830 . . . . 5 (𝜑 → (((𝑦𝐵𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)))
21 rlimcnp2.r . . . . . . . . 9 ((𝜑𝑦𝐵) → 𝑆 ∈ ℂ)
22 eqid 2771 . . . . . . . . 9 (𝑦𝐵𝑆) = (𝑦𝐵𝑆)
2321, 22fmptd 6527 . . . . . . . 8 (𝜑 → (𝑦𝐵𝑆):𝐵⟶ℂ)
24 ffn 6185 . . . . . . . 8 ((𝑦𝐵𝑆):𝐵⟶ℂ → (𝑦𝐵𝑆) Fn 𝐵)
2523, 24syl 17 . . . . . . 7 (𝜑 → (𝑦𝐵𝑆) Fn 𝐵)
26 fnresdm 6140 . . . . . . 7 ((𝑦𝐵𝑆) Fn 𝐵 → ((𝑦𝐵𝑆) ↾ 𝐵) = (𝑦𝐵𝑆))
2725, 26syl 17 . . . . . 6 (𝜑 → ((𝑦𝐵𝑆) ↾ 𝐵) = (𝑦𝐵𝑆))
2827reseq1d 5533 . . . . 5 (𝜑 → (((𝑦𝐵𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦𝐵𝑆) ↾ (1[,)+∞)))
29 inss1 3981 . . . . . . . . . . 11 (𝐵 ∩ ℝ+) ⊆ 𝐵
3029sseli 3748 . . . . . . . . . 10 (𝑦 ∈ (𝐵 ∩ ℝ+) → 𝑦𝐵)
3130, 21sylan2 580 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑆 ∈ ℂ)
32 eqid 2771 . . . . . . . . 9 (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆)
3331, 32fmptd 6527 . . . . . . . 8 (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩ ℝ+)⟶ℂ)
34 frel 6190 . . . . . . . 8 ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆):(𝐵 ∩ ℝ+)⟶ℂ → Rel (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
3533, 34syl 17 . . . . . . 7 (𝜑 → Rel (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
3632, 31dmmptd 6164 . . . . . . . 8 (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) = (𝐵 ∩ ℝ+))
3736, 29syl6eqss 3804 . . . . . . 7 (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵)
38 relssres 5578 . . . . . . 7 ((Rel (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ∧ dom (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⊆ 𝐵) → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
3935, 37, 38syl2anc 573 . . . . . 6 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
4039reseq1d 5533 . . . . 5 (𝜑 → (((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞)))
4120, 28, 403eqtr3d 2813 . . . 4 (𝜑 → ((𝑦𝐵𝑆) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞)))
4241breq1d 4796 . . 3 (𝜑 → (((𝑦𝐵𝑆) ↾ (1[,)+∞)) ⇝𝑟 𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞)) ⇝𝑟 𝐶))
43 rlimcnp2.b . . . 4 (𝜑𝐵 ⊆ ℝ)
44 1red 10257 . . . 4 (𝜑 → 1 ∈ ℝ)
4523, 43, 44rlimresb 14504 . . 3 (𝜑 → ((𝑦𝐵𝑆) ⇝𝑟 𝐶 ↔ ((𝑦𝐵𝑆) ↾ (1[,)+∞)) ⇝𝑟 𝐶))
4629, 43syl5ss 3763 . . . 4 (𝜑 → (𝐵 ∩ ℝ+) ⊆ ℝ)
4733, 46, 44rlimresb 14504 . . 3 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟 𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ↾ (1[,)+∞)) ⇝𝑟 𝐶))
4842, 45, 473bitr4d 300 . 2 (𝜑 → ((𝑦𝐵𝑆) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟 𝐶))
49 inss2 3982 . . . . . . . . . . 11 (𝐵 ∩ ℝ+) ⊆ ℝ+
5049a1i 11 . . . . . . . . . 10 (𝜑 → (𝐵 ∩ ℝ+) ⊆ ℝ+)
5150sselda 3752 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → 𝑦 ∈ ℝ+)
5251rpreccld 12085 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / 𝑦) ∈ ℝ+)
5352rpne0d 12080 . . . . . . 7 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / 𝑦) ≠ 0)
5453neneqd 2948 . . . . . 6 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → ¬ (1 / 𝑦) = 0)
5554iffalsed 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 / 𝑦)) = 𝑦)
5951, 57, 583syl 18 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / (1 / 𝑦)) = 𝑦)
6056, 59sylan9eqr 2827 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → (1 / 𝑥) = 𝑦)
6160eqcomd 2777 . . . . . . . 8 (((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑦 = (1 / 𝑥))
62 rlimcnp2.s . . . . . . . 8 (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅)
6361, 62syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑆 = 𝑅)
6463eqcomd 2777 . . . . . 6 (((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) ∧ 𝑥 = (1 / 𝑦)) → 𝑅 = 𝑆)
6552, 64csbied 3709 . . . . 5 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / 𝑦) / 𝑥𝑅 = 𝑆)
6655, 65eqtrd 2805 . . . 4 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅) = 𝑆)
6766mpteq2dva 4878 . . 3 (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅)) = (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆))
6867breq1d 4796 . 2 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅)) ⇝𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ+) ↦ 𝑆) ⇝𝑟 𝐶))
69 rlimcnp2.a . . . 4 (𝜑𝐴 ⊆ (0[,)+∞))
70 rlimcnp2.0 . . . 4 (𝜑 → 0 ∈ 𝐴)
71 rlimcnp2.c . . . . . 6 (𝜑𝐶 ∈ ℂ)
7271ad2antrr 705 . . . . 5 (((𝜑𝑤𝐴) ∧ 𝑤 = 0) → 𝐶 ∈ ℂ)
7369sselda 3752 . . . . . . . . . . . 12 ((𝜑𝑤𝐴) → 𝑤 ∈ (0[,)+∞))
74 0re 10242 . . . . . . . . . . . . 13 0 ∈ ℝ
75 pnfxr 10294 . . . . . . . . . . . . 13 +∞ ∈ ℝ*
76 elico2 12442 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑤 ∈ (0[,)+∞) ↔ (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤𝑤 < +∞)))
7774, 75, 76mp2an 672 . . . . . . . . . . . 12 (𝑤 ∈ (0[,)+∞) ↔ (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤𝑤 < +∞))
7873, 77sylib 208 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤𝑤 < +∞))
7978simp1d 1136 . . . . . . . . . 10 ((𝜑𝑤𝐴) → 𝑤 ∈ ℝ)
8079adantr 466 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ)
8178simp2d 1137 . . . . . . . . . . . . . 14 ((𝜑𝑤𝐴) → 0 ≤ 𝑤)
82 leloe 10326 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝑤 ∈ ℝ) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤)))
8374, 79, 82sylancr 575 . . . . . . . . . . . . . 14 ((𝜑𝑤𝐴) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤)))
8481, 83mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑤𝐴) → (0 < 𝑤 ∨ 0 = 𝑤))
8584ord 853 . . . . . . . . . . . 12 ((𝜑𝑤𝐴) → (¬ 0 < 𝑤 → 0 = 𝑤))
86 eqcom 2778 . . . . . . . . . . . 12 (0 = 𝑤𝑤 = 0)
8785, 86syl6ib 241 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (¬ 0 < 𝑤𝑤 = 0))
8887con1d 141 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (¬ 𝑤 = 0 → 0 < 𝑤))
8988imp 393 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 0 < 𝑤)
9080, 89elrpd 12072 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ+)
91 rpcnne0 12053 . . . . . . . . 9 (𝑤 ∈ ℝ+ → (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0))
92 recrec 10924 . . . . . . . . 9 ((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) → (1 / (1 / 𝑤)) = 𝑤)
9391, 92syl 17 . . . . . . . 8 (𝑤 ∈ ℝ+ → (1 / (1 / 𝑤)) = 𝑤)
9490, 93syl 17 . . . . . . 7 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) = 𝑤)
9594csbeq1d 3689 . . . . . 6 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) / 𝑥𝑅 = 𝑤 / 𝑥𝑅)
96 oveq2 6801 . . . . . . . . 9 (𝑦 = (1 / 𝑤) → (1 / 𝑦) = (1 / (1 / 𝑤)))
9796csbeq1d 3689 . . . . . . . 8 (𝑦 = (1 / 𝑤) → (1 / 𝑦) / 𝑥𝑅 = (1 / (1 / 𝑤)) / 𝑥𝑅)
9897eleq1d 2835 . . . . . . 7 (𝑦 = (1 / 𝑤) → ((1 / 𝑦) / 𝑥𝑅 ∈ ℂ ↔ (1 / (1 / 𝑤)) / 𝑥𝑅 ∈ ℂ))
9965, 31eqeltrd 2850 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐵 ∩ ℝ+)) → (1 / 𝑦) / 𝑥𝑅 ∈ ℂ)
10099ralrimiva 3115 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (𝐵 ∩ ℝ+)(1 / 𝑦) / 𝑥𝑅 ∈ ℂ)
101100ad2antrr 705 . . . . . . 7 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → ∀𝑦 ∈ (𝐵 ∩ ℝ+)(1 / 𝑦) / 𝑥𝑅 ∈ ℂ)
102 simplr 752 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝑤𝐴)
103 simpll 750 . . . . . . . . . 10 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝜑)
104 eleq1 2838 . . . . . . . . . . . . 13 (𝑦 = (1 / 𝑤) → (𝑦𝐵 ↔ (1 / 𝑤) ∈ 𝐵))
10596eleq1d 2835 . . . . . . . . . . . . 13 (𝑦 = (1 / 𝑤) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))
106104, 105bibi12d 334 . . . . . . . . . . . 12 (𝑦 = (1 / 𝑤) → ((𝑦𝐵 ↔ (1 / 𝑦) ∈ 𝐴) ↔ ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴)))
107 rlimcnp2.d . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ+) → (𝑦𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
108107ralrimiva 3115 . . . . . . . . . . . . 13 (𝜑 → ∀𝑦 ∈ ℝ+ (𝑦𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
109108adantr 466 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → ∀𝑦 ∈ ℝ+ (𝑦𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
110 rpreccl 12060 . . . . . . . . . . . . 13 (𝑤 ∈ ℝ+ → (1 / 𝑤) ∈ ℝ+)
111110adantl 467 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → (1 / 𝑤) ∈ ℝ+)
112106, 109, 111rspcdva 3466 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+) → ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))
11393adantl 467 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → (1 / (1 / 𝑤)) = 𝑤)
114113eleq1d 2835 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+) → ((1 / (1 / 𝑤)) ∈ 𝐴𝑤𝐴))
115112, 114bitr2d 269 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+) → (𝑤𝐴 ↔ (1 / 𝑤) ∈ 𝐵))
116103, 90, 115syl2anc 573 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (𝑤𝐴 ↔ (1 / 𝑤) ∈ 𝐵))
117102, 116mpbid 222 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ 𝐵)
11890rpreccld 12085 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ ℝ+)
119117, 118elind 3949 . . . . . . 7 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ (𝐵 ∩ ℝ+))
12098, 101, 119rspcdva 3466 . . . . . 6 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) / 𝑥𝑅 ∈ ℂ)
12195, 120eqeltrrd 2851 . . . . 5 (((𝜑𝑤𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 / 𝑥𝑅 ∈ ℂ)
12272, 121ifclda 4259 . . . 4 ((𝜑𝑤𝐴) → if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅) ∈ ℂ)
123111biantrud 521 . . . . . 6 ((𝜑𝑤 ∈ ℝ+) → ((1 / 𝑤) ∈ 𝐵 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈ ℝ+)))
124115, 123bitrd 268 . . . . 5 ((𝜑𝑤 ∈ ℝ+) → (𝑤𝐴 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈ ℝ+)))
125 elin 3947 . . . . 5 ((1 / 𝑤) ∈ (𝐵 ∩ ℝ+) ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈ ℝ+))
126124, 125syl6bbr 278 . . . 4 ((𝜑𝑤 ∈ ℝ+) → (𝑤𝐴 ↔ (1 / 𝑤) ∈ (𝐵 ∩ ℝ+)))
127 iftrue 4231 . . . 4 (𝑤 = 0 → if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅) = 𝐶)
128 eqeq1 2775 . . . . 5 (𝑤 = (1 / 𝑦) → (𝑤 = 0 ↔ (1 / 𝑦) = 0))
129 csbeq1 3685 . . . . 5 (𝑤 = (1 / 𝑦) → 𝑤 / 𝑥𝑅 = (1 / 𝑦) / 𝑥𝑅)
130128, 129ifbieq2d 4250 . . . 4 (𝑤 = (1 / 𝑦) → if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅) = if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅))
131 rlimcnp2.j . . . 4 𝐽 = (TopOpen‘ℂfld)
132 rlimcnp2.k . . . 4 𝐾 = (𝐽t 𝐴)
13369, 70, 50, 122, 126, 127, 130, 131, 132rlimcnp 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 𝑥𝑤 / 𝑥𝑅
138135, 136, 137nfif 4254 . . . . 5 𝑥if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅)
139 eqeq1 2775 . . . . . 6 (𝑥 = 𝑤 → (𝑥 = 0 ↔ 𝑤 = 0))
140 csbeq1a 3691 . . . . . 6 (𝑥 = 𝑤𝑅 = 𝑤 / 𝑥𝑅)
141139, 140ifbieq2d 4250 . . . . 5 (𝑥 = 𝑤 → if(𝑥 = 0, 𝐶, 𝑅) = if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅))
142134, 138, 141cbvmpt 4883 . . . 4 (𝑥𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) = (𝑤𝐴 ↦ if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅))
143142eleq1i 2841 . . 3 ((𝑥𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑤𝐴 ↦ if(𝑤 = 0, 𝐶, 𝑤 / 𝑥𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))
144133, 143syl6bbr 278 . 2 (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ+) ↦ if((1 / 𝑦) = 0, 𝐶, (1 / 𝑦) / 𝑥𝑅)) ⇝𝑟 𝐶 ↔ (𝑥𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
14548, 68, 1443bitr2d 296 1 (𝜑 → ((𝑦𝐵𝑆) ⇝𝑟 𝐶 ↔ (𝑥𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 836  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  csb 3682  cin 3722  wss 3723  ifcif 4225   class class class wbr 4786  cmpt 4863  dom cdm 5249  cres 5251  Rel wrel 5254   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  cc 10136  cr 10137  0cc0 10138  1c1 10139  +∞cpnf 10273  *cxr 10275   < clt 10276  cle 10277   / cdiv 10886  +crp 12035  (,)cioo 12380  [,)cico 12382  𝑟 crli 14424  t crest 16289  TopOpenctopn 16290  fldccnfld 19961   CnP ccnp 21250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ico 12386  df-fz 12534  df-seq 13009  df-exp 13068  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-rlim 14428  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-plusg 16162  df-mulr 16163  df-starv 16164  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-rest 16291  df-topn 16292  df-topgen 16312  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-cnfld 19962  df-top 20919  df-topon 20936  df-bases 20971  df-cnp 21253
This theorem is referenced by:  rlimcnp3  24915
  Copyright terms: Public domain W3C validator