Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  addlimc Structured version   Visualization version   GIF version

Theorem addlimc 40395
Description: Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
addlimc.f 𝐹 = (𝑥𝐴𝐵)
addlimc.g 𝐺 = (𝑥𝐴𝐶)
addlimc.h 𝐻 = (𝑥𝐴 ↦ (𝐵 + 𝐶))
addlimc.b ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
addlimc.c ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
addlimc.e (𝜑𝐸 ∈ (𝐹 lim 𝐷))
addlimc.i (𝜑𝐼 ∈ (𝐺 lim 𝐷))
Assertion
Ref Expression
addlimc (𝜑 → (𝐸 + 𝐼) ∈ (𝐻 lim 𝐷))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)   𝐸(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝐻(𝑥)   𝐼(𝑥)

Proof of Theorem addlimc
Dummy variables 𝑎 𝑏 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 23858 . . . 4 (𝐹 lim 𝐷) ⊆ ℂ
2 addlimc.e . . . 4 (𝜑𝐸 ∈ (𝐹 lim 𝐷))
31, 2sseldi 3750 . . 3 (𝜑𝐸 ∈ ℂ)
4 limccl 23858 . . . 4 (𝐺 lim 𝐷) ⊆ ℂ
5 addlimc.i . . . 4 (𝜑𝐼 ∈ (𝐺 lim 𝐷))
64, 5sseldi 3750 . . 3 (𝜑𝐼 ∈ ℂ)
73, 6addcld 10264 . 2 (𝜑 → (𝐸 + 𝐼) ∈ ℂ)
8 addlimc.b . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
9 addlimc.f . . . . . . . . . 10 𝐹 = (𝑥𝐴𝐵)
108, 9fmptd 6529 . . . . . . . . 9 (𝜑𝐹:𝐴⟶ℂ)
119, 8, 2limcmptdm 40382 . . . . . . . . 9 (𝜑𝐴 ⊆ ℂ)
12 limcrcl 23857 . . . . . . . . . . 11 (𝐸 ∈ (𝐹 lim 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
132, 12syl 17 . . . . . . . . . 10 (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
1413simp3d 1138 . . . . . . . . 9 (𝜑𝐷 ∈ ℂ)
1510, 11, 14ellimc3 23862 . . . . . . . 8 (𝜑 → (𝐸 ∈ (𝐹 lim 𝐷) ↔ (𝐸 ∈ ℂ ∧ ∀𝑧 ∈ ℝ+𝑎 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < 𝑧))))
162, 15mpbid 222 . . . . . . 7 (𝜑 → (𝐸 ∈ ℂ ∧ ∀𝑧 ∈ ℝ+𝑎 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < 𝑧)))
1716simprd 483 . . . . . 6 (𝜑 → ∀𝑧 ∈ ℝ+𝑎 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < 𝑧))
18 rphalfcl 12060 . . . . . 6 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
19 breq2 4791 . . . . . . . . 9 (𝑧 = (𝑦 / 2) → ((abs‘((𝐹𝑣) − 𝐸)) < 𝑧 ↔ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)))
2019imbi2d 329 . . . . . . . 8 (𝑧 = (𝑦 / 2) → (((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < 𝑧) ↔ ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2))))
2120rexralbidv 3206 . . . . . . 7 (𝑧 = (𝑦 / 2) → (∃𝑎 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < 𝑧) ↔ ∃𝑎 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2))))
2221rspccva 3459 . . . . . 6 ((∀𝑧 ∈ ℝ+𝑎 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < 𝑧) ∧ (𝑦 / 2) ∈ ℝ+) → ∃𝑎 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)))
2317, 18, 22syl2an 583 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → ∃𝑎 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)))
24 addlimc.c . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
25 addlimc.g . . . . . . . . . 10 𝐺 = (𝑥𝐴𝐶)
2624, 25fmptd 6529 . . . . . . . . 9 (𝜑𝐺:𝐴⟶ℂ)
2726, 11, 14ellimc3 23862 . . . . . . . 8 (𝜑 → (𝐼 ∈ (𝐺 lim 𝐷) ↔ (𝐼 ∈ ℂ ∧ ∀𝑧 ∈ ℝ+𝑏 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < 𝑧))))
285, 27mpbid 222 . . . . . . 7 (𝜑 → (𝐼 ∈ ℂ ∧ ∀𝑧 ∈ ℝ+𝑏 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < 𝑧)))
2928simprd 483 . . . . . 6 (𝜑 → ∀𝑧 ∈ ℝ+𝑏 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < 𝑧))
30 breq2 4791 . . . . . . . . 9 (𝑧 = (𝑦 / 2) → ((abs‘((𝐺𝑣) − 𝐼)) < 𝑧 ↔ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))
3130imbi2d 329 . . . . . . . 8 (𝑧 = (𝑦 / 2) → (((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < 𝑧) ↔ ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))))
3231rexralbidv 3206 . . . . . . 7 (𝑧 = (𝑦 / 2) → (∃𝑏 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < 𝑧) ↔ ∃𝑏 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))))
3332rspccva 3459 . . . . . 6 ((∀𝑧 ∈ ℝ+𝑏 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < 𝑧) ∧ (𝑦 / 2) ∈ ℝ+) → ∃𝑏 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))
3429, 18, 33syl2an 583 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → ∃𝑏 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))
35 reeanv 3255 . . . . 5 (∃𝑎 ∈ ℝ+𝑏 ∈ ℝ+ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))) ↔ (∃𝑎 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∃𝑏 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))))
3623, 34, 35sylanbrc 572 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ∃𝑎 ∈ ℝ+𝑏 ∈ ℝ+ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))))
37 ifcl 4270 . . . . . . . 8 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → if(𝑎𝑏, 𝑎, 𝑏) ∈ ℝ+)
38373ad2ant2 1128 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → if(𝑎𝑏, 𝑎, 𝑏) ∈ ℝ+)
39 nfv 1995 . . . . . . . . 9 𝑣(𝜑𝑦 ∈ ℝ+)
40 nfv 1995 . . . . . . . . 9 𝑣(𝑎 ∈ ℝ+𝑏 ∈ ℝ+)
41 nfra1 3090 . . . . . . . . . 10 𝑣𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2))
42 nfra1 3090 . . . . . . . . . 10 𝑣𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))
4341, 42nfan 1980 . . . . . . . . 9 𝑣(∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))
4439, 40, 43nf3an 1983 . . . . . . . 8 𝑣((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))))
45 simp11l 1368 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → 𝜑)
46 simp2 1131 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → 𝑣𝐴)
4745, 46jca 501 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (𝜑𝑣𝐴))
48 rpre 12041 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
4948adantl 467 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
50493ad2ant1 1127 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → 𝑦 ∈ ℝ)
51503ad2ant1 1127 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → 𝑦 ∈ ℝ)
52 simp13l 1372 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)))
53 simp3l 1243 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → 𝑣𝐷)
5411sselda 3752 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → 𝑣 ∈ ℂ)
5545, 46, 54syl2anc 573 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → 𝑣 ∈ ℂ)
5645, 14syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → 𝐷 ∈ ℂ)
5755, 56subcld 10597 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (𝑣𝐷) ∈ ℂ)
5857abscld 14382 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (abs‘(𝑣𝐷)) ∈ ℝ)
5938rpred 12074 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → if(𝑎𝑏, 𝑎, 𝑏) ∈ ℝ)
60593ad2ant1 1127 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → if(𝑎𝑏, 𝑎, 𝑏) ∈ ℝ)
61 simpl 468 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ ℝ+)
6261rpred 12074 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ ℝ)
63623ad2ant2 1128 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → 𝑎 ∈ ℝ)
64633ad2ant1 1127 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → 𝑎 ∈ ℝ)
65 simp3r 1244 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))
66 simpr 471 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ ℝ+)
6766rpred 12074 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ ℝ)
68 min1 12224 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎𝑏, 𝑎, 𝑏) ≤ 𝑎)
6962, 67, 68syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → if(𝑎𝑏, 𝑎, 𝑏) ≤ 𝑎)
70693ad2ant2 1128 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → if(𝑎𝑏, 𝑎, 𝑏) ≤ 𝑎)
71703ad2ant1 1127 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → if(𝑎𝑏, 𝑎, 𝑏) ≤ 𝑎)
7258, 60, 64, 65, 71ltletrd 10402 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (abs‘(𝑣𝐷)) < 𝑎)
7353, 72jca 501 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎))
74 rsp 3078 . . . . . . . . . . . 12 (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) → (𝑣𝐴 → ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2))))
7552, 46, 73, 74syl3c 66 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2))
7647, 51, 75jca31 504 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)))
77 simp13r 1373 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))
78673ad2ant2 1128 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → 𝑏 ∈ ℝ)
79783ad2ant1 1127 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → 𝑏 ∈ ℝ)
80 min2 12225 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎𝑏, 𝑎, 𝑏) ≤ 𝑏)
8162, 67, 80syl2anc 573 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → if(𝑎𝑏, 𝑎, 𝑏) ≤ 𝑏)
82813ad2ant2 1128 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → if(𝑎𝑏, 𝑎, 𝑏) ≤ 𝑏)
83823ad2ant1 1127 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → if(𝑎𝑏, 𝑎, 𝑏) ≤ 𝑏)
8458, 60, 79, 65, 83ltletrd 10402 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (abs‘(𝑣𝐷)) < 𝑏)
8553, 84jca 501 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏))
86 rsp 3078 . . . . . . . . . . 11 (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (𝑣𝐴 → ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))))
8777, 46, 85, 86syl3c 66 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))
888, 24addcld 10264 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐵 + 𝐶) ∈ ℂ)
89 addlimc.h . . . . . . . . . . . . . . . 16 𝐻 = (𝑥𝐴 ↦ (𝐵 + 𝐶))
9088, 89fmptd 6529 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝐴⟶ℂ)
9190ffvelrnda 6504 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → (𝐻𝑣) ∈ ℂ)
9291ad3antrrr 709 . . . . . . . . . . . . 13 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (𝐻𝑣) ∈ ℂ)
93 simp-4l 768 . . . . . . . . . . . . . 14 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → 𝜑)
9493, 7syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (𝐸 + 𝐼) ∈ ℂ)
9592, 94subcld 10597 . . . . . . . . . . . 12 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → ((𝐻𝑣) − (𝐸 + 𝐼)) ∈ ℂ)
9695abscld 14382 . . . . . . . . . . 11 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) ∈ ℝ)
9710ffvelrnda 6504 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
9897ad3antrrr 709 . . . . . . . . . . . . . 14 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (𝐹𝑣) ∈ ℂ)
9993, 3syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → 𝐸 ∈ ℂ)
10098, 99subcld 10597 . . . . . . . . . . . . 13 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → ((𝐹𝑣) − 𝐸) ∈ ℂ)
101100abscld 14382 . . . . . . . . . . . 12 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (abs‘((𝐹𝑣) − 𝐸)) ∈ ℝ)
10226ffvelrnda 6504 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐺𝑣) ∈ ℂ)
103102ad3antrrr 709 . . . . . . . . . . . . . 14 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (𝐺𝑣) ∈ ℂ)
10493, 6syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → 𝐼 ∈ ℂ)
105103, 104subcld 10597 . . . . . . . . . . . . 13 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → ((𝐺𝑣) − 𝐼) ∈ ℂ)
106105abscld 14382 . . . . . . . . . . . 12 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (abs‘((𝐺𝑣) − 𝐼)) ∈ ℝ)
107101, 106readdcld 10274 . . . . . . . . . . 11 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → ((abs‘((𝐹𝑣) − 𝐸)) + (abs‘((𝐺𝑣) − 𝐼))) ∈ ℝ)
108 simpllr 760 . . . . . . . . . . 11 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → 𝑦 ∈ ℝ)
109 nfv 1995 . . . . . . . . . . . . . . . . . 18 𝑥(𝜑𝑣𝐴)
110 nfmpt1 4882 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑥𝐴 ↦ (𝐵 + 𝐶))
11189, 110nfcxfr 2911 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐻
112 nfcv 2913 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑣
113111, 112nffv 6341 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐻𝑣)
114 nfmpt1 4882 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
1159, 114nfcxfr 2911 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
116115, 112nffv 6341 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝐹𝑣)
117 nfcv 2913 . . . . . . . . . . . . . . . . . . . 20 𝑥 +
118 nfmpt1 4882 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐶)
11925, 118nfcxfr 2911 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐺
120119, 112nffv 6341 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝐺𝑣)
121116, 117, 120nfov 6824 . . . . . . . . . . . . . . . . . . 19 𝑥((𝐹𝑣) + (𝐺𝑣))
122113, 121nfeq 2925 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑣) = ((𝐹𝑣) + (𝐺𝑣))
123109, 122nfim 1977 . . . . . . . . . . . . . . . . 17 𝑥((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) + (𝐺𝑣)))
124 eleq1w 2833 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → (𝑥𝐴𝑣𝐴))
125124anbi2d 614 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → ((𝜑𝑥𝐴) ↔ (𝜑𝑣𝐴)))
126 fveq2 6333 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → (𝐻𝑥) = (𝐻𝑣))
127 fveq2 6333 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
128 fveq2 6333 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝐺𝑥) = (𝐺𝑣))
129127, 128oveq12d 6813 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐹𝑥) + (𝐺𝑥)) = ((𝐹𝑣) + (𝐺𝑣)))
130126, 129eqeq12d 2786 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → ((𝐻𝑥) = ((𝐹𝑥) + (𝐺𝑥)) ↔ (𝐻𝑣) = ((𝐹𝑣) + (𝐺𝑣))))
131125, 130imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) + (𝐺𝑥))) ↔ ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) + (𝐺𝑣)))))
132 simpr 471 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝑥𝐴)
13389fvmpt2 6435 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝐴 ∧ (𝐵 + 𝐶) ∈ ℂ) → (𝐻𝑥) = (𝐵 + 𝐶))
134132, 88, 133syl2anc 573 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐻𝑥) = (𝐵 + 𝐶))
1359fvmpt2 6435 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴𝐵 ∈ ℂ) → (𝐹𝑥) = 𝐵)
136132, 8, 135syl2anc 573 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
137136eqcomd 2777 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝐵 = (𝐹𝑥))
13825fvmpt2 6435 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴𝐶 ∈ ℂ) → (𝐺𝑥) = 𝐶)
139132, 24, 138syl2anc 573 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → (𝐺𝑥) = 𝐶)
140139eqcomd 2777 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝐶 = (𝐺𝑥))
141137, 140oveq12d 6813 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐵 + 𝐶) = ((𝐹𝑥) + (𝐺𝑥)))
142134, 141eqtrd 2805 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) + (𝐺𝑥)))
143123, 131, 142chvar 2424 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) + (𝐺𝑣)))
144143ad3antrrr 709 . . . . . . . . . . . . . . 15 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (𝐻𝑣) = ((𝐹𝑣) + (𝐺𝑣)))
145144oveq1d 6810 . . . . . . . . . . . . . 14 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → ((𝐻𝑣) − (𝐸 + 𝐼)) = (((𝐹𝑣) + (𝐺𝑣)) − (𝐸 + 𝐼)))
14698, 103, 99, 104addsub4d 10644 . . . . . . . . . . . . . 14 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (((𝐹𝑣) + (𝐺𝑣)) − (𝐸 + 𝐼)) = (((𝐹𝑣) − 𝐸) + ((𝐺𝑣) − 𝐼)))
147145, 146eqtrd 2805 . . . . . . . . . . . . 13 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → ((𝐻𝑣) − (𝐸 + 𝐼)) = (((𝐹𝑣) − 𝐸) + ((𝐺𝑣) − 𝐼)))
148147fveq2d 6337 . . . . . . . . . . . 12 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) = (abs‘(((𝐹𝑣) − 𝐸) + ((𝐺𝑣) − 𝐼))))
149100, 105abstrid 14402 . . . . . . . . . . . 12 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (abs‘(((𝐹𝑣) − 𝐸) + ((𝐺𝑣) − 𝐼))) ≤ ((abs‘((𝐹𝑣) − 𝐸)) + (abs‘((𝐺𝑣) − 𝐼))))
150148, 149eqbrtrd 4809 . . . . . . . . . . 11 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) ≤ ((abs‘((𝐹𝑣) − 𝐸)) + (abs‘((𝐺𝑣) − 𝐼))))
151 simplr 752 . . . . . . . . . . . 12 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2))
152 simpr 471 . . . . . . . . . . . 12 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))
153101, 106, 108, 151, 152lt2halvesd 11486 . . . . . . . . . . 11 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → ((abs‘((𝐹𝑣) − 𝐸)) + (abs‘((𝐺𝑣) − 𝐼))) < 𝑦)
15496, 107, 108, 150, 153lelttrd 10400 . . . . . . . . . 10 (((((𝜑𝑣𝐴) ∧ 𝑦 ∈ ℝ) ∧ (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦)
15576, 87, 154syl2anc 573 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦)
1561553exp 1112 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → (𝑣𝐴 → ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏)) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦)))
15744, 156ralrimi 3106 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏)) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦))
158 breq2 4791 . . . . . . . . . . 11 (𝑤 = if(𝑎𝑏, 𝑎, 𝑏) → ((abs‘(𝑣𝐷)) < 𝑤 ↔ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏)))
159158anbi2d 614 . . . . . . . . . 10 (𝑤 = if(𝑎𝑏, 𝑎, 𝑏) → ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) ↔ (𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏))))
160159imbi1d 330 . . . . . . . . 9 (𝑤 = if(𝑎𝑏, 𝑎, 𝑏) → (((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦) ↔ ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏)) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦)))
161160ralbidv 3135 . . . . . . . 8 (𝑤 = if(𝑎𝑏, 𝑎, 𝑏) → (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦) ↔ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏)) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦)))
162161rspcev 3460 . . . . . . 7 ((if(𝑎𝑏, 𝑎, 𝑏) ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < if(𝑎𝑏, 𝑎, 𝑏)) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦)) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦))
16338, 157, 162syl2anc 573 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2)))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦))
1641633exp 1112 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → ((∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦))))
165164rexlimdvv 3185 . . . 4 ((𝜑𝑦 ∈ ℝ+) → (∃𝑎 ∈ ℝ+𝑏 ∈ ℝ+ (∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑎) → (abs‘((𝐹𝑣) − 𝐸)) < (𝑦 / 2)) ∧ ∀𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑏) → (abs‘((𝐺𝑣) − 𝐼)) < (𝑦 / 2))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦)))
16636, 165mpd 15 . . 3 ((𝜑𝑦 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦))
167166ralrimiva 3115 . 2 (𝜑 → ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦))
16890, 11, 14ellimc3 23862 . 2 (𝜑 → ((𝐸 + 𝐼) ∈ (𝐻 lim 𝐷) ↔ ((𝐸 + 𝐼) ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐷 ∧ (abs‘(𝑣𝐷)) < 𝑤) → (abs‘((𝐻𝑣) − (𝐸 + 𝐼))) < 𝑦))))
1697, 167, 168mpbir2and 692 1 (𝜑 → (𝐸 + 𝐼) ∈ (𝐻 lim 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  wss 3723  ifcif 4226   class class class wbr 4787  cmpt 4864  dom cdm 5250  wf 6026  cfv 6030  (class class class)co 6795  cc 10139  cr 10140   + caddc 10144   < clt 10279  cle 10280  cmin 10471   / cdiv 10889  2c2 11275  +crp 12034  abscabs 14181   lim climc 23845
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 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099  ax-cnex 10197  ax-resscn 10198  ax-1cn 10199  ax-icn 10200  ax-addcl 10201  ax-addrcl 10202  ax-mulcl 10203  ax-mulrcl 10204  ax-mulcom 10205  ax-addass 10206  ax-mulass 10207  ax-distr 10208  ax-i2m1 10209  ax-1ne0 10210  ax-1rid 10211  ax-rnegex 10212  ax-rrecex 10213  ax-cnre 10214  ax-pre-lttri 10215  ax-pre-lttrn 10216  ax-pre-ltadd 10217  ax-pre-mulgt0 10218  ax-pre-sup 10219
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 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6756  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-om 7216  df-1st 7318  df-2nd 7319  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-1o 7716  df-oadd 7720  df-er 7899  df-map 8014  df-pm 8015  df-en 8113  df-dom 8114  df-sdom 8115  df-fin 8116  df-fi 8476  df-sup 8507  df-inf 8508  df-pnf 10281  df-mnf 10282  df-xr 10283  df-ltxr 10284  df-le 10285  df-sub 10473  df-neg 10474  df-div 10890  df-nn 11226  df-2 11284  df-3 11285  df-4 11286  df-5 11287  df-6 11288  df-7 11289  df-8 11290  df-9 11291  df-n0 11499  df-z 11584  df-dec 11700  df-uz 11893  df-q 11996  df-rp 12035  df-xneg 12150  df-xadd 12151  df-xmul 12152  df-fz 12533  df-seq 13008  df-exp 13067  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183  df-struct 16065  df-ndx 16066  df-slot 16067  df-base 16069  df-plusg 16161  df-mulr 16162  df-starv 16163  df-tset 16167  df-ple 16168  df-ds 16171  df-unif 16172  df-rest 16290  df-topn 16291  df-topgen 16311  df-psmet 19952  df-xmet 19953  df-met 19954  df-bl 19955  df-mopn 19956  df-cnfld 19961  df-top 20918  df-topon 20935  df-topsp 20957  df-bases 20970  df-cnp 21252  df-xms 22344  df-ms 22345  df-limc 23849
This theorem is referenced by:  sublimc  40399  reclimc  40400  fourierdlem53  40890  fourierdlem60  40897  fourierdlem61  40898
  Copyright terms: Public domain W3C validator