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

Theorem 0ellimcdiv 40543
Description: If the numerator converges to 0 and the denominator converges to a nonzero number, then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
0ellimcdiv.f 𝐹 = (𝑥𝐴𝐵)
0ellimcdiv.g 𝐺 = (𝑥𝐴𝐶)
0ellimcdiv.h 𝐻 = (𝑥𝐴 ↦ (𝐵 / 𝐶))
0ellimcdiv.b ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
0ellimcdiv.c ((𝜑𝑥𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
0ellimcdiv.0limf (𝜑 → 0 ∈ (𝐹 lim 𝐸))
0ellimcdiv.d (𝜑𝐷 ∈ (𝐺 lim 𝐸))
0ellimcdiv.dne0 (𝜑𝐷 ≠ 0)
Assertion
Ref Expression
0ellimcdiv (𝜑 → 0 ∈ (𝐻 lim 𝐸))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)   𝐸(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝐻(𝑥)

Proof of Theorem 0ellimcdiv
Dummy variables 𝑢 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0cnd 10290 . 2 (𝜑 → 0 ∈ ℂ)
2 0ellimcdiv.d . . . . . . . . 9 (𝜑𝐷 ∈ (𝐺 lim 𝐸))
3 0ellimcdiv.c . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
43eldifad 3746 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
5 0ellimcdiv.g . . . . . . . . . . 11 𝐺 = (𝑥𝐴𝐶)
64, 5fmptd 6578 . . . . . . . . . 10 (𝜑𝐺:𝐴⟶ℂ)
7 0ellimcdiv.f . . . . . . . . . . 11 𝐹 = (𝑥𝐴𝐵)
8 0ellimcdiv.b . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
9 0ellimcdiv.0limf . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐸))
107, 8, 9limcmptdm 40529 . . . . . . . . . 10 (𝜑𝐴 ⊆ ℂ)
11 limcrcl 23943 . . . . . . . . . . . 12 (𝐷 ∈ (𝐺 lim 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
122, 11syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
1312simp3d 1174 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
146, 10, 13ellimc3 23948 . . . . . . . . 9 (𝜑 → (𝐷 ∈ (𝐺 lim 𝐸) ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))))
152, 14mpbid 223 . . . . . . . 8 (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦)))
1615simprd 489 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))
1715simpld 488 . . . . . . . . 9 (𝜑𝐷 ∈ ℂ)
18 0ellimcdiv.dne0 . . . . . . . . 9 (𝜑𝐷 ≠ 0)
1917, 18absrpcld 14486 . . . . . . . 8 (𝜑 → (abs‘𝐷) ∈ ℝ+)
2019rphalfcld 12087 . . . . . . 7 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ+)
21 breq2 4815 . . . . . . . . . 10 (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2221imbi2d 331 . . . . . . . . 9 (𝑦 = ((abs‘𝐷) / 2) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2322rexralbidv 3205 . . . . . . . 8 (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2423rspccva 3461 . . . . . . 7 ((∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2516, 20, 24syl2anc 579 . . . . . 6 (𝜑 → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26 simpl1l 1293 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝜑)
27 simpl3 1246 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝑣𝐴)
28 simpr 477 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧))
29 simpl2 1244 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
3027, 28, 29mp2d 49 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
3119rpcnd 12077 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝐷) ∈ ℂ)
32312halvesd 11528 . . . . . . . . . . . . . . 15 (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
3332eqcomd 2771 . . . . . . . . . . . . . 14 (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
3433oveq1d 6861 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35 2cnd 11354 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℂ)
36 2ne0 11387 . . . . . . . . . . . . . . . . 17 2 ≠ 0
3736a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≠ 0)
3817, 35, 37absdivd 14493 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39 2re 11350 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
4039a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ)
41 0le2 11385 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 2)
4340, 42absidd 14460 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘2) = 2)
4443oveq2d 6862 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
4538, 44eqtr2d 2800 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
4645oveq2d 6862 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
4720rpcnd 12077 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
4847, 47pncand 10651 . . . . . . . . . . . . 13 (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
4934, 46, 483eqtr3rd 2808 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50493ad2ant1 1163 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
5145eqcomd 2771 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52513ad2ant1 1163 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
5352oveq2d 6862 . . . . . . . . . . . 12 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
5417adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → 𝐷 ∈ ℂ)
5554abscld 14474 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ∈ ℝ)
56553adant3 1162 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
576ffvelrnda 6553 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ∈ ℂ)
58573adant3 1162 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺𝑣) ∈ ℂ)
5958abscld 14474 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
60173ad2ant1 1163 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
6160, 58subcld 10650 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
6261abscld 14474 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) ∈ ℝ)
6359, 62readdcld 10327 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) ∈ ℝ)
6456rehalfcld 11529 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
6559, 64readdcld 10327 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
6657, 54pncan3d 10653 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → ((𝐺𝑣) + (𝐷 − (𝐺𝑣))) = 𝐷)
6766eqcomd 2771 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → 𝐷 = ((𝐺𝑣) + (𝐷 − (𝐺𝑣))))
6867fveq2d 6383 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘𝐷) = (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))))
6954, 57subcld 10650 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
7057, 69abstrid 14494 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7168, 70eqbrtrd 4833 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
72713adant3 1162 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7360, 58abssubd 14491 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) = (abs‘((𝐺𝑣) − 𝐷)))
74 simp3 1168 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
7573, 74eqbrtrd 4833 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) < ((abs‘𝐷) / 2))
7662, 64, 59, 75ltadd2dd 10454 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7756, 63, 65, 72, 76lelttrd 10453 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7857abscld 14474 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ)
79783adant3 1162 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
8056, 64, 79ltsubaddd 10881 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺𝑣)) ↔ (abs‘𝐷) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2))))
8177, 80mpbird 248 . . . . . . . . . . . 12 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺𝑣)))
8253, 81eqbrtrd 4833 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺𝑣)))
8350, 82eqbrtrd 4833 . . . . . . . . . 10 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
8426, 27, 30, 83syl3anc 1490 . . . . . . . . 9 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
85843exp1 1461 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ+) → ((𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))))
8685ralimdv2 3108 . . . . . . 7 ((𝜑𝑧 ∈ ℝ+) → (∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))))
8786reximdva 3163 . . . . . 6 (𝜑 → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))))
8825, 87mpd 15 . . . . 5 (𝜑 → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
8988adantr 472 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
90 simpr 477 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
9117adantr 472 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐷 ∈ ℂ)
9218adantr 472 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐷 ≠ 0)
9391, 92absrpcld 14486 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (abs‘𝐷) ∈ ℝ+)
9493rphalfcld 12087 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → ((abs‘𝐷) / 2) ∈ ℝ+)
9590, 94rpmulcld 12091 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)
9695ex 401 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℝ+ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9796imdistani 564 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
98 eleq1 2832 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ+ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9998anbi2d 622 . . . . . . . . . 10 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑𝑤 ∈ ℝ+) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)))
100 breq2 4815 . . . . . . . . . . . 12 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((abs‘((𝐹𝑣) − 0)) < 𝑤 ↔ (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
101100imbi2d 331 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
102101rexralbidv 3205 . . . . . . . . . 10 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤) ↔ ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
10399, 102imbi12d 335 . . . . . . . . 9 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝜑𝑤 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤)) ↔ ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))))
1048, 7fmptd 6578 . . . . . . . . . . . . 13 (𝜑𝐹:𝐴⟶ℂ)
105104, 10, 13ellimc3 23948 . . . . . . . . . . . 12 (𝜑 → (0 ∈ (𝐹 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))))
1069, 105mpbid 223 . . . . . . . . . . 11 (𝜑 → (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤)))
107106simprd 489 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
108107r19.21bi 3079 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
109103, 108vtoclg 3418 . . . . . . . 8 ((𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+ → ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
11095, 97, 109sylc 65 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
1111103ad2ant1 1163 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112 simp12 1261 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ+)
113 simp2 1167 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ+)
114112, 113ifcld 4290 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+)
115 nfv 2009 . . . . . . . . . . 11 𝑣(𝜑𝑦 ∈ ℝ+)
116 nfv 2009 . . . . . . . . . . 11 𝑣 𝑧 ∈ ℝ+
117 nfra1 3088 . . . . . . . . . . 11 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
118115, 116, 117nf3an 2000 . . . . . . . . . 10 𝑣((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
119 nfv 2009 . . . . . . . . . 10 𝑣 𝑢 ∈ ℝ+
120 nfra1 3088 . . . . . . . . . 10 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121118, 119, 120nf3an 2000 . . . . . . . . 9 𝑣(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122 simp111 1401 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝜑𝑦 ∈ ℝ+))
123 simp112 1402 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ+)
124 simp12 1261 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ+)
125122, 123, 124jca31 510 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+))
126 simp2 1167 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐴)
127 simp3l 1258 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐸)
128125, 126, 127jca31 510 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸))
12910adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → 𝐴 ⊆ ℂ)
1301293ad2ant1 1163 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐴 ⊆ ℂ)
1311303ad2ant1 1163 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
1321313ad2ant1 1163 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133132, 126sseldd 3764 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
13413adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → 𝐸 ∈ ℂ)
1351343ad2ant1 1163 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐸 ∈ ℂ)
1361353ad2ant1 1163 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
1371363ad2ant1 1163 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138133, 137subcld 10650 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝑣𝐸) ∈ ℂ)
139138abscld 14474 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) ∈ ℝ)
140123rpred 12075 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141124rpred 12075 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142140, 141ifcld 4290 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ)
143 simp3r 1259 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))
144 min1 12227 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
145140, 141, 144syl2anc 579 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
146139, 142, 140, 143, 145ltletrd 10455 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < 𝑧)
147 simp113 1403 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
148 rspa 3077 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
149147, 126, 148syl2anc 579 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
150127, 146, 149mp2and 690 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
151 simp13 1262 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152 rspa 3077 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153151, 126, 152syl2anc 579 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154 min2 12228 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
155140, 141, 154syl2anc 579 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
156139, 142, 141, 143, 155ltletrd 10455 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < 𝑢)
157127, 156jca 507 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢))
158122simpld 488 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝜑)
1591583ad2ant1 1163 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝜑)
160 simp12 1261 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝑣𝐴)
161 nfv 2009 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑣𝐴)
162 nfmpt1 4908 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
1637, 162nfcxfr 2905 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
164 nfcv 2907 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑣
165163, 164nffv 6389 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝐹𝑣)
166165nfel1 2922 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐹𝑣) ∈ ℂ
167161, 166nfim 1995 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
168 eleq1 2832 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝑥𝐴𝑣𝐴))
169168anbi2d 622 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝜑𝑥𝐴) ↔ (𝜑𝑣𝐴)))
170 fveq2 6379 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
171170eleq1d 2829 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐹𝑥) ∈ ℂ ↔ (𝐹𝑣) ∈ ℂ))
172169, 171imbi12d 335 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ) ↔ ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)))
173 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → 𝑥𝐴)
1747fvmpt2 6484 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐵 ∈ ℂ) → (𝐹𝑥) = 𝐵)
175173, 8, 174syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
176175, 8eqeltrd 2844 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ)
177167, 172, 176chvar 2368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
178177subid1d 10639 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → ((𝐹𝑣) − 0) = (𝐹𝑣))
179178eqcomd 2771 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐹𝑣) = ((𝐹𝑣) − 0))
180179fveq2d 6383 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
181159, 160, 180syl2anc 579 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
182 simp3 1168 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢))
183 simp2 1167 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
184182, 183mpd 15 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
185181, 184eqbrtrd 4833 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
186153, 157, 185mpd3an23 1587 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
187 simp-7l 813 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
188 simp-4r 803 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
189 eldifsni 4478 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
1903, 189syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝐶 ≠ 0)
1918, 4, 190divcld 11059 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192 0ellimcdiv.h . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥𝐴 ↦ (𝐵 / 𝐶))
193191, 192fmptd 6578 . . . . . . . . . . . . . . . . 17 (𝜑𝐻:𝐴⟶ℂ)
194193ffvelrnda 6553 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (𝐻𝑣) ∈ ℂ)
195194subid1d 10639 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = (𝐻𝑣))
196 nfmpt1 4908 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥𝐴 ↦ (𝐵 / 𝐶))
197192, 196nfcxfr 2905 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
198197, 164nffv 6389 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑣)
199 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑥 /
200 nfmpt1 4908 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑥𝐴𝐶)
2015, 200nfcxfr 2905 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐺
202201, 164nffv 6389 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣)
203165, 199, 202nfov 6876 . . . . . . . . . . . . . . . . . 18 𝑥((𝐹𝑣) / (𝐺𝑣))
204198, 203nfeq 2919 . . . . . . . . . . . . . . . . 17 𝑥(𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))
205161, 204nfim 1995 . . . . . . . . . . . . . . . 16 𝑥((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
206 fveq2 6379 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (𝐻𝑥) = (𝐻𝑣))
207 fveq2 6379 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → (𝐺𝑥) = (𝐺𝑣))
208170, 207oveq12d 6864 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → ((𝐹𝑥) / (𝐺𝑥)) = ((𝐹𝑣) / (𝐺𝑣)))
209206, 208eqeq12d 2780 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → ((𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)) ↔ (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))))
210169, 209imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥))) ↔ ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))))
211192fvmpt2 6484 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻𝑥) = (𝐵 / 𝐶))
212173, 191, 211syl2anc 579 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐻𝑥) = (𝐵 / 𝐶))
213175eqcomd 2771 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵 = (𝐹𝑥))
2145fvmpt2 6484 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐶 ∈ (ℂ ∖ {0})) → (𝐺𝑥) = 𝐶)
215173, 3, 214syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐺𝑥) = 𝐶)
216215eqcomd 2771 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐶 = (𝐺𝑥))
217213, 216oveq12d 6864 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) = ((𝐹𝑥) / (𝐺𝑥)))
218212, 217eqtrd 2799 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)))
219205, 210, 218chvar 2368 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
220195, 219eqtrd 2799 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = ((𝐹𝑣) / (𝐺𝑣)))
221220fveq2d 6383 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
222187, 188, 221syl2anc 579 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
223 simp-6l 809 . . . . . . . . . . . . . 14 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝜑𝑦 ∈ ℝ+))
224223, 188jca 507 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴))
225 simplr 785 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
226 simpr 477 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
227 nfcv 2907 . . . . . . . . . . . . . . . . . . . 20 𝑥0
228202, 227nfne 3037 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣) ≠ 0
229161, 228nfim 1995 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
230207neeq1d 2996 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐺𝑥) ≠ 0 ↔ (𝐺𝑣) ≠ 0))
231169, 230imbi12d 335 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0) ↔ ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)))
232215, 190eqnetrd 3004 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0)
233229, 231, 232chvar 2368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
234177, 57, 233absdivd 14493 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
235234adantlr 706 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
236235ad2antrr 717 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
237177abscld 14474 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) ∈ ℝ)
23857, 233absne0d 14485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
239237, 78, 238redivcld 11111 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
240239adantlr 706 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
241240ad2antrr 717 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
242 rpre 12041 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
243242ad2antlr 718 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℝ)
24420rpred 12075 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245244ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246243, 245remulcld 10328 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247246ad2antrr 717 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
24857, 233absrpcld 14486 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
249248adantlr 706 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
250249ad2antrr 717 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
251247, 250rerpdivcld 12106 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) ∈ ℝ)
252243ad2antrr 717 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑦 ∈ ℝ)
253 simp-4l 801 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
254 simpllr 793 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
255253, 254, 237syl2anc 579 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) ∈ ℝ)
256 simpr 477 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
257255, 247, 250, 256ltdiv1dd 12132 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))))
258243recnd 10326 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℂ)
25947ad2antrr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260249rpcnd 12077 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℂ)
261238adantlr 706 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
262258, 259, 260, 261divassd 11094 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
263262adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
264245, 249rerpdivcld 12106 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
265264adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
266 1red 10298 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ)
267 simpllr 793 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 𝑦 ∈ ℝ+)
268244ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269 1rp 12037 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ+
270269a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ+)
271248adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
27247div1d 11051 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273272ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
275273, 274eqbrtrd 4833 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺𝑣)))
276268, 270, 271, 275ltdiv23d 12142 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
277276adantllr 710 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
278265, 266, 267, 277ltmul2dd 12131 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))) < (𝑦 · 1))
279263, 278eqbrtrd 4833 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < (𝑦 · 1))
280258mulid1d 10315 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · 1) = 𝑦)
281280adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · 1) = 𝑦)
282279, 281breqtrd 4837 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
283282adantr 472 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
284241, 251, 252, 257, 283lttrd 10456 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < 𝑦)
285236, 284eqbrtrd 4833 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
286224, 225, 226, 285syl21anc 866 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
287222, 286eqbrtrd 4833 . . . . . . . . . . 11 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
288128, 150, 186, 287syl21anc 866 . . . . . . . . . 10 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
2892883exp 1148 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
290121, 289ralrimi 3104 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
291 brimralrspcev 4872 . . . . . . . 8 ((if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
292114, 290, 291syl2anc 579 . . . . . . 7 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
293292rexlimdv3a 3180 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → (∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
294111, 293mpd 15 . . . . 5 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
295294rexlimdv3a 3180 . . . 4 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
29689, 295mpd 15 . . 3 ((𝜑𝑦 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
297296ralrimiva 3113 . 2 (𝜑 → ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
298193, 10, 13ellimc3 23948 . 2 (𝜑 → (0 ∈ (𝐻 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))))
2991, 297, 298mpbir2and 704 1 (𝜑 → 0 ∈ (𝐻 lim 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  cdif 3731  wss 3734  ifcif 4245  {csn 4336   class class class wbr 4811  cmpt 4890  dom cdm 5279  wf 6066  cfv 6070  (class class class)co 6846  cc 10191  cr 10192  0cc0 10193  1c1 10194   + caddc 10196   · cmul 10198   < clt 10332  cle 10333  cmin 10524   / cdiv 10942  2c2 11331  +crp 12033  abscabs 14273   lim climc 23931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-fi 8528  df-sup 8559  df-inf 8560  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-div 10943  df-nn 11279  df-2 11339  df-3 11340  df-4 11341  df-5 11342  df-6 11343  df-7 11344  df-8 11345  df-9 11346  df-n0 11543  df-z 11629  df-dec 11746  df-uz 11892  df-q 11995  df-rp 12034  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-fz 12539  df-seq 13014  df-exp 13073  df-cj 14138  df-re 14139  df-im 14140  df-sqrt 14274  df-abs 14275  df-struct 16146  df-ndx 16147  df-slot 16148  df-base 16150  df-plusg 16241  df-mulr 16242  df-starv 16243  df-tset 16247  df-ple 16248  df-ds 16250  df-unif 16251  df-rest 16363  df-topn 16364  df-topgen 16384  df-psmet 20025  df-xmet 20026  df-met 20027  df-bl 20028  df-mopn 20029  df-cnfld 20034  df-top 20992  df-topon 21009  df-topsp 21031  df-bases 21044  df-cnp 21326  df-xms 22418  df-ms 22419  df-limc 23935
This theorem is referenced by:  reclimc  40547
  Copyright terms: Public domain W3C validator