Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ellimc3apf GIF version

Theorem ellimc3apf 12989
 Description: Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.)
Hypotheses
Ref Expression
ellimc3.f (𝜑𝐹:𝐴⟶ℂ)
ellimc3.a (𝜑𝐴 ⊆ ℂ)
ellimc3.b (𝜑𝐵 ∈ ℂ)
ellimc3.nf 𝑧𝐹
Assertion
Ref Expression
ellimc3apf (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
Distinct variable groups:   𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑥,𝐹,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑥,𝑦)   𝐹(𝑧)

Proof of Theorem ellimc3apf
Dummy variables 𝑓 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnex 7839 . . . . . . 7 ℂ ∈ V
21a1i 9 . . . . . 6 (𝜑 → ℂ ∈ V)
3 ellimc3.f . . . . . 6 (𝜑𝐹:𝐴⟶ℂ)
4 ellimc3.a . . . . . 6 (𝜑𝐴 ⊆ ℂ)
5 elpm2r 6604 . . . . . 6 (((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm ℂ))
62, 2, 3, 4, 5syl22anc 1221 . . . . 5 (𝜑𝐹 ∈ (ℂ ↑pm ℂ))
7 ellimc3.b . . . . 5 (𝜑𝐵 ∈ ℂ)
81rabex 4108 . . . . . 6 {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))} ∈ V
98a1i 9 . . . . 5 (𝜑 → {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))} ∈ V)
10 simpl 108 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝐵) → 𝑓 = 𝐹)
1110dmeqd 4785 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝐵) → dom 𝑓 = dom 𝐹)
1210, 11feq12d 5306 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑓:dom 𝑓⟶ℂ ↔ 𝐹:dom 𝐹⟶ℂ))
1311sseq1d 3157 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝐵) → (dom 𝑓 ⊆ ℂ ↔ dom 𝐹 ⊆ ℂ))
1412, 13anbi12d 465 . . . . . . . 8 ((𝑓 = 𝐹𝑤 = 𝐵) → ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ)))
15 simpr 109 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝐵) → 𝑤 = 𝐵)
1615eleq1d 2226 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑤 ∈ ℂ ↔ 𝐵 ∈ ℂ))
17 nfcv 2299 . . . . . . . . . . . . . 14 𝑧dom 𝑓
18 ellimc3.nf . . . . . . . . . . . . . . 15 𝑧𝐹
1918nfdm 4827 . . . . . . . . . . . . . 14 𝑧dom 𝐹
2017, 19raleqf 2648 . . . . . . . . . . . . 13 (dom 𝑓 = dom 𝐹 → (∀𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)))
2111, 20syl 14 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑤 = 𝐵) → (∀𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)))
2218nfeq2 2311 . . . . . . . . . . . . . 14 𝑧 𝑓 = 𝐹
23 nfv 1508 . . . . . . . . . . . . . 14 𝑧 𝑤 = 𝐵
2422, 23nfan 1545 . . . . . . . . . . . . 13 𝑧(𝑓 = 𝐹𝑤 = 𝐵)
2515breq2d 3977 . . . . . . . . . . . . . . 15 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑧 # 𝑤𝑧 # 𝐵))
2615oveq2d 5834 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑧𝑤) = (𝑧𝐵))
2726fveq2d 5469 . . . . . . . . . . . . . . . 16 ((𝑓 = 𝐹𝑤 = 𝐵) → (abs‘(𝑧𝑤)) = (abs‘(𝑧𝐵)))
2827breq1d 3975 . . . . . . . . . . . . . . 15 ((𝑓 = 𝐹𝑤 = 𝐵) → ((abs‘(𝑧𝑤)) < 𝑦 ↔ (abs‘(𝑧𝐵)) < 𝑦))
2925, 28anbi12d 465 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑤 = 𝐵) → ((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) ↔ (𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦)))
3010fveq1d 5467 . . . . . . . . . . . . . . . 16 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑓𝑧) = (𝐹𝑧))
3130fvoveq1d 5840 . . . . . . . . . . . . . . 15 ((𝑓 = 𝐹𝑤 = 𝐵) → (abs‘((𝑓𝑧) − 𝑢)) = (abs‘((𝐹𝑧) − 𝑢)))
3231breq1d 3975 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑤 = 𝐵) → ((abs‘((𝑓𝑧) − 𝑢)) < 𝑥 ↔ (abs‘((𝐹𝑧) − 𝑢)) < 𝑥))
3329, 32imbi12d 233 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑤 = 𝐵) → (((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3424, 33ralbid 2455 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑤 = 𝐵) → (∀𝑧 ∈ dom 𝐹((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3521, 34bitrd 187 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑤 = 𝐵) → (∀𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3635rexbidv 2458 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝐵) → (∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3736ralbidv 2457 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝐵) → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3816, 37anbi12d 465 . . . . . . . 8 ((𝑓 = 𝐹𝑤 = 𝐵) → ((𝑤 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)) ↔ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥))))
3914, 38anbi12d 465 . . . . . . 7 ((𝑓 = 𝐹𝑤 = 𝐵) → (((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑤 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥))) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))))
4039rabbidv 2701 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝐵) → {𝑢 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑤 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)))} = {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))})
41 df-limced 12985 . . . . . 6 lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑤 ∈ ℂ ↦ {𝑢 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑤 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)))})
4240, 41ovmpoga 5944 . . . . 5 ((𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝐵 ∈ ℂ ∧ {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))} ∈ V) → (𝐹 lim 𝐵) = {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))})
436, 7, 9, 42syl3anc 1220 . . . 4 (𝜑 → (𝐹 lim 𝐵) = {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))})
4443eleq2d 2227 . . 3 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ 𝐶 ∈ {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))}))
45 oveq2 5826 . . . . . . . . . . . 12 (𝑢 = 𝐶 → ((𝐹𝑧) − 𝑢) = ((𝐹𝑧) − 𝐶))
4645fveq2d 5469 . . . . . . . . . . 11 (𝑢 = 𝐶 → (abs‘((𝐹𝑧) − 𝑢)) = (abs‘((𝐹𝑧) − 𝐶)))
4746breq1d 3975 . . . . . . . . . 10 (𝑢 = 𝐶 → ((abs‘((𝐹𝑧) − 𝑢)) < 𝑥 ↔ (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))
4847imbi2d 229 . . . . . . . . 9 (𝑢 = 𝐶 → (((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥) ↔ ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
4948ralbidv 2457 . . . . . . . 8 (𝑢 = 𝐶 → (∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
5049rexbidv 2458 . . . . . . 7 (𝑢 = 𝐶 → (∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥) ↔ ∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
5150ralbidv 2457 . . . . . 6 (𝑢 = 𝐶 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
5251anbi2d 460 . . . . 5 (𝑢 = 𝐶 → ((𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)) ↔ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
5352anbi2d 460 . . . 4 (𝑢 = 𝐶 → (((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥))) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
5453elrab 2868 . . 3 (𝐶 ∈ {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))} ↔ (𝐶 ∈ ℂ ∧ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
5544, 54bitrdi 195 . 2 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))))
567biantrurd 303 . . . 4 (𝜑 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
573fdmd 5323 . . . . . . 7 (𝜑 → dom 𝐹 = 𝐴)
5857feq2d 5304 . . . . . 6 (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:𝐴⟶ℂ))
593, 58mpbird 166 . . . . 5 (𝜑𝐹:dom 𝐹⟶ℂ)
6057, 4eqsstrd 3164 . . . . 5 (𝜑 → dom 𝐹 ⊆ ℂ)
61 ibar 299 . . . . 5 ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) → ((𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
6259, 60, 61syl2anc 409 . . . 4 (𝜑 → ((𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
6356, 62bitrd 187 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
6463anbi2d 460 . 2 (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ (𝐶 ∈ ℂ ∧ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))))
65 nfcv 2299 . . . . . . 7 𝑧𝐴
6619, 65raleqf 2648 . . . . . 6 (dom 𝐹 = 𝐴 → (∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
6757, 66syl 14 . . . . 5 (𝜑 → (∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
6867rexbidv 2458 . . . 4 (𝜑 → (∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
6968ralbidv 2457 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
7069anbi2d 460 . 2 (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
7155, 64, 703bitr2d 215 1 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1335   ∈ wcel 2128  Ⅎwnfc 2286  ∀wral 2435  ∃wrex 2436  {crab 2439  Vcvv 2712   ⊆ wss 3102   class class class wbr 3965  dom cdm 4583  ⟶wf 5163  ‘cfv 5167  (class class class)co 5818   ↑pm cpm 6587  ℂcc 7713   < clt 7895   − cmin 8029   # cap 8439  ℝ+crp 9542  abscabs 10879   limℂ climc 12983 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-cnex 7806 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-id 4252  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-pm 6589  df-limced 12985 This theorem is referenced by:  ellimc3ap  12990  limcmpted  12992
 Copyright terms: Public domain W3C validator