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 40402
Description: If the numerator converges to 0 and the denominator converges to non zero 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 10245 . 2 (𝜑 → 0 ∈ ℂ)
2 0ellimcdiv.d . . . . . . . . 9 (𝜑𝐷 ∈ (𝐺 lim 𝐸))
3 0ellimcdiv.c . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
43eldifad 3727 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
5 0ellimcdiv.g . . . . . . . . . . 11 𝐺 = (𝑥𝐴𝐶)
64, 5fmptd 6549 . . . . . . . . . 10 (𝜑𝐺:𝐴⟶ℂ)
7 0ellimcdiv.f . . . . . . . . . . 11 𝐹 = (𝑥𝐴𝐵)
8 0ellimcdiv.b . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
9 0ellimcdiv.0limf . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐸))
107, 8, 9limcmptdm 40388 . . . . . . . . . 10 (𝜑𝐴 ⊆ ℂ)
11 limcrcl 23857 . . . . . . . . . . . 12 (𝐷 ∈ (𝐺 lim 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
122, 11syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
1312simp3d 1139 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
146, 10, 13ellimc3 23862 . . . . . . . . 9 (𝜑 → (𝐷 ∈ (𝐺 lim 𝐸) ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))))
152, 14mpbid 222 . . . . . . . 8 (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦)))
1615simprd 482 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))
1715simpld 477 . . . . . . . . 9 (𝜑𝐷 ∈ ℂ)
18 0ellimcdiv.dne0 . . . . . . . . 9 (𝜑𝐷 ≠ 0)
1917, 18absrpcld 14406 . . . . . . . 8 (𝜑 → (abs‘𝐷) ∈ ℝ+)
2019rphalfcld 12097 . . . . . . 7 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ+)
21 breq2 4808 . . . . . . . . . 10 (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2221imbi2d 329 . . . . . . . . 9 (𝑦 = ((abs‘𝐷) / 2) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2322rexralbidv 3196 . . . . . . . 8 (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2423rspccva 3448 . . . . . . 7 ((∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2516, 20, 24syl2anc 696 . . . . . 6 (𝜑 → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26 simpl1l 1279 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝜑)
27 simpl3 1232 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝑣𝐴)
28 simpr 479 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧))
29 simpl2 1230 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
3027, 28, 29mp2d 49 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
3119rpcnd 12087 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝐷) ∈ ℂ)
32312halvesd 11490 . . . . . . . . . . . . . . 15 (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
3332eqcomd 2766 . . . . . . . . . . . . . 14 (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
3433oveq1d 6829 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35 2cnd 11305 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℂ)
36 2ne0 11325 . . . . . . . . . . . . . . . . 17 2 ≠ 0
3736a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≠ 0)
3817, 35, 37absdivd 14413 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39 2re 11302 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
4039a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ)
41 0le2 11323 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 2)
4340, 42absidd 14380 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘2) = 2)
4443oveq2d 6830 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
4538, 44eqtr2d 2795 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
4645oveq2d 6830 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
4720rpcnd 12087 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
4847, 47pncand 10605 . . . . . . . . . . . . 13 (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
4934, 46, 483eqtr3rd 2803 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50493ad2ant1 1128 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
5145eqcomd 2766 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52513ad2ant1 1128 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
5352oveq2d 6830 . . . . . . . . . . . 12 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
5417adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → 𝐷 ∈ ℂ)
5554abscld 14394 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ∈ ℝ)
56553adant3 1127 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
576ffvelrnda 6523 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ∈ ℂ)
58573adant3 1127 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺𝑣) ∈ ℂ)
5958abscld 14394 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
60173ad2ant1 1128 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
6160, 58subcld 10604 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
6261abscld 14394 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) ∈ ℝ)
6359, 62readdcld 10281 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) ∈ ℝ)
6456rehalfcld 11491 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
6559, 64readdcld 10281 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
6657, 54pncan3d 10607 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → ((𝐺𝑣) + (𝐷 − (𝐺𝑣))) = 𝐷)
6766eqcomd 2766 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → 𝐷 = ((𝐺𝑣) + (𝐷 − (𝐺𝑣))))
6867fveq2d 6357 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘𝐷) = (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))))
6954, 57subcld 10604 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
7057, 69abstrid 14414 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7168, 70eqbrtrd 4826 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
72713adant3 1127 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7360, 58abssubd 14411 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) = (abs‘((𝐺𝑣) − 𝐷)))
74 simp3 1133 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
7573, 74eqbrtrd 4826 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) < ((abs‘𝐷) / 2))
7662, 64, 59, 75ltadd2dd 10408 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7756, 63, 65, 72, 76lelttrd 10407 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7857abscld 14394 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ)
79783adant3 1127 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
8056, 64, 79ltsubaddd 10835 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺𝑣)) ↔ (abs‘𝐷) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2))))
8177, 80mpbird 247 . . . . . . . . . . . 12 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺𝑣)))
8253, 81eqbrtrd 4826 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺𝑣)))
8350, 82eqbrtrd 4826 . . . . . . . . . 10 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
8426, 27, 30, 83syl3anc 1477 . . . . . . . . 9 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
85843exp1 1446 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ+) → ((𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))))
8685ralimdv2 3099 . . . . . . 7 ((𝜑𝑧 ∈ ℝ+) → (∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))))
8786reximdva 3155 . . . . . 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 479 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
9117adantr 472 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐷 ∈ ℂ)
9218adantr 472 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐷 ≠ 0)
9391, 92absrpcld 14406 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (abs‘𝐷) ∈ ℝ+)
9493rphalfcld 12097 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → ((abs‘𝐷) / 2) ∈ ℝ+)
9590, 94rpmulcld 12101 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)
9695ex 449 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℝ+ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9796imdistani 728 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
98 eleq1 2827 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ+ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9998anbi2d 742 . . . . . . . . . 10 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑𝑤 ∈ ℝ+) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)))
100 breq2 4808 . . . . . . . . . . . 12 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((abs‘((𝐹𝑣) − 0)) < 𝑤 ↔ (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
101100imbi2d 329 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
102101rexralbidv 3196 . . . . . . . . . 10 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤) ↔ ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
10399, 102imbi12d 333 . . . . . . . . 9 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝜑𝑤 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤)) ↔ ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))))
1048, 7fmptd 6549 . . . . . . . . . . . . 13 (𝜑𝐹:𝐴⟶ℂ)
105104, 10, 13ellimc3 23862 . . . . . . . . . . . 12 (𝜑 → (0 ∈ (𝐹 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))))
1069, 105mpbid 222 . . . . . . . . . . 11 (𝜑 → (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤)))
107106simprd 482 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
108107r19.21bi 3070 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
109103, 108vtoclg 3406 . . . . . . . 8 ((𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+ → ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
11095, 97, 109sylc 65 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
1111103ad2ant1 1128 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112 simp12 1247 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ+)
113 simp2 1132 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ+)
114112, 113ifcld 4275 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+)
115 nfv 1992 . . . . . . . . . . 11 𝑣(𝜑𝑦 ∈ ℝ+)
116 nfv 1992 . . . . . . . . . . 11 𝑣 𝑧 ∈ ℝ+
117 nfra1 3079 . . . . . . . . . . 11 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
118115, 116, 117nf3an 1980 . . . . . . . . . 10 𝑣((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
119 nfv 1992 . . . . . . . . . 10 𝑣 𝑢 ∈ ℝ+
120 nfra1 3079 . . . . . . . . . 10 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121118, 119, 120nf3an 1980 . . . . . . . . 9 𝑣(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122 simp111 1387 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝜑𝑦 ∈ ℝ+))
123 simp112 1388 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ+)
124 simp12 1247 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ+)
125122, 123, 124jca31 558 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+))
126 simp2 1132 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐴)
127 simp3l 1244 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐸)
128125, 126, 127jca31 558 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸))
12910adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → 𝐴 ⊆ ℂ)
1301293ad2ant1 1128 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐴 ⊆ ℂ)
1311303ad2ant1 1128 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
1321313ad2ant1 1128 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133132, 126sseldd 3745 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
13413adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → 𝐸 ∈ ℂ)
1351343ad2ant1 1128 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐸 ∈ ℂ)
1361353ad2ant1 1128 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
1371363ad2ant1 1128 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138133, 137subcld 10604 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝑣𝐸) ∈ ℂ)
139138abscld 14394 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) ∈ ℝ)
140123rpred 12085 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141124rpred 12085 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142140, 141ifcld 4275 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ)
143 simp3r 1245 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))
144 min1 12233 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
145140, 141, 144syl2anc 696 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
146139, 142, 140, 143, 145ltletrd 10409 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < 𝑧)
147 simp113 1389 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
148 rspa 3068 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
149147, 126, 148syl2anc 696 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
150127, 146, 149mp2and 717 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
151 simp13 1248 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152 rspa 3068 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153151, 126, 152syl2anc 696 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154 min2 12234 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
155140, 141, 154syl2anc 696 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
156139, 142, 141, 143, 155ltletrd 10409 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < 𝑢)
157127, 156jca 555 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢))
158122simpld 477 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝜑)
1591583ad2ant1 1128 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝜑)
160 simp12 1247 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝑣𝐴)
161 nfv 1992 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑣𝐴)
162 nfmpt1 4899 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
1637, 162nfcxfr 2900 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
164 nfcv 2902 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑣
165163, 164nffv 6360 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝐹𝑣)
166165nfel1 2917 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐹𝑣) ∈ ℂ
167161, 166nfim 1974 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
168 eleq1 2827 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝑥𝐴𝑣𝐴))
169168anbi2d 742 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝜑𝑥𝐴) ↔ (𝜑𝑣𝐴)))
170 fveq2 6353 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
171170eleq1d 2824 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐹𝑥) ∈ ℂ ↔ (𝐹𝑣) ∈ ℂ))
172169, 171imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ) ↔ ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)))
173 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → 𝑥𝐴)
1747fvmpt2 6454 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐵 ∈ ℂ) → (𝐹𝑥) = 𝐵)
175173, 8, 174syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
176175, 8eqeltrd 2839 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ)
177167, 172, 176chvar 2407 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
178177subid1d 10593 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → ((𝐹𝑣) − 0) = (𝐹𝑣))
179178eqcomd 2766 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐹𝑣) = ((𝐹𝑣) − 0))
180179fveq2d 6357 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
181159, 160, 180syl2anc 696 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
182 simp3 1133 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢))
183 simp2 1132 . . . . . . . . . . . . . 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 4826 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
186153, 157, 185mpd3an23 1575 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
187 simp-7l 837 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
188 simp-4r 827 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
189 eldifsni 4466 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
1903, 189syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝐶 ≠ 0)
1918, 4, 190divcld 11013 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192 0ellimcdiv.h . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥𝐴 ↦ (𝐵 / 𝐶))
193191, 192fmptd 6549 . . . . . . . . . . . . . . . . 17 (𝜑𝐻:𝐴⟶ℂ)
194193ffvelrnda 6523 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (𝐻𝑣) ∈ ℂ)
195194subid1d 10593 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = (𝐻𝑣))
196 nfmpt1 4899 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥𝐴 ↦ (𝐵 / 𝐶))
197192, 196nfcxfr 2900 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
198197, 164nffv 6360 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑣)
199 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑥 /
200 nfmpt1 4899 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑥𝐴𝐶)
2015, 200nfcxfr 2900 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐺
202201, 164nffv 6360 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣)
203165, 199, 202nfov 6840 . . . . . . . . . . . . . . . . . 18 𝑥((𝐹𝑣) / (𝐺𝑣))
204198, 203nfeq 2914 . . . . . . . . . . . . . . . . 17 𝑥(𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))
205161, 204nfim 1974 . . . . . . . . . . . . . . . 16 𝑥((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
206 fveq2 6353 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (𝐻𝑥) = (𝐻𝑣))
207 fveq2 6353 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → (𝐺𝑥) = (𝐺𝑣))
208170, 207oveq12d 6832 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → ((𝐹𝑥) / (𝐺𝑥)) = ((𝐹𝑣) / (𝐺𝑣)))
209206, 208eqeq12d 2775 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → ((𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)) ↔ (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))))
210169, 209imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥))) ↔ ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))))
211192fvmpt2 6454 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻𝑥) = (𝐵 / 𝐶))
212173, 191, 211syl2anc 696 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐻𝑥) = (𝐵 / 𝐶))
213175eqcomd 2766 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵 = (𝐹𝑥))
2145fvmpt2 6454 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐶 ∈ (ℂ ∖ {0})) → (𝐺𝑥) = 𝐶)
215173, 3, 214syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐺𝑥) = 𝐶)
216215eqcomd 2766 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐶 = (𝐺𝑥))
217213, 216oveq12d 6832 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) = ((𝐹𝑥) / (𝐺𝑥)))
218212, 217eqtrd 2794 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)))
219205, 210, 218chvar 2407 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
220195, 219eqtrd 2794 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = ((𝐹𝑣) / (𝐺𝑣)))
221220fveq2d 6357 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
222187, 188, 221syl2anc 696 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
223 simp-6l 833 . . . . . . . . . . . . . 14 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝜑𝑦 ∈ ℝ+))
224223, 188jca 555 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴))
225 simplr 809 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
226 simpr 479 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
227 nfcv 2902 . . . . . . . . . . . . . . . . . . . 20 𝑥0
228202, 227nfne 3032 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣) ≠ 0
229161, 228nfim 1974 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
230207neeq1d 2991 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐺𝑥) ≠ 0 ↔ (𝐺𝑣) ≠ 0))
231169, 230imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0) ↔ ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)))
232215, 190eqnetrd 2999 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0)
233229, 231, 232chvar 2407 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
234177, 57, 233absdivd 14413 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
235234adantlr 753 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
236235ad2antrr 764 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
237177abscld 14394 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) ∈ ℝ)
23857, 233absne0d 14405 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
239237, 78, 238redivcld 11065 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
240239adantlr 753 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
241240ad2antrr 764 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
242 rpre 12052 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
243242ad2antlr 765 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℝ)
24420rpred 12085 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245244ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246243, 245remulcld 10282 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247246ad2antrr 764 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
24857, 233absrpcld 14406 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
249248adantlr 753 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
250249ad2antrr 764 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
251247, 250rerpdivcld 12116 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) ∈ ℝ)
252243ad2antrr 764 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑦 ∈ ℝ)
253 simp-4l 825 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
254 simpllr 817 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
255253, 254, 237syl2anc 696 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) ∈ ℝ)
256 simpr 479 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
257255, 247, 250, 256ltdiv1dd 12142 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))))
258243recnd 10280 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℂ)
25947ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260249rpcnd 12087 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℂ)
261238adantlr 753 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
262258, 259, 260, 261divassd 11048 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
263262adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
264245, 249rerpdivcld 12116 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
265264adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
266 1red 10267 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ)
267 simpllr 817 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 𝑦 ∈ ℝ+)
268244ad2antrr 764 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269 1rp 12049 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ+
270269a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ+)
271248adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
27247div1d 11005 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273272ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274 simpr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
275273, 274eqbrtrd 4826 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺𝑣)))
276268, 270, 271, 275ltdiv23d 12150 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
277276adantllr 757 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
278265, 266, 267, 277ltmul2dd 12141 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))) < (𝑦 · 1))
279263, 278eqbrtrd 4826 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < (𝑦 · 1))
280258mulid1d 10269 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · 1) = 𝑦)
281280adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · 1) = 𝑦)
282279, 281breqtrd 4830 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
283282adantr 472 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
284241, 251, 252, 257, 283lttrd 10410 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < 𝑦)
285236, 284eqbrtrd 4826 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
286224, 225, 226, 285syl21anc 1476 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
287222, 286eqbrtrd 4826 . . . . . . . . . . 11 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
288128, 150, 186, 287syl21anc 1476 . . . . . . . . . 10 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
2892883exp 1113 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
290121, 289ralrimi 3095 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
291 breq2 4808 . . . . . . . . . . . 12 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → ((abs‘(𝑣𝐸)) < 𝑤 ↔ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)))
292291anbi2d 742 . . . . . . . . . . 11 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) ↔ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))))
293292imbi1d 330 . . . . . . . . . 10 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
294293ralbidv 3124 . . . . . . . . 9 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → (∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦) ↔ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
295294rspcev 3449 . . . . . . . 8 ((if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
296114, 290, 295syl2anc 696 . . . . . . 7 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
297296rexlimdv3a 3171 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → (∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
298111, 297mpd 15 . . . . 5 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
299298rexlimdv3a 3171 . . . 4 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
30089, 299mpd 15 . . 3 ((𝜑𝑦 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
301300ralrimiva 3104 . 2 (𝜑 → ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
302193, 10, 13ellimc3 23862 . 2 (𝜑 → (0 ∈ (𝐻 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))))
3031, 301, 302mpbir2and 995 1 (𝜑 → 0 ∈ (𝐻 lim 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  cdif 3712  wss 3715  ifcif 4230  {csn 4321   class class class wbr 4804  cmpt 4881  dom cdm 5266  wf 6045  cfv 6049  (class class class)co 6814  cc 10146  cr 10147  0cc0 10148  1c1 10149   + caddc 10151   · cmul 10153   < clt 10286  cle 10287  cmin 10478   / cdiv 10896  2c2 11282  +crp 12045  abscabs 14193   lim climc 23845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-er 7913  df-map 8027  df-pm 8028  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-fi 8484  df-sup 8515  df-inf 8516  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295  df-7 11296  df-8 11297  df-9 11298  df-n0 11505  df-z 11590  df-dec 11706  df-uz 11900  df-q 12002  df-rp 12046  df-xneg 12159  df-xadd 12160  df-xmul 12161  df-fz 12540  df-seq 13016  df-exp 13075  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-struct 16081  df-ndx 16082  df-slot 16083  df-base 16085  df-plusg 16176  df-mulr 16177  df-starv 16178  df-tset 16182  df-ple 16183  df-ds 16186  df-unif 16187  df-rest 16305  df-topn 16306  df-topgen 16326  df-psmet 19960  df-xmet 19961  df-met 19962  df-bl 19963  df-mopn 19964  df-cnfld 19969  df-top 20921  df-topon 20938  df-topsp 20959  df-bases 20972  df-cnp 21254  df-xms 22346  df-ms 22347  df-limc 23849
This theorem is referenced by:  reclimc  40406
  Copyright terms: Public domain W3C validator