This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addlimc

Description: Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses addlimc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
addlimc.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
addlimc.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) )
addlimc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
addlimc.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
addlimc.e ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 limℂ 𝐷 ) )
addlimc.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 limℂ 𝐷 ) )
Assertion addlimc ( 𝜑 → ( 𝐸 + 𝐼 ) ∈ ( 𝐻 limℂ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 addlimc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 addlimc.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
3 addlimc.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) )
4 addlimc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5 addlimc.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
6 addlimc.e ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 limℂ 𝐷 ) )
7 addlimc.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 limℂ 𝐷 ) )
8 limccl ⊢ ( 𝐹 limℂ 𝐷 ) ⊆ ℂ
9 8 6 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
10 limccl ⊢ ( 𝐺 limℂ 𝐷 ) ⊆ ℂ
11 10 7 sselid ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
12 9 11 addcld ⊢ ( 𝜑 → ( 𝐸 + 𝐼 ) ∈ ℂ )
13 4 1 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
14 1 4 6 limcmptdm ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
15 limcrcl ⊢ ( 𝐸 ∈ ( 𝐹 limℂ 𝐷 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
16 6 15 syl ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
17 16 simp3d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
18 13 14 17 ellimc3 ⊢ ( 𝜑 → ( 𝐸 ∈ ( 𝐹 limℂ 𝐷 ) ↔ ( 𝐸 ∈ ℂ ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < 𝑧 ) ) ) )
19 6 18 mpbid ⊢ ( 𝜑 → ( 𝐸 ∈ ℂ ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < 𝑧 ) ) )
20 19 simprd ⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < 𝑧 ) )
21 rphalfcl ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ+ )
22 breq2 ⊢ ( 𝑧 = ( 𝑦 / 2 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < 𝑧 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) )
23 22 imbi2d ⊢ ( 𝑧 = ( 𝑦 / 2 ) → ( ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < 𝑧 ) ↔ ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ) )
24 23 rexralbidv ⊢ ( 𝑧 = ( 𝑦 / 2 ) → ( ∃ 𝑎 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < 𝑧 ) ↔ ∃ 𝑎 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ) )
25 24 rspccva ⊢ ( ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < 𝑧 ) ∧ ( 𝑦 / 2 ) ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) )
26 20 21 25 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) )
27 5 2 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℂ )
28 27 14 17 ellimc3 ⊢ ( 𝜑 → ( 𝐼 ∈ ( 𝐺 limℂ 𝐷 ) ↔ ( 𝐼 ∈ ℂ ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < 𝑧 ) ) ) )
29 7 28 mpbid ⊢ ( 𝜑 → ( 𝐼 ∈ ℂ ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < 𝑧 ) ) )
30 29 simprd ⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < 𝑧 ) )
31 breq2 ⊢ ( 𝑧 = ( 𝑦 / 2 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < 𝑧 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) )
32 31 imbi2d ⊢ ( 𝑧 = ( 𝑦 / 2 ) → ( ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < 𝑧 ) ↔ ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) )
33 32 rexralbidv ⊢ ( 𝑧 = ( 𝑦 / 2 ) → ( ∃ 𝑏 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < 𝑧 ) ↔ ∃ 𝑏 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) )
34 33 rspccva ⊢ ( ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < 𝑧 ) ∧ ( 𝑦 / 2 ) ∈ ℝ+ ) → ∃ 𝑏 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) )
35 30 21 34 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑏 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) )
36 reeanv ⊢ ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ↔ ( ∃ 𝑎 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑏 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) )
37 26 35 36 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) )
38 ifcl ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ+ )
39 38 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ+ )
40 nfv ⊢ Ⅎ 𝑣 ( 𝜑 ∧ 𝑦 ∈ ℝ+ )
41 nfv ⊢ Ⅎ 𝑣 ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ )
42 nfra1 ⊢ Ⅎ 𝑣 ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) )
43 nfra1 ⊢ Ⅎ 𝑣 ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) )
44 42 43 nfan ⊢ Ⅎ 𝑣 ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) )
45 40 41 44 nf3an ⊢ Ⅎ 𝑣 ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) )
46 simp11l ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → 𝜑 )
47 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → 𝑣 ∈ 𝐴 )
48 46 47 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) )
49 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
51 50 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → 𝑦 ∈ ℝ )
52 51 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → 𝑦 ∈ ℝ )
53 simp13l ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) )
54 simp3l ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → 𝑣 ≠ 𝐷 )
55 14 sselda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ ℂ )
56 46 47 55 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → 𝑣 ∈ ℂ )
57 46 17 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → 𝐷 ∈ ℂ )
58 56 57 subcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( 𝑣 − 𝐷 ) ∈ ℂ )
59 58 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( abs ‘ ( 𝑣 − 𝐷 ) ) ∈ ℝ )
60 39 rpred ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ )
61 60 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ )
62 simpl ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑎 ∈ ℝ+ )
63 62 rpred ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑎 ∈ ℝ )
64 63 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → 𝑎 ∈ ℝ )
65 64 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → 𝑎 ∈ ℝ )
66 simp3r ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) )
67 simpr ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑏 ∈ ℝ+ )
68 67 rpred ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑏 ∈ ℝ )
69 min1 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑎 )
70 63 68 69 syl2anc ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑎 )
71 70 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑎 )
72 71 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑎 )
73 59 61 65 66 72 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 )
74 54 73 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) )
75 rsp ⊢ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) → ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ) )
76 53 47 74 75 syl3c ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) )
77 48 52 76 jca31 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) )
78 simp13r ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) )
79 68 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → 𝑏 ∈ ℝ )
80 79 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → 𝑏 ∈ ℝ )
81 min2 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑏 )
82 63 68 81 syl2anc ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑏 )
83 82 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑏 )
84 83 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑏 )
85 59 61 80 66 84 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 )
86 54 85 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) )
87 rsp ⊢ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) )
88 78 47 86 87 syl3c ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) )
89 4 5 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
90 89 3 fmptd ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ ℂ )
91 90 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑣 ) ∈ ℂ )
92 91 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( 𝐻 ‘ 𝑣 ) ∈ ℂ )
93 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → 𝜑 )
94 93 12 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( 𝐸 + 𝐼 ) ∈ ℂ )
95 92 94 subcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ∈ ℂ )
96 95 abscld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) ∈ ℝ )
97 13 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ ℂ )
98 97 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( 𝐹 ‘ 𝑣 ) ∈ ℂ )
99 93 9 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → 𝐸 ∈ ℂ )
100 98 99 subcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ∈ ℂ )
101 100 abscld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) ∈ ℝ )
102 27 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑣 ) ∈ ℂ )
103 102 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( 𝐺 ‘ 𝑣 ) ∈ ℂ )
104 93 11 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → 𝐼 ∈ ℂ )
105 103 104 subcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ∈ ℂ )
106 105 abscld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) ∈ ℝ )
107 101 106 readdcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) ) ∈ ℝ )
108 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → 𝑦 ∈ ℝ )
109 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑣 ∈ 𝐴 )
110 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) )
111 3 110 nfcxfr ⊢ Ⅎ 𝑥 𝐻
112 nfcv ⊢ Ⅎ 𝑥 𝑣
113 111 112 nffv ⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑣 )
114 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
115 1 114 nfcxfr ⊢ Ⅎ 𝑥 𝐹
116 115 112 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑣 )
117 nfcv ⊢ Ⅎ 𝑥 +
118 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
119 2 118 nfcxfr ⊢ Ⅎ 𝑥 𝐺
120 119 112 nffv ⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑣 )
121 116 117 120 nfov ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) )
122 113 121 nfeq ⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) )
123 109 122 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) ) )
124 eleq1w ⊢ ( 𝑥 = 𝑣 → ( 𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴 ) )
125 124 anbi2d ⊢ ( 𝑥 = 𝑣 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ) )
126 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑣 ) )
127 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑣 ) )
128 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑣 ) )
129 127 128 oveq12d ⊢ ( 𝑥 = 𝑣 → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) ) )
130 126 129 eqeq12d ⊢ ( 𝑥 = 𝑣 → ( ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) ) ) )
131 125 130 imbi12d ⊢ ( 𝑥 = 𝑣 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) ) ) ) )
132 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
133 3 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐵 + 𝐶 ) ∈ ℂ ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐵 + 𝐶 ) )
134 132 89 133 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐵 + 𝐶 ) )
135 1 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
136 132 4 135 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
137 136 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = ( 𝐹 ‘ 𝑥 ) )
138 2 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
139 132 5 138 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
140 139 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = ( 𝐺 ‘ 𝑥 ) )
141 137 140 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
142 134 141 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
143 123 131 142 chvarfv ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) ) )
144 143 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) ) )
145 144 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) = ( ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) ) − ( 𝐸 + 𝐼 ) ) )
146 98 103 99 104 addsub4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( ( ( 𝐹 ‘ 𝑣 ) + ( 𝐺 ‘ 𝑣 ) ) − ( 𝐸 + 𝐼 ) ) = ( ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) + ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) )
147 145 146 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) = ( ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) + ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) )
148 147 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) + ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) ) )
149 100 105 abstrid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) + ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) ) )
150 148 149 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) ) )
151 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) )
152 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) )
153 101 106 108 151 152 lt2halvesd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) ) < 𝑦 )
154 96 107 108 150 153 lelttrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 )
155 77 88 154 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 )
156 155 3exp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) ) )
157 45 156 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) )
158 brimralrspcev ⊢ ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ+ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) )
159 39 157 158 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) )
160 159 3exp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) ) ) )
161 160 rexlimdvv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐸 ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐼 ) ) < ( 𝑦 / 2 ) ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) ) )
162 37 161 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) )
163 162 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) )
164 90 14 17 ellimc3 ⊢ ( 𝜑 → ( ( 𝐸 + 𝐼 ) ∈ ( 𝐻 limℂ 𝐷 ) ↔ ( ( 𝐸 + 𝐼 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐷 ∧ ( abs ‘ ( 𝑣 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − ( 𝐸 + 𝐼 ) ) ) < 𝑦 ) ) ) )
165 12 163 164 mpbir2and ⊢ ( 𝜑 → ( 𝐸 + 𝐼 ) ∈ ( 𝐻 limℂ 𝐷 ) )