MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  taylthlem1 Structured version   Visualization version   GIF version

Theorem taylthlem1 24065
Description: Lemma for taylth 24067. This is the main part of Taylor's theorem, except for the induction step, which is supposed to be proven using L'Hôpital's rule. However, since our proof of L'Hôpital assumes that 𝑆 = ℝ, we can only do this part generically, and for taylth 24067 itself we must restrict to . (Contributed by Mario Carneiro, 1-Jan-2017.)
Hypotheses
Ref Expression
taylthlem1.s (𝜑𝑆 ∈ {ℝ, ℂ})
taylthlem1.f (𝜑𝐹:𝐴⟶ℂ)
taylthlem1.a (𝜑𝐴𝑆)
taylthlem1.d (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) = 𝐴)
taylthlem1.n (𝜑𝑁 ∈ ℕ)
taylthlem1.b (𝜑𝐵𝐴)
taylthlem1.t 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
taylthlem1.r 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁)))
taylthlem1.i ((𝜑 ∧ (𝑛 ∈ (1..^𝑁) ∧ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵))) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))
Assertion
Ref Expression
taylthlem1 (𝜑 → 0 ∈ (𝑅 lim 𝐵))
Distinct variable groups:   𝑥,𝑛,𝑦,𝐴   𝐵,𝑛,𝑥,𝑦   𝑛,𝐹,𝑥,𝑦   𝜑,𝑛,𝑥,𝑦   𝑛,𝑁,𝑥,𝑦   𝑆,𝑛,𝑥,𝑦   𝑇,𝑛,𝑥,𝑦
Allowed substitution hints:   𝑅(𝑥,𝑦,𝑛)

