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 40199
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 10071 . 2 (𝜑 → 0 ∈ ℂ)
2 0ellimcdiv.d . . . . . . . . 9 (𝜑𝐷 ∈ (𝐺 lim 𝐸))
3 0ellimcdiv.c . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
43eldifad 3619 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
5 0ellimcdiv.g . . . . . . . . . . 11 𝐺 = (𝑥𝐴𝐶)
64, 5fmptd 6425 . . . . . . . . . 10 (𝜑𝐺:𝐴⟶ℂ)
7 0ellimcdiv.f . . . . . . . . . . 11 𝐹 = (𝑥𝐴𝐵)
8 0ellimcdiv.b . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
9 0ellimcdiv.0limf . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐸))
107, 8, 9limcmptdm 40185 . . . . . . . . . 10 (𝜑𝐴 ⊆ ℂ)
11 limcrcl 23683 . . . . . . . . . . . 12 (𝐷 ∈ (𝐺 lim 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
122, 11syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
1312simp3d 1095 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
146, 10, 13ellimc3 23688 . . . . . . . . 9 (𝜑 → (𝐷 ∈ (𝐺 lim 𝐸) ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))))
152, 14mpbid 222 . . . . . . . 8 (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦)))
1615simprd 478 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))
1715simpld 474 . . . . . . . . 9 (𝜑𝐷 ∈ ℂ)
18 0ellimcdiv.dne0 . . . . . . . . 9 (𝜑𝐷 ≠ 0)
1917, 18absrpcld 14231 . . . . . . . 8 (𝜑 → (abs‘𝐷) ∈ ℝ+)
2019rphalfcld 11922 . . . . . . 7 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ+)
21 breq2 4689 . . . . . . . . . 10 (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2221imbi2d 329 . . . . . . . . 9 (𝑦 = ((abs‘𝐷) / 2) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2322rexralbidv 3087 . . . . . . . 8 (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2423rspccva 3339 . . . . . . 7 ((∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2516, 20, 24syl2anc 694 . . . . . 6 (𝜑 → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26 simpl1l 1132 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝜑)
27 simpl3 1086 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝑣𝐴)
28 simpr 476 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧))
29 simpl2 1085 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
3027, 28, 29mp2d 49 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
3119rpcnd 11912 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝐷) ∈ ℂ)
32312halvesd 11316 . . . . . . . . . . . . . . 15 (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
3332eqcomd 2657 . . . . . . . . . . . . . 14 (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
3433oveq1d 6705 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35 2cnd 11131 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℂ)
36 2ne0 11151 . . . . . . . . . . . . . . . . 17 2 ≠ 0
3736a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≠ 0)
3817, 35, 37absdivd 14238 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39 2re 11128 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
4039a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ)
41 0le2 11149 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 2)
4340, 42absidd 14205 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘2) = 2)
4443oveq2d 6706 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
4538, 44eqtr2d 2686 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
4645oveq2d 6706 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
4720rpcnd 11912 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
4847, 47pncand 10431 . . . . . . . . . . . . 13 (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
4934, 46, 483eqtr3rd 2694 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50493ad2ant1 1102 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
5145eqcomd 2657 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52513ad2ant1 1102 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
5352oveq2d 6706 . . . . . . . . . . . 12 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
5417adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → 𝐷 ∈ ℂ)
5554abscld 14219 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ∈ ℝ)
56553adant3 1101 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
576ffvelrnda 6399 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ∈ ℂ)
58573adant3 1101 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺𝑣) ∈ ℂ)
5958abscld 14219 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
60173ad2ant1 1102 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
6160, 58subcld 10430 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
6261abscld 14219 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) ∈ ℝ)
6359, 62readdcld 10107 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) ∈ ℝ)
6456rehalfcld 11317 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
6559, 64readdcld 10107 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
6657, 54pncan3d 10433 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → ((𝐺𝑣) + (𝐷 − (𝐺𝑣))) = 𝐷)
6766eqcomd 2657 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → 𝐷 = ((𝐺𝑣) + (𝐷 − (𝐺𝑣))))
6867fveq2d 6233 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘𝐷) = (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))))
6954, 57subcld 10430 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
7057, 69abstrid 14239 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7168, 70eqbrtrd 4707 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
72713adant3 1101 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7360, 58abssubd 14236 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) = (abs‘((𝐺𝑣) − 𝐷)))
74 simp3 1083 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
7573, 74eqbrtrd 4707 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) < ((abs‘𝐷) / 2))
7662, 64, 59, 75ltadd2dd 10234 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7756, 63, 65, 72, 76lelttrd 10233 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7857abscld 14219 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ)
79783adant3 1101 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
8056, 64, 79ltsubaddd 10661 . . . . . . . . . . . . 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 4707 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺𝑣)))
8350, 82eqbrtrd 4707 . . . . . . . . . 10 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
8426, 27, 30, 83syl3anc 1366 . . . . . . . . 9 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
85843exp1 1305 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ+) → ((𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))))
8685ralimdv2 2990 . . . . . . 7 ((𝜑𝑧 ∈ ℝ+) → (∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))))
8786reximdva 3046 . . . . . 6 (𝜑 → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))))
8825, 87mpd 15 . . . . 5 (𝜑 → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
8988adantr 480 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
90 simpr 476 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
9117adantr 480 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐷 ∈ ℂ)
9218adantr 480 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐷 ≠ 0)
9391, 92absrpcld 14231 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (abs‘𝐷) ∈ ℝ+)
9493rphalfcld 11922 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → ((abs‘𝐷) / 2) ∈ ℝ+)
9590, 94rpmulcld 11926 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)
9695ex 449 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℝ+ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9796imdistani 726 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
98 eleq1 2718 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ+ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9998anbi2d 740 . . . . . . . . . 10 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑𝑤 ∈ ℝ+) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)))
100 breq2 4689 . . . . . . . . . . . 12 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((abs‘((𝐹𝑣) − 0)) < 𝑤 ↔ (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
101100imbi2d 329 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
102101rexralbidv 3087 . . . . . . . . . 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 6425 . . . . . . . . . . . . 13 (𝜑𝐹:𝐴⟶ℂ)
105104, 10, 13ellimc3 23688 . . . . . . . . . . . 12 (𝜑 → (0 ∈ (𝐹 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))))
1069, 105mpbid 222 . . . . . . . . . . 11 (𝜑 → (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤)))
107106simprd 478 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
108107r19.21bi 2961 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
109103, 108vtoclg 3297 . . . . . . . 8 ((𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+ → ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
11095, 97, 109sylc 65 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
1111103ad2ant1 1102 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112 simp12 1112 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ+)
113 simp2 1082 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ+)
114112, 113ifcld 4164 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+)
115 nfv 1883 . . . . . . . . . . 11 𝑣(𝜑𝑦 ∈ ℝ+)
116 nfv 1883 . . . . . . . . . . 11 𝑣 𝑧 ∈ ℝ+
117 nfra1 2970 . . . . . . . . . . 11 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
118115, 116, 117nf3an 1871 . . . . . . . . . 10 𝑣((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
119 nfv 1883 . . . . . . . . . 10 𝑣 𝑢 ∈ ℝ+
120 nfra1 2970 . . . . . . . . . 10 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121118, 119, 120nf3an 1871 . . . . . . . . 9 𝑣(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122 simp111 1210 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝜑𝑦 ∈ ℝ+))
123 simp112 1211 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ+)
124 simp12 1112 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ+)
125122, 123, 124jca31 556 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+))
126 simp2 1082 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐴)
127 simp3l 1109 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐸)
128125, 126, 127jca31 556 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸))
12910adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → 𝐴 ⊆ ℂ)
1301293ad2ant1 1102 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐴 ⊆ ℂ)
1311303ad2ant1 1102 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
1321313ad2ant1 1102 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133132, 126sseldd 3637 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
13413adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → 𝐸 ∈ ℂ)
1351343ad2ant1 1102 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐸 ∈ ℂ)
1361353ad2ant1 1102 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
1371363ad2ant1 1102 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138133, 137subcld 10430 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝑣𝐸) ∈ ℂ)
139138abscld 14219 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) ∈ ℝ)
140123rpred 11910 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141124rpred 11910 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142140, 141ifcld 4164 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ)
143 simp3r 1110 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))
144 min1 12058 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
145140, 141, 144syl2anc 694 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
146139, 142, 140, 143, 145ltletrd 10235 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < 𝑧)
147 simp113 1212 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
148 rspa 2959 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
149147, 126, 148syl2anc 694 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
150127, 146, 149mp2and 715 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
151 simp13 1113 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152 rspa 2959 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153151, 126, 152syl2anc 694 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154 min2 12059 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
155140, 141, 154syl2anc 694 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
156139, 142, 141, 143, 155ltletrd 10235 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < 𝑢)
157127, 156jca 553 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢))
158122simpld 474 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝜑)
1591583ad2ant1 1102 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝜑)
160 simp12 1112 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝑣𝐴)
161 nfv 1883 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑣𝐴)
162 nfmpt1 4780 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
1637, 162nfcxfr 2791 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
164 nfcv 2793 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑣
165163, 164nffv 6236 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝐹𝑣)
166165nfel1 2808 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐹𝑣) ∈ ℂ
167161, 166nfim 1865 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
168 eleq1 2718 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝑥𝐴𝑣𝐴))
169168anbi2d 740 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝜑𝑥𝐴) ↔ (𝜑𝑣𝐴)))
170 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
171170eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐹𝑥) ∈ ℂ ↔ (𝐹𝑣) ∈ ℂ))
172169, 171imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ) ↔ ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)))
173 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → 𝑥𝐴)
1747fvmpt2 6330 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐵 ∈ ℂ) → (𝐹𝑥) = 𝐵)
175173, 8, 174syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
176175, 8eqeltrd 2730 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ)
177167, 172, 176chvar 2298 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
178177subid1d 10419 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → ((𝐹𝑣) − 0) = (𝐹𝑣))
179178eqcomd 2657 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐹𝑣) = ((𝐹𝑣) − 0))
180179fveq2d 6233 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
181159, 160, 180syl2anc 694 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
182 simp3 1083 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢))
183 simp2 1082 . . . . . . . . . . . . . 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 4707 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
186153, 157, 185mpd3an23 1466 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
187 simp-7l 829 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
188 simp-4r 824 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
189 eldifsni 4353 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
1903, 189syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝐶 ≠ 0)
1918, 4, 190divcld 10839 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192 0ellimcdiv.h . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥𝐴 ↦ (𝐵 / 𝐶))
193191, 192fmptd 6425 . . . . . . . . . . . . . . . . 17 (𝜑𝐻:𝐴⟶ℂ)
194193ffvelrnda 6399 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (𝐻𝑣) ∈ ℂ)
195194subid1d 10419 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = (𝐻𝑣))
196 nfmpt1 4780 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥𝐴 ↦ (𝐵 / 𝐶))
197192, 196nfcxfr 2791 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
198197, 164nffv 6236 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑣)
199 nfcv 2793 . . . . . . . . . . . . . . . . . . 19 𝑥 /
200 nfmpt1 4780 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑥𝐴𝐶)
2015, 200nfcxfr 2791 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐺
202201, 164nffv 6236 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣)
203165, 199, 202nfov 6716 . . . . . . . . . . . . . . . . . 18 𝑥((𝐹𝑣) / (𝐺𝑣))
204198, 203nfeq 2805 . . . . . . . . . . . . . . . . 17 𝑥(𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))
205161, 204nfim 1865 . . . . . . . . . . . . . . . 16 𝑥((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
206 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (𝐻𝑥) = (𝐻𝑣))
207 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → (𝐺𝑥) = (𝐺𝑣))
208170, 207oveq12d 6708 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → ((𝐹𝑥) / (𝐺𝑥)) = ((𝐹𝑣) / (𝐺𝑣)))
209206, 208eqeq12d 2666 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → ((𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)) ↔ (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))))
210169, 209imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥))) ↔ ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))))
211192fvmpt2 6330 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻𝑥) = (𝐵 / 𝐶))
212173, 191, 211syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐻𝑥) = (𝐵 / 𝐶))
213175eqcomd 2657 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵 = (𝐹𝑥))
2145fvmpt2 6330 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐶 ∈ (ℂ ∖ {0})) → (𝐺𝑥) = 𝐶)
215173, 3, 214syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐺𝑥) = 𝐶)
216215eqcomd 2657 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐶 = (𝐺𝑥))
217213, 216oveq12d 6708 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) = ((𝐹𝑥) / (𝐺𝑥)))
218212, 217eqtrd 2685 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)))
219205, 210, 218chvar 2298 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
220195, 219eqtrd 2685 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = ((𝐹𝑣) / (𝐺𝑣)))
221220fveq2d 6233 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
222187, 188, 221syl2anc 694 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
223 simp-6l 827 . . . . . . . . . . . . . 14 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝜑𝑦 ∈ ℝ+))
224223, 188jca 553 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴))
225 simplr 807 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
226 simpr 476 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
227 nfcv 2793 . . . . . . . . . . . . . . . . . . . 20 𝑥0
228202, 227nfne 2923 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣) ≠ 0
229161, 228nfim 1865 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
230207neeq1d 2882 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐺𝑥) ≠ 0 ↔ (𝐺𝑣) ≠ 0))
231169, 230imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0) ↔ ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)))
232215, 190eqnetrd 2890 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0)
233229, 231, 232chvar 2298 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
234177, 57, 233absdivd 14238 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
235234adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
236235ad2antrr 762 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
237177abscld 14219 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) ∈ ℝ)
23857, 233absne0d 14230 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
239237, 78, 238redivcld 10891 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
240239adantlr 751 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
241240ad2antrr 762 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
242 rpre 11877 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
243242ad2antlr 763 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℝ)
24420rpred 11910 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245244ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246243, 245remulcld 10108 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247246ad2antrr 762 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
24857, 233absrpcld 14231 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
249248adantlr 751 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
250249ad2antrr 762 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
251247, 250rerpdivcld 11941 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) ∈ ℝ)
252243ad2antrr 762 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑦 ∈ ℝ)
253 simp-4l 823 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
254 simpllr 815 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
255253, 254, 237syl2anc 694 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) ∈ ℝ)
256 simpr 476 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
257255, 247, 250, 256ltdiv1dd 11967 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))))
258243recnd 10106 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℂ)
25947ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260249rpcnd 11912 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℂ)
261238adantlr 751 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
262258, 259, 260, 261divassd 10874 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
263262adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
264245, 249rerpdivcld 11941 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
265264adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
266 1red 10093 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ)
267 simpllr 815 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 𝑦 ∈ ℝ+)
268244ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269 1rp 11874 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ+
270269a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ+)
271248adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
27247div1d 10831 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273272ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
275273, 274eqbrtrd 4707 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺𝑣)))
276268, 270, 271, 275ltdiv23d 11975 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
277276adantllr 755 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
278265, 266, 267, 277ltmul2dd 11966 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))) < (𝑦 · 1))
279263, 278eqbrtrd 4707 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < (𝑦 · 1))
280258mulid1d 10095 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · 1) = 𝑦)
281280adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · 1) = 𝑦)
282279, 281breqtrd 4711 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
283282adantr 480 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
284241, 251, 252, 257, 283lttrd 10236 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < 𝑦)
285236, 284eqbrtrd 4707 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
286224, 225, 226, 285syl21anc 1365 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
287222, 286eqbrtrd 4707 . . . . . . . . . . 11 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
288128, 150, 186, 287syl21anc 1365 . . . . . . . . . 10 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
2892883exp 1283 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
290121, 289ralrimi 2986 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
291 breq2 4689 . . . . . . . . . . . 12 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → ((abs‘(𝑣𝐸)) < 𝑤 ↔ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)))
292291anbi2d 740 . . . . . . . . . . 11 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) ↔ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))))
293292imbi1d 330 . . . . . . . . . 10 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
294293ralbidv 3015 . . . . . . . . 9 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → (∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦) ↔ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
295294rspcev 3340 . . . . . . . 8 ((if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
296114, 290, 295syl2anc 694 . . . . . . 7 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
297296rexlimdv3a 3062 . . . . . 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 3062 . . . 4 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
30089, 299mpd 15 . . 3 ((𝜑𝑦 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
301300ralrimiva 2995 . 2 (𝜑 → ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
302193, 10, 13ellimc3 23688 . 2 (𝜑 → (0 ∈ (𝐻 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))))
3031, 301, 302mpbir2and 977 1 (𝜑 → 0 ∈ (𝐻 lim 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  cdif 3604  wss 3607  ifcif 4119  {csn 4210   class class class wbr 4685  cmpt 4762  dom cdm 5143  wf 5922  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  2c2 11108  +crp 11870  abscabs 14018   lim climc 23671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-fz 12365  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-plusg 16001  df-mulr 16002  df-starv 16003  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-rest 16130  df-topn 16131  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cnp 21080  df-xms 22172  df-ms 22173  df-limc 23675
This theorem is referenced by:  reclimc  40203
  Copyright terms: Public domain W3C validator