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

Theorem 0ellimcdiv 42284
 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 10627 . 2 (𝜑 → 0 ∈ ℂ)
2 0ellimcdiv.d . . . . . . . . 9 (𝜑𝐷 ∈ (𝐺 lim 𝐸))
3 0ellimcdiv.c . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
43eldifad 3896 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
5 0ellimcdiv.g . . . . . . . . . . 11 𝐺 = (𝑥𝐴𝐶)
64, 5fmptd 6859 . . . . . . . . . 10 (𝜑𝐺:𝐴⟶ℂ)
7 0ellimcdiv.f . . . . . . . . . . 11 𝐹 = (𝑥𝐴𝐵)
8 0ellimcdiv.b . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
9 0ellimcdiv.0limf . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐸))
107, 8, 9limcmptdm 42270 . . . . . . . . . 10 (𝜑𝐴 ⊆ ℂ)
11 limcrcl 24481 . . . . . . . . . . . 12 (𝐷 ∈ (𝐺 lim 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
122, 11syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
1312simp3d 1141 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
146, 10, 13ellimc3 24486 . . . . . . . . 9 (𝜑 → (𝐷 ∈ (𝐺 lim 𝐸) ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))))
152, 14mpbid 235 . . . . . . . 8 (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦)))
1615simprd 499 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))
1715simpld 498 . . . . . . . . 9 (𝜑𝐷 ∈ ℂ)
18 0ellimcdiv.dne0 . . . . . . . . 9 (𝜑𝐷 ≠ 0)
1917, 18absrpcld 14804 . . . . . . . 8 (𝜑 → (abs‘𝐷) ∈ ℝ+)
2019rphalfcld 12435 . . . . . . 7 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ+)
21 breq2 5037 . . . . . . . . . 10 (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2221imbi2d 344 . . . . . . . . 9 (𝑦 = ((abs‘𝐷) / 2) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2322rexralbidv 3263 . . . . . . . 8 (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2423rspccva 3573 . . . . . . 7 ((∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2516, 20, 24syl2anc 587 . . . . . 6 (𝜑 → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26 simpl1l 1221 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝜑)
27 simpl3 1190 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝑣𝐴)
28 simpr 488 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧))
29 simpl2 1189 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
3027, 28, 29mp2d 49 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
3119rpcnd 12425 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝐷) ∈ ℂ)
32312halvesd 11875 . . . . . . . . . . . . . . 15 (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
3332eqcomd 2807 . . . . . . . . . . . . . 14 (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
3433oveq1d 7154 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35 2cnd 11707 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℂ)
36 2ne0 11733 . . . . . . . . . . . . . . . . 17 2 ≠ 0
3736a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≠ 0)
3817, 35, 37absdivd 14811 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39 2re 11703 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
4039a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ)
41 0le2 11731 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 2)
4340, 42absidd 14778 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘2) = 2)
4443oveq2d 7155 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
4538, 44eqtr2d 2837 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
4645oveq2d 7155 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
4720rpcnd 12425 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
4847, 47pncand 10991 . . . . . . . . . . . . 13 (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
4934, 46, 483eqtr3rd 2845 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50493ad2ant1 1130 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
5145eqcomd 2807 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52513ad2ant1 1130 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
5352oveq2d 7155 . . . . . . . . . . . 12 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
5417adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → 𝐷 ∈ ℂ)
5554abscld 14792 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ∈ ℝ)
56553adant3 1129 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
576ffvelrnda 6832 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ∈ ℂ)
58573adant3 1129 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺𝑣) ∈ ℂ)
5958abscld 14792 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
60173ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
6160, 58subcld 10990 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
6261abscld 14792 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) ∈ ℝ)
6359, 62readdcld 10663 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) ∈ ℝ)
6456rehalfcld 11876 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
6559, 64readdcld 10663 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
6657, 54pncan3d 10993 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → ((𝐺𝑣) + (𝐷 − (𝐺𝑣))) = 𝐷)
6766eqcomd 2807 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → 𝐷 = ((𝐺𝑣) + (𝐷 − (𝐺𝑣))))
6867fveq2d 6653 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘𝐷) = (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))))
6954, 57subcld 10990 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
7057, 69abstrid 14812 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7168, 70eqbrtrd 5055 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
72713adant3 1129 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7360, 58abssubd 14809 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) = (abs‘((𝐺𝑣) − 𝐷)))
74 simp3 1135 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
7573, 74eqbrtrd 5055 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) < ((abs‘𝐷) / 2))
7662, 64, 59, 75ltadd2dd 10792 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7756, 63, 65, 72, 76lelttrd 10791 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7857abscld 14792 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ)
79783adant3 1129 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
8056, 64, 79ltsubaddd 11229 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺𝑣)) ↔ (abs‘𝐷) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2))))
8177, 80mpbird 260 . . . . . . . . . . . 12 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺𝑣)))
8253, 81eqbrtrd 5055 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺𝑣)))
8350, 82eqbrtrd 5055 . . . . . . . . . 10 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
8426, 27, 30, 83syl3anc 1368 . . . . . . . . 9 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
85843exp1 1349 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ+) → ((𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))))
8685ralimdv2 3146 . . . . . . 7 ((𝜑𝑧 ∈ ℝ+) → (∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))))
8786reximdva 3236 . . . . . 6 (𝜑 → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))))
8825, 87mpd 15 . . . . 5 (𝜑 → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
8988adantr 484 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
90 simpr 488 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
9117adantr 484 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐷 ∈ ℂ)
9218adantr 484 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐷 ≠ 0)
9391, 92absrpcld 14804 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (abs‘𝐷) ∈ ℝ+)
9493rphalfcld 12435 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → ((abs‘𝐷) / 2) ∈ ℝ+)
9590, 94rpmulcld 12439 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)
9695ex 416 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℝ+ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9796imdistani 572 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
98 eleq1 2880 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ+ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9998anbi2d 631 . . . . . . . . . 10 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑𝑤 ∈ ℝ+) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)))
100 breq2 5037 . . . . . . . . . . . 12 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((abs‘((𝐹𝑣) − 0)) < 𝑤 ↔ (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
101100imbi2d 344 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
102101rexralbidv 3263 . . . . . . . . . 10 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤) ↔ ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
10399, 102imbi12d 348 . . . . . . . . 9 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝜑𝑤 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤)) ↔ ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))))
1048, 7fmptd 6859 . . . . . . . . . . . . 13 (𝜑𝐹:𝐴⟶ℂ)
105104, 10, 13ellimc3 24486 . . . . . . . . . . . 12 (𝜑 → (0 ∈ (𝐹 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))))
1069, 105mpbid 235 . . . . . . . . . . 11 (𝜑 → (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤)))
107106simprd 499 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
108107r19.21bi 3176 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
109103, 108vtoclg 3518 . . . . . . . 8 ((𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+ → ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
11095, 97, 109sylc 65 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
1111103ad2ant1 1130 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112 simp12 1201 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ+)
113 simp2 1134 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ+)
114112, 113ifcld 4473 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+)
115 nfv 1915 . . . . . . . . . . 11 𝑣(𝜑𝑦 ∈ ℝ+)
116 nfv 1915 . . . . . . . . . . 11 𝑣 𝑧 ∈ ℝ+
117 nfra1 3186 . . . . . . . . . . 11 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
118115, 116, 117nf3an 1902 . . . . . . . . . 10 𝑣((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
119 nfv 1915 . . . . . . . . . 10 𝑣 𝑢 ∈ ℝ+
120 nfra1 3186 . . . . . . . . . 10 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121118, 119, 120nf3an 1902 . . . . . . . . 9 𝑣(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122 simp111 1299 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝜑𝑦 ∈ ℝ+))
123 simp112 1300 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ+)
124 simp12 1201 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ+)
125122, 123, 124jca31 518 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+))
126 simp2 1134 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐴)
127 simp3l 1198 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐸)
128125, 126, 127jca31 518 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸))
12910adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → 𝐴 ⊆ ℂ)
1301293ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐴 ⊆ ℂ)
1311303ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
1321313ad2ant1 1130 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133132, 126sseldd 3919 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
13413adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → 𝐸 ∈ ℂ)
1351343ad2ant1 1130 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐸 ∈ ℂ)
1361353ad2ant1 1130 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
1371363ad2ant1 1130 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138133, 137subcld 10990 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝑣𝐸) ∈ ℂ)
139138abscld 14792 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) ∈ ℝ)
140123rpred 12423 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141124rpred 12423 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142140, 141ifcld 4473 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ)
143 simp3r 1199 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))
144 min1 12574 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
145140, 141, 144syl2anc 587 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
146139, 142, 140, 143, 145ltletrd 10793 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < 𝑧)
147 simp113 1301 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
148 rspa 3174 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
149147, 126, 148syl2anc 587 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
150127, 146, 149mp2and 698 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
151 simp13 1202 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152 rspa 3174 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153151, 126, 152syl2anc 587 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154 min2 12575 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
155140, 141, 154syl2anc 587 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
156139, 142, 141, 143, 155ltletrd 10793 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < 𝑢)
157127, 156jca 515 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢))
158122simpld 498 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝜑)
1591583ad2ant1 1130 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝜑)
160 simp12 1201 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝑣𝐴)
161 nfv 1915 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑣𝐴)
162 nfmpt1 5131 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
1637, 162nfcxfr 2956 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
164 nfcv 2958 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑣
165163, 164nffv 6659 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝐹𝑣)
166165nfel1 2974 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐹𝑣) ∈ ℂ
167161, 166nfim 1897 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
168 eleq1 2880 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝑥𝐴𝑣𝐴))
169168anbi2d 631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝜑𝑥𝐴) ↔ (𝜑𝑣𝐴)))
170 fveq2 6649 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
171170eleq1d 2877 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐹𝑥) ∈ ℂ ↔ (𝐹𝑣) ∈ ℂ))
172169, 171imbi12d 348 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ) ↔ ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)))
173 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → 𝑥𝐴)
1747fvmpt2 6760 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐵 ∈ ℂ) → (𝐹𝑥) = 𝐵)
175173, 8, 174syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
176175, 8eqeltrd 2893 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ)
177167, 172, 176chvarfv 2241 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
178177subid1d 10979 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → ((𝐹𝑣) − 0) = (𝐹𝑣))
179178eqcomd 2807 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐹𝑣) = ((𝐹𝑣) − 0))
180179fveq2d 6653 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
181159, 160, 180syl2anc 587 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
182 simp3 1135 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢))
183 simp2 1134 . . . . . . . . . . . . . 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 5055 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
186153, 157, 185mpd3an23 1460 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
187 simp-7l 788 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
188 simp-4r 783 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
189 eldifsni 4686 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
1903, 189syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝐶 ≠ 0)
1918, 4, 190divcld 11409 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192 0ellimcdiv.h . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥𝐴 ↦ (𝐵 / 𝐶))
193191, 192fmptd 6859 . . . . . . . . . . . . . . . . 17 (𝜑𝐻:𝐴⟶ℂ)
194193ffvelrnda 6832 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (𝐻𝑣) ∈ ℂ)
195194subid1d 10979 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = (𝐻𝑣))
196 nfmpt1 5131 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥𝐴 ↦ (𝐵 / 𝐶))
197192, 196nfcxfr 2956 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
198197, 164nffv 6659 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑣)
199 nfcv 2958 . . . . . . . . . . . . . . . . . . 19 𝑥 /
200 nfmpt1 5131 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑥𝐴𝐶)
2015, 200nfcxfr 2956 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐺
202201, 164nffv 6659 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣)
203165, 199, 202nfov 7169 . . . . . . . . . . . . . . . . . 18 𝑥((𝐹𝑣) / (𝐺𝑣))
204198, 203nfeq 2971 . . . . . . . . . . . . . . . . 17 𝑥(𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))
205161, 204nfim 1897 . . . . . . . . . . . . . . . 16 𝑥((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
206 fveq2 6649 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (𝐻𝑥) = (𝐻𝑣))
207 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → (𝐺𝑥) = (𝐺𝑣))
208170, 207oveq12d 7157 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → ((𝐹𝑥) / (𝐺𝑥)) = ((𝐹𝑣) / (𝐺𝑣)))
209206, 208eqeq12d 2817 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → ((𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)) ↔ (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))))
210169, 209imbi12d 348 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥))) ↔ ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))))
211192fvmpt2 6760 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻𝑥) = (𝐵 / 𝐶))
212173, 191, 211syl2anc 587 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐻𝑥) = (𝐵 / 𝐶))
213175eqcomd 2807 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵 = (𝐹𝑥))
2145fvmpt2 6760 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐶 ∈ (ℂ ∖ {0})) → (𝐺𝑥) = 𝐶)
215173, 3, 214syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐺𝑥) = 𝐶)
216215eqcomd 2807 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐶 = (𝐺𝑥))
217213, 216oveq12d 7157 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) = ((𝐹𝑥) / (𝐺𝑥)))
218212, 217eqtrd 2836 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)))
219205, 210, 218chvarfv 2241 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
220195, 219eqtrd 2836 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = ((𝐹𝑣) / (𝐺𝑣)))
221220fveq2d 6653 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
222187, 188, 221syl2anc 587 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
223 simp-6l 786 . . . . . . . . . . . . . 14 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝜑𝑦 ∈ ℝ+))
224223, 188jca 515 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴))
225 simplr 768 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
226 simpr 488 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
227 nfcv 2958 . . . . . . . . . . . . . . . . . . . 20 𝑥0
228202, 227nfne 3090 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣) ≠ 0
229161, 228nfim 1897 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
230207neeq1d 3049 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐺𝑥) ≠ 0 ↔ (𝐺𝑣) ≠ 0))
231169, 230imbi12d 348 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0) ↔ ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)))
232215, 190eqnetrd 3057 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0)
233229, 231, 232chvarfv 2241 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
234177, 57, 233absdivd 14811 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
235234adantlr 714 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
236235ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
237177abscld 14792 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) ∈ ℝ)
23857, 233absne0d 14803 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
239237, 78, 238redivcld 11461 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
240239adantlr 714 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
241240ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
242 rpre 12389 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
243242ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℝ)
24420rpred 12423 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245244ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246243, 245remulcld 10664 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247246ad2antrr 725 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
24857, 233absrpcld 14804 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
249248adantlr 714 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
250249ad2antrr 725 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
251247, 250rerpdivcld 12454 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) ∈ ℝ)
252243ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑦 ∈ ℝ)
253 simp-4l 782 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
254 simpllr 775 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
255253, 254, 237syl2anc 587 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) ∈ ℝ)
256 simpr 488 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
257255, 247, 250, 256ltdiv1dd 12480 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))))
258243recnd 10662 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℂ)
25947ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260249rpcnd 12425 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℂ)
261238adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
262258, 259, 260, 261divassd 11444 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
263262adantr 484 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
264245, 249rerpdivcld 12454 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
265264adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
266 1red 10635 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ)
267 simpllr 775 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 𝑦 ∈ ℝ+)
268244ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269 1rp 12385 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ+
270269a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ+)
271248adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
27247div1d 11401 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273272ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274 simpr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
275273, 274eqbrtrd 5055 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺𝑣)))
276268, 270, 271, 275ltdiv23d 12490 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
277276adantllr 718 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
278265, 266, 267, 277ltmul2dd 12479 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))) < (𝑦 · 1))
279263, 278eqbrtrd 5055 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < (𝑦 · 1))
280258mulid1d 10651 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · 1) = 𝑦)
281280adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · 1) = 𝑦)
282279, 281breqtrd 5059 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
283282adantr 484 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
284241, 251, 252, 257, 283lttrd 10794 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < 𝑦)
285236, 284eqbrtrd 5055 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
286224, 225, 226, 285syl21anc 836 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
287222, 286eqbrtrd 5055 . . . . . . . . . . 11 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
288128, 150, 186, 287syl21anc 836 . . . . . . . . . 10 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
2892883exp 1116 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
290121, 289ralrimi 3183 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
291 brimralrspcev 5094 . . . . . . . 8 ((if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
292114, 290, 291syl2anc 587 . . . . . . 7 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
293292rexlimdv3a 3248 . . . . . 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 3248 . . . 4 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
29689, 295mpd 15 . . 3 ((𝜑𝑦 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
297296ralrimiva 3152 . 2 (𝜑 → ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
298193, 10, 13ellimc3 24486 . 2 (𝜑 → (0 ∈ (𝐻 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))))
2991, 297, 298mpbir2and 712 1 (𝜑 → 0 ∈ (𝐻 lim 𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112   ≠ wne 2990  ∀wral 3109  ∃wrex 3110   ∖ cdif 3881   ⊆ wss 3884  ifcif 4428  {csn 4528   class class class wbr 5033   ↦ cmpt 5113  dom cdm 5523  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139  ℂcc 10528  ℝcr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535   < clt 10668   ≤ cle 10669   − cmin 10863   / cdiv 11290  2c2 11684  ℝ+crp 12381  abscabs 14589   limℂ climc 24469 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fi 8863  df-sup 8894  df-inf 8895  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-fz 12890  df-seq 13369  df-exp 13430  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-plusg 16574  df-mulr 16575  df-starv 16576  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-rest 16692  df-topn 16693  df-topgen 16713  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-cnfld 20096  df-top 21503  df-topon 21520  df-topsp 21542  df-bases 21555  df-cnp 21837  df-xms 22931  df-ms 22932  df-limc 24473 This theorem is referenced by:  reclimc  42288
 Copyright terms: Public domain W3C validator