Proof of Theorem taylthlem1
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 taylthlem1.n . . . 4 (𝜑𝑁 ∈ ℕ)
2 elfz1end 12329 . . . 4 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
31, 2sylib 208 . . 3 (𝜑𝑁 ∈ (1...𝑁))
4 oveq2 6623 . . . . . . . . . . . 12 (𝑚 = 1 → (𝑁𝑚) = (𝑁 − 1))
54fveq2d 6162 . . . . . . . . . . 11 (𝑚 = 1 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
65fveq1d 6160 . . . . . . . . . 10 (𝑚 = 1 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
74fveq2d 6162 . . . . . . . . . . 11 (𝑚 = 1 → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 1)))
87fveq1d 6160 . . . . . . . . . 10 (𝑚 = 1 → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
96, 8oveq12d 6633 . . . . . . . . 9 (𝑚 = 1 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
10 oveq2 6623 . . . . . . . . 9 (𝑚 = 1 → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑1))
119, 10oveq12d 6633 . . . . . . . 8 (𝑚 = 1 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1)))
1211mpteq2dv 4715 . . . . . . 7 (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))))
1312oveq1d 6630 . . . . . 6 (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵))
1413eleq2d 2684 . . . . 5 (𝑚 = 1 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵)))
1514imbi2d 330 . . . 4 (𝑚 = 1 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵))))
16 oveq2 6623 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (𝑁𝑚) = (𝑁𝑛))
1716fveq2d 6162 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁𝑛)))
1817fveq1d 6160 . . . . . . . . . . 11 (𝑚 = 𝑛 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥))
1916fveq2d 6162 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑛)))
2019fveq1d 6160 . . . . . . . . . . 11 (𝑚 = 𝑛 → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥))
2118, 20oveq12d 6633 . . . . . . . . . 10 (𝑚 = 𝑛 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)))
22 oveq2 6623 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑𝑛))
2321, 22oveq12d 6633 . . . . . . . . 9 (𝑚 = 𝑛 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛)))
2423mpteq2dv 4715 . . . . . . . 8 (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛))))
25 fveq2 6158 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦))
26 fveq2 6158 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦))
2725, 26oveq12d 6633 . . . . . . . . . 10 (𝑥 = 𝑦 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)))
28 oveq1 6622 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥𝐵) = (𝑦𝐵))
2928oveq1d 6630 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥𝐵)↑𝑛) = ((𝑦𝐵)↑𝑛))
3027, 29oveq12d 6633 . . . . . . . . 9 (𝑥 = 𝑦 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛)) = (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛)))
3130cbvmptv 4720 . . . . . . . 8 (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛)))
3224, 31syl6eq 2671 . . . . . . 7 (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))))
3332oveq1d 6630 . . . . . 6 (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵))
3433eleq2d 2684 . . . . 5 (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵)))
3534imbi2d 330 . . . 4 (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵))))
36 oveq2 6623 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (𝑁𝑚) = (𝑁 − (𝑛 + 1)))
3736fveq2d 6162 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1))))
3837fveq1d 6160 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥))
3936fveq2d 6162 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1))))
4039fveq1d 6160 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))
4138, 40oveq12d 6633 . . . . . . . . 9 (𝑚 = (𝑛 + 1) → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)))
42 oveq2 6623 . . . . . . . . 9 (𝑚 = (𝑛 + 1) → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑(𝑛 + 1)))
4341, 42oveq12d 6633 . . . . . . . 8 (𝑚 = (𝑛 + 1) → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1))))
4443mpteq2dv 4715 . . . . . . 7 (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))))
4544oveq1d 6630 . . . . . 6 (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))
4645eleq2d 2684 . . . . 5 (𝑚 = (𝑛 + 1) → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵)))
4746imbi2d 330 . . . 4 (𝑚 = (𝑛 + 1) → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))))
48 oveq2 6623 . . . . . . . . . . . 12 (𝑚 = 𝑁 → (𝑁𝑚) = (𝑁𝑁))
4948fveq2d 6162 . . . . . . . . . . 11 (𝑚 = 𝑁 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁𝑁)))
5049fveq1d 6160 . . . . . . . . . 10 (𝑚 = 𝑁 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥))
5148fveq2d 6162 . . . . . . . . . . 11 (𝑚 = 𝑁 → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑁)))
5251fveq1d 6160 . . . . . . . . . 10 (𝑚 = 𝑁 → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥))
5350, 52oveq12d 6633 . . . . . . . . 9 (𝑚 = 𝑁 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)))
54 oveq2 6623 . . . . . . . . 9 (𝑚 = 𝑁 → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑𝑁))
5553, 54oveq12d 6633 . . . . . . . 8 (𝑚 = 𝑁 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁)))
5655mpteq2dv 4715 . . . . . . 7 (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))))
5756oveq1d 6630 . . . . . 6 (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵))
5857eleq2d 2684 . . . . 5 (𝑚 = 𝑁 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵)))
5958imbi2d 330 . . . 4 (𝑚 = 𝑁 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵))))
60 taylthlem1.b . . . . . . . . . . . 12 (𝜑𝐵𝐴)
61 fveq2 6158 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵))
62 fveq2 6158 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) = (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵))
6361, 62oveq12d 6633 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)))
64 eqid 2621 . . . . . . . . . . . . 13 (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))) = (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
65 ovex 6643 . . . . . . . . . . . . 13 ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)) ∈ V
6663, 64, 65fvmpt 6249 . . . . . . . . . . . 12 (𝐵𝐴 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)))
6760, 66syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)))
68 taylthlem1.s . . . . . . . . . . . . 13 (𝜑𝑆 ∈ {ℝ, ℂ})
69 taylthlem1.f . . . . . . . . . . . . 13 (𝜑𝐹:𝐴⟶ℂ)
70 taylthlem1.a . . . . . . . . . . . . 13 (𝜑𝐴𝑆)
711nnnn0d 11311 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℕ0)
72 nn0uz 11682 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
7371, 72syl6eleq 2708 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (ℤ‘0))
74 eluzfz2b 12308 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘0) ↔ 𝑁 ∈ (0...𝑁))
7573, 74sylib 208 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (0...𝑁))
76 taylthlem1.d . . . . . . . . . . . . . 14 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) = 𝐴)
7760, 76eleqtrrd 2701 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))
78 taylthlem1.t . . . . . . . . . . . . 13 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
7968, 69, 70, 75, 77, 78dvntaylp0 24064 . . . . . . . . . . . 12 (𝜑 → (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵))
8079oveq2d 6631 . . . . . . . . . . 11 (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)))
81 cnex 9977 . . . . . . . . . . . . . . . 16 ℂ ∈ V
8281a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℂ ∈ V)
83 elpm2r 7835 . . . . . . . . . . . . . . 15 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆))
8482, 68, 69, 70, 83syl22anc 1324 . . . . . . . . . . . . . 14 (𝜑𝐹 ∈ (ℂ ↑pm 𝑆))
85 dvnf 23630 . . . . . . . . . . . . . 14 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ 𝑁 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ)
8668, 84, 71, 85syl3anc 1323 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ)
8786, 77ffvelrnd 6326 . . . . . . . . . . . 12 (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ)
8887subidd 10340 . . . . . . . . . . 11 (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) = 0)
8967, 80, 883eqtrd 2659 . . . . . . . . . 10 (𝜑 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0)
90 funmpt 5894 . . . . . . . . . . 11 Fun (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
91 ovex 6643 . . . . . . . . . . . . 13 ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)) ∈ V
9291, 64dmmpti 5990 . . . . . . . . . . . 12 dom (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))) = 𝐴
9360, 92syl6eleqr 2709 . . . . . . . . . . 11 (𝜑𝐵 ∈ dom (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))))
94 funbrfvb 6205 . . . . . . . . . . 11 ((Fun (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))) ∧ 𝐵 ∈ dom (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))) → (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0))
9590, 93, 94sylancr 694 . . . . . . . . . 10 (𝜑 → (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0))
9689, 95mpbid 222 . . . . . . . . 9 (𝜑𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0)
97 nnm1nn0 11294 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
981, 97syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 − 1) ∈ ℕ0)
99 dvnf 23630 . . . . . . . . . . . . . 14 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
10068, 84, 98, 99syl3anc 1323 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
101 dvnbss 23631 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0) → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
10268, 84, 98, 101syl3anc 1323 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
103 fdm 6018 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴)
10469, 103syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐹 = 𝐴)
105102, 104sseqtrd 3626 . . . . . . . . . . . . . . 15 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴)
106 fzo0end 12517 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
107 elfzofz 12442 . . . . . . . . . . . . . . . . . 18 ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁))
1081, 106, 1073syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 − 1) ∈ (0...𝑁))
109 dvn2bss 23633 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
11068, 84, 108, 109syl3anc 1323 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
11176, 110eqsstr3d 3625 . . . . . . . . . . . . . . 15 (𝜑𝐴 ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
112105, 111eqssd 3605 . . . . . . . . . . . . . 14 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = 𝐴)
113112feq2d 5998 . . . . . . . . . . . . 13 (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ))
114100, 113mpbid 222 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)
115114ffvelrnda 6325 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
11676feq2d 5998 . . . . . . . . . . . . 13 (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ))
11786, 116mpbid 222 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ)
118117ffvelrnda 6325 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ)
1191nncnd 10996 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
120 1cnd 10016 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
121119, 120npcand 10356 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
122121fveq2d 6162 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D𝑛 𝐹)‘𝑁))
123 recnprss 23608 . . . . . . . . . . . . . . 15 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
12468, 123syl 17 . . . . . . . . . . . . . 14 (𝜑𝑆 ⊆ ℂ)
125 dvnp1 23628 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
126124, 84, 98, 125syl3anc 1323 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
127122, 126eqtr3d 2657 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
128117feqmptd 6216 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦)))
129114feqmptd 6216 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))
130129oveq2d 6631 . . . . . . . . . . . 12 (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))))
131127, 128, 1303eqtr3rd 2664 . . . . . . . . . . 11 (𝜑 → (𝑆 D (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦)))
13270, 124sstrd 3598 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℂ)
133132sselda 3588 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝑦 ∈ ℂ)
134 1nn0 11268 . . . . . . . . . . . . . . . 16 1 ∈ ℕ0
135134a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℕ0)
136 elpm2r 7835 . . . . . . . . . . . . . . . . . . . 20 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴𝑆)) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑pm 𝑆))
13782, 68, 114, 70, 136syl22anc 1324 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑pm 𝑆))
138 dvn1 23629 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
139124, 137, 138syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
140126, 122eqtr3d 2657 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁))
141139, 140eqtrd 2655 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D𝑛 𝐹)‘𝑁))
142141dmeqd 5296 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
14377, 142eleqtrrd 2701 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1))
144 eqid 2621 . . . . . . . . . . . . . . 15 (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵)
14568, 114, 70, 135, 143, 144taylpf 24058 . . . . . . . . . . . . . 14 (𝜑 → (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)
146120, 119pncan3d 10355 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 + (𝑁 − 1)) = 𝑁)
147146oveq1d 6630 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
148147, 78syl6reqr 2674 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))
149148oveq2d 6631 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℂ D𝑛 𝑇) = (ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)))
150149fveq1d 6160 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)))
151146fveq2d 6162 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁))
152151dmeqd 5296 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
15377, 152eleqtrrd 2701 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))))
15468, 69, 70, 98, 135, 153dvntaylp 24063 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵))
155150, 154eqtrd 2655 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵))
156155feq1d 5997 . . . . . . . . . . . . . 14 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔ (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ))
157145, 156mpbird 247 . . . . . . . . . . . . 13 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ)
158157ffvelrnda 6325 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
159133, 158syldan 487 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
160 0nn0 11267 . . . . . . . . . . . . . . . 16 0 ∈ ℕ0
161160a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℕ0)
162 elpm2r 7835 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴𝑆)) → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆))
16382, 68, 117, 70, 162syl22anc 1324 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆))
164 dvn0 23627 . . . . . . . . . . . . . . . . . 18 ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁))
165124, 163, 164syl2anc 692 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁))
166165dmeqd 5296 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
16777, 166eleqtrrd 2701 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0))
168 eqid 2621 . . . . . . . . . . . . . . 15 (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵)
16968, 117, 70, 161, 167, 168taylpf 24058 . . . . . . . . . . . . . 14 (𝜑 → (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)
170119addid2d 10197 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (0 + 𝑁) = 𝑁)
171170oveq1d 6630 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
172171, 78syl6eqr 2673 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇)
173172oveq2d 6631 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℂ D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D𝑛 𝑇))
174173fveq1d 6160 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D𝑛 𝑇)‘𝑁))
175170fveq2d 6162 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D𝑛 𝐹)‘𝑁))
176175dmeqd 5296 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
17777, 176eleqtrrd 2701 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)))
17868, 69, 70, 71, 161, 177dvntaylp 24063 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵))
179174, 178eqtr3d 2657 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵))
180179feq1d 5997 . . . . . . . . . . . . . 14 (𝜑 → (((ℂ D𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ))
181169, 180mpbird 247 . . . . . . . . . . . . 13 (𝜑 → ((ℂ D𝑛 𝑇)‘𝑁):ℂ⟶ℂ)
182181ffvelrnda 6325 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
183133, 182syldan 487 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
184124sselda 3588 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → 𝑦 ∈ ℂ)
185184, 158syldan 487 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
186184, 182syldan 487 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
187 eqid 2621 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
188187cnfldtopon 22526 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
189 toponmax 20670 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
190188, 189mp1i 13 . . . . . . . . . . . . 13 (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
191 df-ss 3574 . . . . . . . . . . . . . 14 (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆)
192124, 191sylib 208 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∩ ℂ) = 𝑆)
193 ssid 3609 . . . . . . . . . . . . . . . . 17 ℂ ⊆ ℂ
194193a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ℂ ⊆ ℂ)
195 mapsspm 7851 . . . . . . . . . . . . . . . . 17 (ℂ ↑𝑚 ℂ) ⊆ (ℂ ↑pm ℂ)
19668, 69, 70, 71, 77, 78taylpf 24058 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:ℂ⟶ℂ)
19781, 81elmap 7846 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ (ℂ ↑𝑚 ℂ) ↔ 𝑇:ℂ⟶ℂ)
198196, 197sylibr 224 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ (ℂ ↑𝑚 ℂ))
199195, 198sseldi 3586 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ (ℂ ↑pm ℂ))
200 dvnp1 23628 . . . . . . . . . . . . . . . 16 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ) ∧ (𝑁 − 1) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))))
201194, 199, 98, 200syl3anc 1323 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))))
202121fveq2d 6162 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ D𝑛 𝑇)‘𝑁))
203201, 202eqtr3d 2657 . . . . . . . . . . . . . 14 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ D𝑛 𝑇)‘𝑁))
204157feqmptd 6216 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
205204oveq2d 6631 . . . . . . . . . . . . . 14 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))
206181feqmptd 6216 . . . . . . . . . . . . . 14 (𝜑 → ((ℂ D𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
207203, 205, 2063eqtr3d 2663 . . . . . . . . . . . . 13 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
208187, 68, 190, 192, 158, 182, 207dvmptres3 23659 . . . . . . . . . . . 12 (𝜑 → (𝑆 D (𝑦𝑆 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦𝑆 ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
209 eqid 2621 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
210 resttopon 20905 . . . . . . . . . . . . . . . 16 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
211188, 124, 210sylancr 694 . . . . . . . . . . . . . . 15 (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
212 topontop 20658 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
213211, 212syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
214 toponuni 20659 . . . . . . . . . . . . . . . 16 (((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
215211, 214syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
21670, 215sseqtrd 3626 . . . . . . . . . . . . . 14 (𝜑𝐴 ((TopOpen‘ℂfld) ↾t 𝑆))
217 eqid 2621 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
218217ntrss2 20801 . . . . . . . . . . . . . 14 ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝐴 ((TopOpen‘ℂfld) ↾t 𝑆)) → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴)
219213, 216, 218syl2anc 692 . . . . . . . . . . . . 13 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴)
220140dmeqd 5296 . . . . . . . . . . . . . . 15 (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
221220, 76eqtrd 2655 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = 𝐴)
222124, 114, 70, 209, 187dvbssntr 23604 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) ⊆ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴))
223221, 222eqsstr3d 3625 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴))
224219, 223eqssd 3605 . . . . . . . . . . . 12 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) = 𝐴)
22568, 185, 186, 208, 70, 209, 187, 224dvmptres2 23665 . . . . . . . . . . 11 (𝜑 → (𝑆 D (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
22668, 115, 118, 131, 159, 183, 225dvmptsub 23670 . . . . . . . . . 10 (𝜑 → (𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))))
227226breqd 4634 . . . . . . . . 9 (𝜑 → (𝐵(𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0))
22896, 227mpbird 247 . . . . . . . 8 (𝜑𝐵(𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0)
229 eqid 2621 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵)))
230115, 159subcld 10352 . . . . . . . . . 10 ((𝜑𝑦𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ)
231 eqid 2621 . . . . . . . . . 10 (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
232230, 231fmptd 6351 . . . . . . . . 9 (𝜑 → (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ)
233209, 187, 229, 124, 232, 70eldv 23602 . . . . . . . 8 (𝜑 → (𝐵(𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ (𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵))))
234228, 233mpbid 222 . . . . . . 7 (𝜑 → (𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵)))
235234simprd 479 . . . . . 6 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵))
236 eldifi 3716 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐴)
237 fveq2 6158 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
238 fveq2 6158 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
239237, 238oveq12d 6633 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
240 ovex 6643 . . . . . . . . . . . . 13 ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V
241239, 231, 240fvmpt 6249 . . . . . . . . . . . 12 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
242 fveq2 6158 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
243 fveq2 6158 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵))
244242, 243oveq12d 6633 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
245 ovex 6643 . . . . . . . . . . . . . . 15 ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V
246244, 231, 245fvmpt 6249 . . . . . . . . . . . . . 14 (𝐵𝐴 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
24760, 246syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
24868, 69, 70, 108, 77, 78dvntaylp0 24064 . . . . . . . . . . . . . 14 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
249248oveq2d 6631 . . . . . . . . . . . . 13 (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)))
250114, 60ffvelrnd 6326 . . . . . . . . . . . . . 14 (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ)
251250subidd 10340 . . . . . . . . . . . . 13 (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0)
252247, 249, 2513eqtrd 2659 . . . . . . . . . . . 12 (𝜑 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0)
253241, 252oveqan12rd 6635 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0))
254114ffvelrnda 6325 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
255132sselda 3588 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑥 ∈ ℂ)
256157ffvelrnda 6325 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
257255, 256syldan 487 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
258254, 257subcld 10352 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ)
259258subid1d 10341 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
260253, 259eqtr2d 2656 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
261236, 260sylan2 491 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
262132ssdifssd 3732 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
263262sselda 3588 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
264132, 60sseldd 3589 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
265264adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
266263, 265subcld 10352 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℂ)
267266exp1d 12959 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑1) = (𝑥𝐵))
268261, 267oveq12d 6633 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1)) = ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵)))
269268mpteq2dva 4714 . . . . . . 7 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))))
270269oveq1d 6630 . . . . . 6 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵))
271235, 270eleqtrrd 2701 . . . . 5 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵))
272271a1i 11 . . . 4 (𝑁 ∈ (ℤ‘1) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵)))
273 taylthlem1.i . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (1..^𝑁) ∧ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵))) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))
274273expr 642 . . . . . 6 ((𝜑𝑛 ∈ (1..^𝑁)) → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵)))
275274expcom 451 . . . . 5 (𝑛 ∈ (1..^𝑁) → (𝜑 → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))))
276275a2d 29 . . . 4 (𝑛 ∈ (1..^𝑁) → ((𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵)) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))))
27715, 35, 47, 59, 272, 276fzind2 12542 . . 3 (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵)))
2783, 277mpcom 38 . 2 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵))
279119subidd 10340 . . . . . . . . . 10 (𝜑 → (𝑁𝑁) = 0)
280279fveq2d 6162 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑁)) = ((𝑆 D𝑛 𝐹)‘0))
281 dvn0 23627 . . . . . . . . . 10 ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
282124, 84, 281syl2anc 692 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
283280, 282eqtrd 2655 . . . . . . . 8 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑁)) = 𝐹)
284283fveq1d 6160 . . . . . . 7 (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) = (𝐹𝑥))
285279fveq2d 6162 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑁)) = ((ℂ D𝑛 𝑇)‘0))
286 dvn0 23627 . . . . . . . . . 10 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ)) → ((ℂ D𝑛 𝑇)‘0) = 𝑇)
287193, 199, 286sylancr 694 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘0) = 𝑇)
288285, 287eqtrd 2655 . . . . . . . 8 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑁)) = 𝑇)
289288fveq1d 6160 . . . . . . 7 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥) = (𝑇𝑥))
290284, 289oveq12d 6633 . . . . . 6 (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) = ((𝐹𝑥) − (𝑇𝑥)))
291290oveq1d 6630 . . . . 5 (𝜑 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁)) = (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁)))
292291mpteq2dv 4715 . . . 4 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁))))
293 taylthlem1.r . . . 4 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁)))
294292, 293syl6eqr 2673 . . 3 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) = 𝑅)
295294oveq1d 6630 . 2 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵) = (𝑅 lim 𝐵))
296278, 295eleqtrd 2700 1 (𝜑 → 0 ∈ (𝑅 lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  Vcvv 3190  cdif 3557  cin 3559  wss 3560  {csn 4155  {cpr 4157   cuni 4409   class class class wbr 4623  cmpt 4683  dom cdm 5084  Fun wfun 5851  wf 5853  cfv 5857  (class class class)co 6615  𝑚 cmap 7817  pm cpm 7818  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899  cmin 10226   / cdiv 10644  cn 10980  0cn0 11252  cuz 11647  ...cfz 12284  ..^cfzo 12422  cexp 12816  t crest 16021  TopOpenctopn 16022  fldccnfld 19686  Topctop 20638  TopOnctopon 20655  intcnt 20761   lim climc 23566   D cdv 23567   D𝑛 cdvn 23568   Tayl ctayl 24045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-fi 8277  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-xnn0 11324  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-icc 12140  df-fz 12285  df-fzo 12423  df-seq 12758  df-exp 12817  df-fac 13017  df-hash 13074  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-clim 14169  df-sum 14367  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-starv 15896  df-sca 15897  df-vsca 15898  df-ip 15899  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-hom 15906  df-cco 15907  df-rest 16023  df-topn 16024  df-0g 16042  df-gsum 16043  df-topgen 16044  df-pt 16045  df-prds 16048  df-xrs 16102  df-qtop 16107  df-imas 16108  df-xps 16110  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-grp 17365  df-minusg 17366  df-mulg 17481  df-cntz 17690  df-cmn 18135  df-abl 18136  df-mgp 18430  df-ur 18442  df-ring 18489  df-cring 18490  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-fbas 19683  df-fg 19684  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-cld 20763  df-ntr 20764  df-cls 20765  df-nei 20842  df-lp 20880  df-perf 20881  df-cn 20971  df-cnp 20972  df-haus 21059  df-tx 21305  df-hmeo 21498  df-fil 21590  df-fm 21682  df-flim 21683  df-flf 21684  df-tsms 21870  df-xms 22065  df-ms 22066  df-tms 22067  df-cncf 22621  df-limc 23570  df-dv 23571  df-dvn 23572  df-tayl 24047
This theorem is referenced by:  taylth  24067
  Copyright terms: Public domain W3C validator