ellimc3ap - Intuitionistic Logic Explorer

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

Theorem ellimc3ap 14840

Description: Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) Use apartness. (Revised by Jim Kingdon, 3-Jun-2023.)

**Hypotheses**
Ref	Expression
ellimc3.f	⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
ellimc3.a	⊢ (𝜑 → 𝐴 ⊆ ℂ)
ellimc3.b	⊢ (𝜑 → 𝐵 ∈ ℂ)

**Assertion**
Ref	Expression
ellimc3ap	⊢ (𝜑 → (𝐶 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))

Distinct variable groups: 𝑧,𝐴 𝑥,𝐵,𝑦,𝑧 𝑥,𝐶,𝑦,𝑧 𝑥,𝐹,𝑦 𝜑,𝑥,𝑦 𝑧,𝐹 Allowed substitution hints: 𝜑(𝑧) 𝐴(𝑥,𝑦)

**Proof of Theorem ellimc3ap**
Step	Hyp	Ref	Expression
1		ellimc3.f	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
2		ellimc3.a	. 2 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
3		ellimc3.b	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4		nfcv 2336	. 2 ⊢ Ⅎ𝑧𝐹
5	1, 2, 3, 4	ellimc3apf 14839	1 ⊢ (𝜑 → (𝐶 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∈ wcel 2164 ∀wral 2472 ∃wrex 2473 ⊆ wss 3154 class class class wbr 4030 ⟶wf 5251 ‘cfv 5255 (class class class)co 5919 ℂcc 7872 < clt 8056 − cmin 8192 # cap 8602 ℝ⁺crp 9722 abscabs 11144 lim_ℂ climc 14833

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4148 ax-pow 4204 ax-pr 4239 ax-un 4465 ax-setind 4570 ax-cnex 7965

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-ral 2477 df-rex 2478 df-rab 2481 df-v 2762 df-sbc 2987 df-dif 3156 df-un 3158 df-in 3160 df-ss 3167 df-pw 3604 df-sn 3625 df-pr 3626 df-op 3628 df-uni 3837 df-br 4031 df-opab 4092 df-id 4325 df-xp 4666 df-rel 4667 df-cnv 4668 df-co 4669 df-dm 4670 df-rn 4671 df-iota 5216 df-fun 5257 df-fn 5258 df-f 5259 df-fv 5263 df-ov 5922 df-oprab 5923 df-mpo 5924 df-pm 6707 df-limced 14835

This theorem is referenced by: limcdifap 14841 limcimolemlt 14843 limcimo 14844 limcresi 14845 cnplimcim 14846 cnplimclemr 14848 limccnpcntop 14854 dveflem 14905

W3C validator