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

Theorem 0ellimcdiv 38716
 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 9912 . 2 (𝜑 → 0 ∈ ℂ)
2 0ellimcdiv.d . . . . . . . . 9 (𝜑𝐷 ∈ (𝐺 lim 𝐸))
3 0ellimcdiv.c . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
43eldifad 3552 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
5 0ellimcdiv.g . . . . . . . . . . 11 𝐺 = (𝑥𝐴𝐶)
64, 5fmptd 6292 . . . . . . . . . 10 (𝜑𝐺:𝐴⟶ℂ)
7 0ellimcdiv.f . . . . . . . . . . 11 𝐹 = (𝑥𝐴𝐵)
8 0ellimcdiv.b . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
9 0ellimcdiv.0limf . . . . . . . . . . 11 (𝜑 → 0 ∈ (𝐹 lim 𝐸))
107, 8, 9limcmptdm 38702 . . . . . . . . . 10 (𝜑𝐴 ⊆ ℂ)
11 limcrcl 23444 . . . . . . . . . . . 12 (𝐷 ∈ (𝐺 lim 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
122, 11syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
1312simp3d 1068 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
146, 10, 13ellimc3 23449 . . . . . . . . 9 (𝜑 → (𝐷 ∈ (𝐺 lim 𝐸) ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))))
152, 14mpbid 221 . . . . . . . 8 (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦)))
1615simprd 478 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦))
1715simpld 474 . . . . . . . . 9 (𝜑𝐷 ∈ ℂ)
18 0ellimcdiv.dne0 . . . . . . . . 9 (𝜑𝐷 ≠ 0)
1917, 18absrpcld 14035 . . . . . . . 8 (𝜑 → (abs‘𝐷) ∈ ℝ+)
2019rphalfcld 11760 . . . . . . 7 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ+)
21 breq2 4587 . . . . . . . . . 10 (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2221imbi2d 329 . . . . . . . . 9 (𝑦 = ((abs‘𝐷) / 2) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2322rexralbidv 3040 . . . . . . . 8 (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
2423rspccva 3281 . . . . . . 7 ((∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
2516, 20, 24syl2anc 691 . . . . . 6 (𝜑 → ∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26 simpl1l 1105 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝜑)
27 simpl3 1059 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → 𝑣𝐴)
28 simpr 476 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧))
29 simpl2 1058 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
3027, 28, 29mp2d 47 . . . . . . . . . 10 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
3119rpcnd 11750 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝐷) ∈ ℂ)
32312halvesd 11155 . . . . . . . . . . . . . . 15 (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
3332eqcomd 2616 . . . . . . . . . . . . . 14 (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
3433oveq1d 6564 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35 2cnd 10970 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℂ)
36 2ne0 10990 . . . . . . . . . . . . . . . . 17 2 ≠ 0
3736a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≠ 0)
3817, 35, 37absdivd 14042 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39 2re 10967 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
4039a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ)
41 0le2 10988 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
4241a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 2)
4340, 42absidd 14009 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘2) = 2)
4443oveq2d 6565 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
4538, 44eqtr2d 2645 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
4645oveq2d 6565 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
4720rpcnd 11750 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
4847, 47pncand 10272 . . . . . . . . . . . . 13 (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
4934, 46, 483eqtr3rd 2653 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50493ad2ant1 1075 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
5145eqcomd 2616 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52513ad2ant1 1075 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
5352oveq2d 6565 . . . . . . . . . . . 12 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
5417adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → 𝐷 ∈ ℂ)
5554abscld 14023 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ∈ ℝ)
56553adant3 1074 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
576ffvelrnda 6267 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ∈ ℂ)
58573adant3 1074 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺𝑣) ∈ ℂ)
5958abscld 14023 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
60173ad2ant1 1075 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
6160, 58subcld 10271 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
6261abscld 14023 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) ∈ ℝ)
6359, 62readdcld 9948 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) ∈ ℝ)
6456rehalfcld 11156 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
6559, 64readdcld 9948 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
6657, 54pncan3d 10274 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → ((𝐺𝑣) + (𝐷 − (𝐺𝑣))) = 𝐷)
6766eqcomd 2616 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → 𝐷 = ((𝐺𝑣) + (𝐷 − (𝐺𝑣))))
6867fveq2d 6107 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘𝐷) = (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))))
6954, 57subcld 10271 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐷 − (𝐺𝑣)) ∈ ℂ)
7057, 69abstrid 14043 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐺𝑣) + (𝐷 − (𝐺𝑣)))) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7168, 70eqbrtrd 4605 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
72713adant3 1074 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))))
7360, 58abssubd 14040 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) = (abs‘((𝐺𝑣) − 𝐷)))
74 simp3 1056 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
7573, 74eqbrtrd 4605 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺𝑣))) < ((abs‘𝐷) / 2))
7662, 64, 59, 75ltadd2dd 10075 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺𝑣)) + (abs‘(𝐷 − (𝐺𝑣)))) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7756, 63, 65, 72, 76lelttrd 10074 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2)))
7857abscld 14023 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ)
79783adant3 1074 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺𝑣)) ∈ ℝ)
8056, 64, 79ltsubaddd 10502 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺𝑣)) ↔ (abs‘𝐷) < ((abs‘(𝐺𝑣)) + ((abs‘𝐷) / 2))))
8177, 80mpbird 246 . . . . . . . . . . . 12 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺𝑣)))
8253, 81eqbrtrd 4605 . . . . . . . . . . 11 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺𝑣)))
8350, 82eqbrtrd 4605 . . . . . . . . . 10 ((𝜑𝑣𝐴 ∧ (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
8426, 27, 30, 83syl3anc 1318 . . . . . . . . 9 ((((𝜑𝑧 ∈ ℝ+) ∧ (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
85843exp1 1275 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ+) → ((𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))))
8685ralimdv2 2944 . . . . . . 7 ((𝜑𝑧 ∈ ℝ+) → (∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → (abs‘((𝐺𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))))
8786reximdva 3000 . . . . . 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 14035 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (abs‘𝐷) ∈ ℝ+)
9493rphalfcld 11760 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → ((abs‘𝐷) / 2) ∈ ℝ+)
9590, 94rpmulcld 11764 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)
9695ex 449 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℝ+ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9796imdistani 722 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
98 eleq1 2676 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ+ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+))
9998anbi2d 736 . . . . . . . . . 10 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑𝑤 ∈ ℝ+) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+)))
100 breq2 4587 . . . . . . . . . . . 12 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((abs‘((𝐹𝑣) − 0)) < 𝑤 ↔ (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
101100imbi2d 329 . . . . . . . . . . 11 (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
102101rexralbidv 3040 . . . . . . . . . 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 6292 . . . . . . . . . . . . 13 (𝜑𝐹:𝐴⟶ℂ)
105104, 10, 13ellimc3 23449 . . . . . . . . . . . 12 (𝜑 → (0 ∈ (𝐹 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))))
1069, 105mpbid 221 . . . . . . . . . . 11 (𝜑 → (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤)))
107106simprd 478 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
108107r19.21bi 2916 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < 𝑤))
109103, 108vtoclg 3239 . . . . . . . 8 ((𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+ → ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
11095, 97, 109sylc 63 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
1111103ad2ant1 1075 . . . . . 6 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → ∃𝑢 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112 simp12 1085 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ+)
113 simp2 1055 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ+)
114112, 113ifcld 4081 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+)
115 nfv 1830 . . . . . . . . . . 11 𝑣(𝜑𝑦 ∈ ℝ+)
116 nfv 1830 . . . . . . . . . . 11 𝑣 𝑧 ∈ ℝ+
117 nfra1 2925 . . . . . . . . . . 11 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
118115, 116, 117nf3an 1819 . . . . . . . . . 10 𝑣((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
119 nfv 1830 . . . . . . . . . 10 𝑣 𝑢 ∈ ℝ+
120 nfra1 2925 . . . . . . . . . 10 𝑣𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121118, 119, 120nf3an 1819 . . . . . . . . 9 𝑣(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122 simp111 1183 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝜑𝑦 ∈ ℝ+))
123 simp112 1184 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ+)
124 simp12 1085 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ+)
125122, 123, 124jca31 555 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+))
126 simp2 1055 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐴)
127 simp3l 1082 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣𝐸)
128125, 126, 127jca31 555 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸))
12910adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → 𝐴 ⊆ ℂ)
1301293ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐴 ⊆ ℂ)
1311303ad2ant1 1075 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
1321313ad2ant1 1075 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133132, 126sseldd 3569 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
13413adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → 𝐸 ∈ ℂ)
1351343ad2ant1 1075 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) → 𝐸 ∈ ℂ)
1361353ad2ant1 1075 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
1371363ad2ant1 1075 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138133, 137subcld 10271 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (𝑣𝐸) ∈ ℂ)
139138abscld 14023 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) ∈ ℝ)
140123rpred 11748 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141124rpred 11748 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142140, 141ifcld 4081 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ)
143 simp3r 1083 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))
144 min1 11894 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
145140, 141, 144syl2anc 691 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑧)
146139, 142, 140, 143, 145ltletrd 10076 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝑣𝐸)) < 𝑧)
147 simp113 1185 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
148 rspa 2914 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
149147, 126, 148syl2anc 691 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))))
150127, 146, 149mp2and 711 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
151 simp13 1086 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152 rspa 2914 . . . . . . . . . . . . 13 ((∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣𝐴) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153151, 126, 152syl2anc 691 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154 min2 11895 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
155140, 141, 154syl2anc 691 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → if(𝑧𝑢, 𝑧, 𝑢) ≤ 𝑢)
156139, 142, 141, 143, 155ltletrd 10076 . . . . . . . . . . . . 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 1075 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝜑)
160 simp12 1085 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → 𝑣𝐴)
161 nfv 1830 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑣𝐴)
162 nfmpt1 4675 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
1637, 162nfcxfr 2749 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝐹
164 nfcv 2751 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑣
165163, 164nffv 6110 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝐹𝑣)
166165nfel1 2765 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐹𝑣) ∈ ℂ
167161, 166nfim 1813 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
168 eleq1 2676 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝑥𝐴𝑣𝐴))
169168anbi2d 736 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝜑𝑥𝐴) ↔ (𝜑𝑣𝐴)))
170 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
171170eleq1d 2672 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐹𝑥) ∈ ℂ ↔ (𝐹𝑣) ∈ ℂ))
172169, 171imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ) ↔ ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)))
173 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → 𝑥𝐴)
1747fvmpt2 6200 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐵 ∈ ℂ) → (𝐹𝑥) = 𝐵)
175173, 8, 174syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
176175, 8eqeltrd 2688 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ)
177167, 172, 176chvar 2250 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐹𝑣) ∈ ℂ)
178177subid1d 10260 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → ((𝐹𝑣) − 0) = (𝐹𝑣))
179178eqcomd 2616 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐹𝑣) = ((𝐹𝑣) − 0))
180179fveq2d 6107 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
181159, 160, 180syl2anc 691 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) = (abs‘((𝐹𝑣) − 0)))
182 simp3 1056 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢))
183 simp2 1055 . . . . . . . . . . . . . 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 4605 . . . . . . . . . . . 12 ((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) ∧ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢)) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
186153, 157, 185mpd3an23 1418 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
187 simp-7l 808 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
188 simp-4r 803 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
189 eldifsni 4261 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
1903, 189syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝐶 ≠ 0)
1918, 4, 190divcld 10680 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192 0ellimcdiv.h . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥𝐴 ↦ (𝐵 / 𝐶))
193191, 192fmptd 6292 . . . . . . . . . . . . . . . . 17 (𝜑𝐻:𝐴⟶ℂ)
194193ffvelrnda 6267 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (𝐻𝑣) ∈ ℂ)
195194subid1d 10260 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = (𝐻𝑣))
196 nfmpt1 4675 . . . . . . . . . . . . . . . . . . . 20 𝑥(𝑥𝐴 ↦ (𝐵 / 𝐶))
197192, 196nfcxfr 2749 . . . . . . . . . . . . . . . . . . 19 𝑥𝐻
198197, 164nffv 6110 . . . . . . . . . . . . . . . . . 18 𝑥(𝐻𝑣)
199 nfcv 2751 . . . . . . . . . . . . . . . . . . 19 𝑥 /
200 nfmpt1 4675 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑥𝐴𝐶)
2015, 200nfcxfr 2749 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐺
202201, 164nffv 6110 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣)
203165, 199, 202nfov 6575 . . . . . . . . . . . . . . . . . 18 𝑥((𝐹𝑣) / (𝐺𝑣))
204198, 203nfeq 2762 . . . . . . . . . . . . . . . . 17 𝑥(𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))
205161, 204nfim 1813 . . . . . . . . . . . . . . . 16 𝑥((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
206 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (𝐻𝑥) = (𝐻𝑣))
207 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → (𝐺𝑥) = (𝐺𝑣))
208170, 207oveq12d 6567 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → ((𝐹𝑥) / (𝐺𝑥)) = ((𝐹𝑣) / (𝐺𝑣)))
209206, 208eqeq12d 2625 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → ((𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)) ↔ (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣))))
210169, 209imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥))) ↔ ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))))
211192fvmpt2 6200 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻𝑥) = (𝐵 / 𝐶))
212173, 191, 211syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐻𝑥) = (𝐵 / 𝐶))
213175eqcomd 2616 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵 = (𝐹𝑥))
2145fvmpt2 6200 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐶 ∈ (ℂ ∖ {0})) → (𝐺𝑥) = 𝐶)
215173, 3, 214syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝐺𝑥) = 𝐶)
216215eqcomd 2616 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐶 = (𝐺𝑥))
217213, 216oveq12d 6567 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝐵 / 𝐶) = ((𝐹𝑥) / (𝐺𝑥)))
218212, 217eqtrd 2644 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐻𝑥) = ((𝐹𝑥) / (𝐺𝑥)))
219205, 210, 218chvar 2250 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐴) → (𝐻𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
220195, 219eqtrd 2644 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐴) → ((𝐻𝑣) − 0) = ((𝐹𝑣) / (𝐺𝑣)))
221220fveq2d 6107 . . . . . . . . . . . . 13 ((𝜑𝑣𝐴) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
222187, 188, 221syl2anc 691 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) = (abs‘((𝐹𝑣) / (𝐺𝑣))))
223 simp-6l 806 . . . . . . . . . . . . . 14 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝜑𝑦 ∈ ℝ+))
224223, 188jca 553 . . . . . . . . . . . . 13 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴))
225 simplr 788 . . . . . . . . . . . . 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 2751 . . . . . . . . . . . . . . . . . . . 20 𝑥0
228202, 227nfne 2882 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐺𝑣) ≠ 0
229161, 228nfim 1813 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
230207neeq1d 2841 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑣 → ((𝐺𝑥) ≠ 0 ↔ (𝐺𝑣) ≠ 0))
231169, 230imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0) ↔ ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)))
232215, 190eqnetrd 2849 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐺𝑥) ≠ 0)
233229, 231, 232chvar 2250 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → (𝐺𝑣) ≠ 0)
234177, 57, 233absdivd 14042 . . . . . . . . . . . . . . . 16 ((𝜑𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
235234adantlr 747 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
236235ad2antrr 758 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) = ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))))
237177abscld 14023 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐹𝑣)) ∈ ℝ)
23857, 233absne0d 14034 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
239237, 78, 238redivcld 10732 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
240239adantlr 747 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
241240ad2antrr 758 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) ∈ ℝ)
242 rpre 11715 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
243242ad2antlr 759 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℝ)
24420rpred 11748 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245244ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246243, 245remulcld 9949 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247246ad2antrr 758 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
24857, 233absrpcld 14035 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
249248adantlr 747 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℝ+)
250249ad2antrr 758 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
251247, 250rerpdivcld 11779 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) ∈ ℝ)
252243ad2antrr 758 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑦 ∈ ℝ)
253 simp-4l 802 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
254 simpllr 795 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣𝐴)
255253, 254, 237syl2anc 691 . . . . . . . . . . . . . . . 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 11805 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))))
258243recnd 9947 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → 𝑦 ∈ ℂ)
25947ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260249rpcnd 11750 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ∈ ℂ)
261238adantlr 747 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (abs‘(𝐺𝑣)) ≠ 0)
262258, 259, 260, 261divassd 10715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
263262adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))))
264245, 249rerpdivcld 11779 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
265264adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) ∈ ℝ)
266 1red 9934 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ)
267 simpllr 795 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 𝑦 ∈ ℝ+)
268244ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269 1rp 11712 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ+
270269a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → 1 ∈ ℝ+)
271248adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (abs‘(𝐺𝑣)) ∈ ℝ+)
27247div1d 10672 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273272ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))
275273, 274eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺𝑣)))
276268, 270, 271, 275ltdiv23d 11813 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
277276adantllr 751 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣))) < 1)
278265, 266, 267, 277ltmul2dd 11804 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺𝑣)))) < (𝑦 · 1))
279263, 278eqbrtrd 4605 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < (𝑦 · 1))
280258mulid1d 9936 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) → (𝑦 · 1) = 𝑦)
281280adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → (𝑦 · 1) = 𝑦)
282279, 281breqtrd 4609 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
283282adantr 480 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺𝑣))) < 𝑦)
284241, 251, 252, 257, 283lttrd 10077 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹𝑣)) / (abs‘(𝐺𝑣))) < 𝑦)
285236, 284eqbrtrd 4605 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑣𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
286224, 225, 226, 285syl21anc 1317 . . . . . . . . . . . 12 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹𝑣) / (𝐺𝑣))) < 𝑦)
287222, 286eqbrtrd 4605 . . . . . . . . . . 11 ((((((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+) ∧ 𝑢 ∈ ℝ+) ∧ 𝑣𝐴) ∧ 𝑣𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) ∧ (abs‘(𝐹𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
288128, 150, 186, 287syl21anc 1317 . . . . . . . . . 10 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣𝐴 ∧ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))) → (abs‘((𝐻𝑣) − 0)) < 𝑦)
2892883exp 1256 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣𝐴 → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
290121, 289ralrimi 2940 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
291 breq2 4587 . . . . . . . . . . . 12 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → ((abs‘(𝑣𝐸)) < 𝑤 ↔ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)))
292291anbi2d 736 . . . . . . . . . . 11 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) ↔ (𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢))))
293292imbi1d 330 . . . . . . . . . 10 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → (((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦) ↔ ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
294293ralbidv 2969 . . . . . . . . 9 (𝑤 = if(𝑧𝑢, 𝑧, 𝑢) → (∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦) ↔ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
295294rspcev 3282 . . . . . . . 8 ((if(𝑧𝑢, 𝑧, 𝑢) ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < if(𝑧𝑢, 𝑧, 𝑢)) → (abs‘((𝐻𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
296114, 290, 295syl2anc 691 . . . . . . 7 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣)))) ∧ 𝑢 ∈ ℝ+ ∧ ∀𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑢) → (abs‘((𝐹𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
297296rexlimdv3a 3015 . . . . . 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 3015 . . . 4 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺𝑣))) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦)))
30089, 299mpd 15 . . 3 ((𝜑𝑦 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
301300ralrimiva 2949 . 2 (𝜑 → ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))
302193, 10, 13ellimc3 23449 . 2 (𝜑 → (0 ∈ (𝐻 lim 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ((𝑣𝐸 ∧ (abs‘(𝑣𝐸)) < 𝑤) → (abs‘((𝐻𝑣) − 0)) < 𝑦))))
3031, 301, 302mpbir2and 959 1 (𝜑 → 0 ∈ (𝐻 lim 𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537   ⊆ wss 3540  ifcif 4036  {csn 4125   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  2c2 10947  ℝ+crp 11708  abscabs 13822   limℂ climc 23432 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-fz 12198  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-mulr 15782  df-starv 15783  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-rest 15906  df-topn 15907  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cnp 20842  df-xms 21935  df-ms 21936  df-limc 23436 This theorem is referenced by:  reclimc  38720
 Copyright terms: Public domain W3C validator