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

Theorem taylthlem1 25278
Description: Lemma for taylth 25280. 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 25280 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 13155 . . . 4 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
31, 2sylib 221 . . 3 (𝜑𝑁 ∈ (1...𝑁))
4 oveq2 7230 . . . . . . . . . . . 12 (𝑚 = 1 → (𝑁𝑚) = (𝑁 − 1))
54fveq2d 6730 . . . . . . . . . . 11 (𝑚 = 1 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
65fveq1d 6728 . . . . . . . . . 10 (𝑚 = 1 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
74fveq2d 6730 . . . . . . . . . . 11 (𝑚 = 1 → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 1)))
87fveq1d 6728 . . . . . . . . . 10 (𝑚 = 1 → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
96, 8oveq12d 7240 . . . . . . . . 9 (𝑚 = 1 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
10 oveq2 7230 . . . . . . . . 9 (𝑚 = 1 → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑1))
119, 10oveq12d 7240 . . . . . . . 8 (𝑚 = 1 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1)))
1211mpteq2dv 5160 . . . . . . 7 (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))))
1312oveq1d 7237 . . . . . 6 (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵))
1413eleq2d 2824 . . . . 5 (𝑚 = 1 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵)))
1514imbi2d 344 . . . 4 (𝑚 = 1 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵))))
16 oveq2 7230 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (𝑁𝑚) = (𝑁𝑛))
1716fveq2d 6730 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁𝑛)))
1817fveq1d 6728 . . . . . . . . . . 11 (𝑚 = 𝑛 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥))
1916fveq2d 6730 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑛)))
2019fveq1d 6728 . . . . . . . . . . 11 (𝑚 = 𝑛 → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥))
2118, 20oveq12d 7240 . . . . . . . . . 10 (𝑚 = 𝑛 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)))
22 oveq2 7230 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑𝑛))
2321, 22oveq12d 7240 . . . . . . . . 9 (𝑚 = 𝑛 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛)))
2423mpteq2dv 5160 . . . . . . . 8 (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛))))
25 fveq2 6726 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦))
26 fveq2 6726 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦))
2725, 26oveq12d 7240 . . . . . . . . . 10 (𝑥 = 𝑦 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)))
28 oveq1 7229 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥𝐵) = (𝑦𝐵))
2928oveq1d 7237 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥𝐵)↑𝑛) = ((𝑦𝐵)↑𝑛))
3027, 29oveq12d 7240 . . . . . . . . 9 (𝑥 = 𝑦 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛)) = (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛)))
3130cbvmptv 5167 . . . . . . . 8 (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛)))
3224, 31eqtrdi 2795 . . . . . . 7 (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))))
3332oveq1d 7237 . . . . . 6 (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵))
3433eleq2d 2824 . . . . 5 (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵)))
3534imbi2d 344 . . . 4 (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵))))
36 oveq2 7230 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (𝑁𝑚) = (𝑁 − (𝑛 + 1)))
3736fveq2d 6730 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1))))
3837fveq1d 6728 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥))
3936fveq2d 6730 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1))))
4039fveq1d 6728 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))
4138, 40oveq12d 7240 . . . . . . . . 9 (𝑚 = (𝑛 + 1) → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)))
42 oveq2 7230 . . . . . . . . 9 (𝑚 = (𝑛 + 1) → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑(𝑛 + 1)))
4341, 42oveq12d 7240 . . . . . . . 8 (𝑚 = (𝑛 + 1) → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1))))
4443mpteq2dv 5160 . . . . . . 7 (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))))
4544oveq1d 7237 . . . . . 6 (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))
4645eleq2d 2824 . . . . 5 (𝑚 = (𝑛 + 1) → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵)))
4746imbi2d 344 . . . 4 (𝑚 = (𝑛 + 1) → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))))
48 oveq2 7230 . . . . . . . . . . . 12 (𝑚 = 𝑁 → (𝑁𝑚) = (𝑁𝑁))
4948fveq2d 6730 . . . . . . . . . . 11 (𝑚 = 𝑁 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁𝑁)))
5049fveq1d 6728 . . . . . . . . . 10 (𝑚 = 𝑁 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥))
5148fveq2d 6730 . . . . . . . . . . 11 (𝑚 = 𝑁 → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑁)))
5251fveq1d 6728 . . . . . . . . . 10 (𝑚 = 𝑁 → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥))
5350, 52oveq12d 7240 . . . . . . . . 9 (𝑚 = 𝑁 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)))
54 oveq2 7230 . . . . . . . . 9 (𝑚 = 𝑁 → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑𝑁))
5553, 54oveq12d 7240 . . . . . . . 8 (𝑚 = 𝑁 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁)))
5655mpteq2dv 5160 . . . . . . 7 (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))))
5756oveq1d 7237 . . . . . 6 (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵))
5857eleq2d 2824 . . . . 5 (𝑚 = 𝑁 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵)))
5958imbi2d 344 . . . 4 (𝑚 = 𝑁 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵))))
60 taylthlem1.b . . . . . . . . . . . 12 (𝜑𝐵𝐴)
61 fveq2 6726 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵))
62 fveq2 6726 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) = (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵))
6361, 62oveq12d 7240 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)))
64 eqid 2738 . . . . . . . . . . . . 13 (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))) = (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
65 ovex 7255 . . . . . . . . . . . . 13 ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)) ∈ V
6663, 64, 65fvmpt 6827 . . . . . . . . . . . 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 12163 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℕ0)
72 nn0uz 12489 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
7371, 72eleqtrdi 2849 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (ℤ‘0))
74 eluzfz2b 13134 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘0) ↔ 𝑁 ∈ (0...𝑁))
7573, 74sylib 221 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (0...𝑁))
76 taylthlem1.d . . . . . . . . . . . . . 14 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) = 𝐴)
7760, 76eleqtrrd 2842 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))
78 taylthlem1.t . . . . . . . . . . . . 13 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
7968, 69, 70, 75, 77, 78dvntaylp0 25277 . . . . . . . . . . . 12 (𝜑 → (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵))
8079oveq2d 7238 . . . . . . . . . . 11 (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)))
81 cnex 10823 . . . . . . . . . . . . . . . 16 ℂ ∈ V
8281a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℂ ∈ V)
83 elpm2r 8535 . . . . . . . . . . . . . . 15 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆))
8482, 68, 69, 70, 83syl22anc 839 . . . . . . . . . . . . . 14 (𝜑𝐹 ∈ (ℂ ↑pm 𝑆))
85 dvnf 24837 . . . . . . . . . . . . . 14 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ 𝑁 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ)
8668, 84, 71, 85syl3anc 1373 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ)
8786, 77ffvelrnd 6914 . . . . . . . . . . . 12 (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ)
8887subidd 11190 . . . . . . . . . . 11 (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) = 0)
8967, 80, 883eqtrd 2782 . . . . . . . . . 10 (𝜑 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0)
90 funmpt 6427 . . . . . . . . . . 11 Fun (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
91 ovex 7255 . . . . . . . . . . . . 13 ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)) ∈ V
9291, 64dmmpti 6531 . . . . . . . . . . . 12 dom (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))) = 𝐴
9360, 92eleqtrrdi 2850 . . . . . . . . . . 11 (𝜑𝐵 ∈ dom (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))))
94 funbrfvb 6776 . . . . . . . . . . 11 ((Fun (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))) ∧ 𝐵 ∈ dom (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))) → (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0))
9590, 93, 94sylancr 590 . . . . . . . . . 10 (𝜑 → (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0))
9689, 95mpbid 235 . . . . . . . . 9 (𝜑𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0)
97 nnm1nn0 12144 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
981, 97syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 − 1) ∈ ℕ0)
99 dvnf 24837 . . . . . . . . . . . . . 14 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
10068, 84, 98, 99syl3anc 1373 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
101 dvnbss 24838 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0) → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
10268, 84, 98, 101syl3anc 1373 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
10369, 102fssdmd 6573 . . . . . . . . . . . . . . 15 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴)
104 fzo0end 13347 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
105 elfzofz 13271 . . . . . . . . . . . . . . . . . 18 ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁))
1061, 104, 1053syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 − 1) ∈ (0...𝑁))
107 dvn2bss 24840 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
10868, 84, 106, 107syl3anc 1373 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
10976, 108eqsstrrd 3949 . . . . . . . . . . . . . . 15 (𝜑𝐴 ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
110103, 109eqssd 3927 . . . . . . . . . . . . . 14 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = 𝐴)
111110feq2d 6540 . . . . . . . . . . . . 13 (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ))
112100, 111mpbid 235 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)
113112ffvelrnda 6913 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
11476feq2d 6540 . . . . . . . . . . . . 13 (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ))
11586, 114mpbid 235 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ)
116115ffvelrnda 6913 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ)
1171nncnd 11859 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
118 1cnd 10841 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
119117, 118npcand 11206 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
120119fveq2d 6730 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D𝑛 𝐹)‘𝑁))
121 recnprss 24814 . . . . . . . . . . . . . . 15 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
12268, 121syl 17 . . . . . . . . . . . . . 14 (𝜑𝑆 ⊆ ℂ)
123 dvnp1 24835 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
124122, 84, 98, 123syl3anc 1373 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
125120, 124eqtr3d 2780 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
126115feqmptd 6789 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦)))
127112feqmptd 6789 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))
128127oveq2d 7238 . . . . . . . . . . . 12 (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))))
129125, 126, 1283eqtr3rd 2787 . . . . . . . . . . 11 (𝜑 → (𝑆 D (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦)))
13070, 122sstrd 3920 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℂ)
131130sselda 3910 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝑦 ∈ ℂ)
132 1nn0 12119 . . . . . . . . . . . . . . . 16 1 ∈ ℕ0
133132a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℕ0)
134 elpm2r 8535 . . . . . . . . . . . . . . . . . . . 20 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴𝑆)) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑pm 𝑆))
13582, 68, 112, 70, 134syl22anc 839 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑pm 𝑆))
136 dvn1 24836 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
137122, 135, 136syl2anc 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
138124, 120eqtr3d 2780 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁))
139137, 138eqtrd 2778 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D𝑛 𝐹)‘𝑁))
140139dmeqd 5783 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
14177, 140eleqtrrd 2842 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1))
142 eqid 2738 . . . . . . . . . . . . . . 15 (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵)
14368, 112, 70, 133, 141, 142taylpf 25271 . . . . . . . . . . . . . 14 (𝜑 → (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)
144118, 117pncan3d 11205 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 + (𝑁 − 1)) = 𝑁)
145144oveq1d 7237 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
14678, 145eqtr4id 2798 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))
147146oveq2d 7238 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℂ D𝑛 𝑇) = (ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)))
148147fveq1d 6728 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)))
149144fveq2d 6730 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁))
150149dmeqd 5783 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
15177, 150eleqtrrd 2842 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))))
15268, 69, 70, 98, 133, 151dvntaylp 25276 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵))
153148, 152eqtrd 2778 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵))
154153feq1d 6539 . . . . . . . . . . . . . 14 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔ (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ))
155143, 154mpbird 260 . . . . . . . . . . . . 13 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ)
156155ffvelrnda 6913 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
157131, 156syldan 594 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
158 0nn0 12118 . . . . . . . . . . . . . . . 16 0 ∈ ℕ0
159158a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℕ0)
160 elpm2r 8535 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴𝑆)) → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆))
16182, 68, 115, 70, 160syl22anc 839 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆))
162 dvn0 24834 . . . . . . . . . . . . . . . . . 18 ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁))
163122, 161, 162syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁))
164163dmeqd 5783 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
16577, 164eleqtrrd 2842 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0))
166 eqid 2738 . . . . . . . . . . . . . . 15 (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵)
16768, 115, 70, 159, 165, 166taylpf 25271 . . . . . . . . . . . . . 14 (𝜑 → (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)
168117addid2d 11046 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (0 + 𝑁) = 𝑁)
169168oveq1d 7237 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
170169, 78eqtr4di 2797 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇)
171170oveq2d 7238 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℂ D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D𝑛 𝑇))
172171fveq1d 6728 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D𝑛 𝑇)‘𝑁))
173168fveq2d 6730 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D𝑛 𝐹)‘𝑁))
174173dmeqd 5783 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
17577, 174eleqtrrd 2842 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)))
17668, 69, 70, 71, 159, 175dvntaylp 25276 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵))
177172, 176eqtr3d 2780 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵))
178177feq1d 6539 . . . . . . . . . . . . . 14 (𝜑 → (((ℂ D𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ))
179167, 178mpbird 260 . . . . . . . . . . . . 13 (𝜑 → ((ℂ D𝑛 𝑇)‘𝑁):ℂ⟶ℂ)
180179ffvelrnda 6913 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
181131, 180syldan 594 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
182122sselda 3910 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → 𝑦 ∈ ℂ)
183182, 156syldan 594 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
184182, 180syldan 594 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
185 eqid 2738 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
186185cnfldtopon 23693 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
187 toponmax 21836 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
188186, 187mp1i 13 . . . . . . . . . . . . 13 (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
189 df-ss 3892 . . . . . . . . . . . . . 14 (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆)
190122, 189sylib 221 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∩ ℂ) = 𝑆)
191 ssid 3932 . . . . . . . . . . . . . . . . 17 ℂ ⊆ ℂ
192191a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ℂ ⊆ ℂ)
193 mapsspm 8566 . . . . . . . . . . . . . . . . 17 (ℂ ↑m ℂ) ⊆ (ℂ ↑pm ℂ)
19468, 69, 70, 71, 77, 78taylpf 25271 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:ℂ⟶ℂ)
19581, 81elmap 8561 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ (ℂ ↑m ℂ) ↔ 𝑇:ℂ⟶ℂ)
196194, 195sylibr 237 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ (ℂ ↑m ℂ))
197193, 196sselid 3907 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ (ℂ ↑pm ℂ))
198 dvnp1 24835 . . . . . . . . . . . . . . . 16 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ) ∧ (𝑁 − 1) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))))
199192, 197, 98, 198syl3anc 1373 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))))
200119fveq2d 6730 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ D𝑛 𝑇)‘𝑁))
201199, 200eqtr3d 2780 . . . . . . . . . . . . . 14 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ D𝑛 𝑇)‘𝑁))
202155feqmptd 6789 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
203202oveq2d 7238 . . . . . . . . . . . . . 14 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))
204179feqmptd 6789 . . . . . . . . . . . . . 14 (𝜑 → ((ℂ D𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
205201, 203, 2043eqtr3d 2786 . . . . . . . . . . . . 13 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
206185, 68, 188, 190, 156, 180, 205dvmptres3 24866 . . . . . . . . . . . 12 (𝜑 → (𝑆 D (𝑦𝑆 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦𝑆 ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
207 eqid 2738 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
208 resttopon 22071 . . . . . . . . . . . . . . . 16 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
209186, 122, 208sylancr 590 . . . . . . . . . . . . . . 15 (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
210 topontop 21823 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
211209, 210syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
212 toponuni 21824 . . . . . . . . . . . . . . . 16 (((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
213209, 212syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
21470, 213sseqtrd 3950 . . . . . . . . . . . . . 14 (𝜑𝐴 ((TopOpen‘ℂfld) ↾t 𝑆))
215 eqid 2738 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
216215ntrss2 21967 . . . . . . . . . . . . . 14 ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝐴 ((TopOpen‘ℂfld) ↾t 𝑆)) → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴)
217211, 214, 216syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴)
218138dmeqd 5783 . . . . . . . . . . . . . . 15 (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
219218, 76eqtrd 2778 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = 𝐴)
220122, 112, 70, 207, 185dvbssntr 24810 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) ⊆ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴))
221219, 220eqsstrrd 3949 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴))
222217, 221eqssd 3927 . . . . . . . . . . . 12 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) = 𝐴)
22368, 183, 184, 206, 70, 207, 185, 222dvmptres2 24872 . . . . . . . . . . 11 (𝜑 → (𝑆 D (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
22468, 113, 116, 129, 157, 181, 223dvmptsub 24877 . . . . . . . . . 10 (𝜑 → (𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))))
225224breqd 5073 . . . . . . . . 9 (𝜑 → (𝐵(𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0))
22696, 225mpbird 260 . . . . . . . 8 (𝜑𝐵(𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0)
227 eqid 2738 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵)))
228113, 157subcld 11202 . . . . . . . . . 10 ((𝜑𝑦𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ)
229228fmpttd 6941 . . . . . . . . 9 (𝜑 → (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ)
230207, 185, 227, 122, 229, 70eldv 24808 . . . . . . . 8 (𝜑 → (𝐵(𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ (𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵))))
231226, 230mpbid 235 . . . . . . 7 (𝜑 → (𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵)))
232231simprd 499 . . . . . 6 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵))
233 eldifi 4050 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐴)
234 fveq2 6726 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
235 fveq2 6726 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
236234, 235oveq12d 7240 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
237 eqid 2738 . . . . . . . . . . . . 13 (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
238 ovex 7255 . . . . . . . . . . . . 13 ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V
239236, 237, 238fvmpt 6827 . . . . . . . . . . . 12 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
240 fveq2 6726 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
241 fveq2 6726 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵))
242240, 241oveq12d 7240 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
243 ovex 7255 . . . . . . . . . . . . . . 15 ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V
244242, 237, 243fvmpt 6827 . . . . . . . . . . . . . 14 (𝐵𝐴 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
24560, 244syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
24668, 69, 70, 106, 77, 78dvntaylp0 25277 . . . . . . . . . . . . . 14 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
247246oveq2d 7238 . . . . . . . . . . . . 13 (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)))
248112, 60ffvelrnd 6914 . . . . . . . . . . . . . 14 (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ)
249248subidd 11190 . . . . . . . . . . . . 13 (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0)
250245, 247, 2493eqtrd 2782 . . . . . . . . . . . 12 (𝜑 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0)
251239, 250oveqan12rd 7242 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0))
252112ffvelrnda 6913 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
253130sselda 3910 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑥 ∈ ℂ)
254155ffvelrnda 6913 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
255253, 254syldan 594 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
256252, 255subcld 11202 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ)
257256subid1d 11191 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
258251, 257eqtr2d 2779 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
259233, 258sylan2 596 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
260130ssdifssd 4066 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
261260sselda 3910 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
262130, 60sseldd 3911 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
263262adantr 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
264261, 263subcld 11202 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℂ)
265264exp1d 13724 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑1) = (𝑥𝐵))
266259, 265oveq12d 7240 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1)) = ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵)))
267266mpteq2dva 5159 . . . . . . 7 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))))
268267oveq1d 7237 . . . . . 6 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵))
269232, 268eleqtrrd 2842 . . . . 5 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵))
270269a1i 11 . . . 4 (𝑁 ∈ (ℤ‘1) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵)))
271 taylthlem1.i . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (1..^𝑁) ∧ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵))) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))
272271expr 460 . . . . . 6 ((𝜑𝑛 ∈ (1..^𝑁)) → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵)))
273272expcom 417 . . . . 5 (𝑛 ∈ (1..^𝑁) → (𝜑 → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))))
274273a2d 29 . . . 4 (𝑛 ∈ (1..^𝑁) → ((𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵)) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))))
27515, 35, 47, 59, 270, 274fzind2 13373 . . 3 (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵)))
2763, 275mpcom 38 . 2 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵))
277117subidd 11190 . . . . . . . . . 10 (𝜑 → (𝑁𝑁) = 0)
278277fveq2d 6730 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑁)) = ((𝑆 D𝑛 𝐹)‘0))
279 dvn0 24834 . . . . . . . . . 10 ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
280122, 84, 279syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
281278, 280eqtrd 2778 . . . . . . . 8 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑁)) = 𝐹)
282281fveq1d 6728 . . . . . . 7 (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) = (𝐹𝑥))
283277fveq2d 6730 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑁)) = ((ℂ D𝑛 𝑇)‘0))
284 dvn0 24834 . . . . . . . . . 10 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ)) → ((ℂ D𝑛 𝑇)‘0) = 𝑇)
285191, 197, 284sylancr 590 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘0) = 𝑇)
286283, 285eqtrd 2778 . . . . . . . 8 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑁)) = 𝑇)
287286fveq1d 6728 . . . . . . 7 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥) = (𝑇𝑥))
288282, 287oveq12d 7240 . . . . . 6 (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) = ((𝐹𝑥) − (𝑇𝑥)))
289288oveq1d 7237 . . . . 5 (𝜑 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁)) = (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁)))
290289mpteq2dv 5160 . . . 4 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁))))
291 taylthlem1.r . . . 4 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁)))
292290, 291eqtr4di 2797 . . 3 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) = 𝑅)
293292oveq1d 7237 . 2 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵) = (𝑅 lim 𝐵))
294276, 293eleqtrd 2841 1 (𝜑 → 0 ∈ (𝑅 lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  Vcvv 3415  cdif 3872  cin 3874  wss 3875  {csn 4550  {cpr 4552   cuni 4828   class class class wbr 5062  cmpt 5144  dom cdm 5560  Fun wfun 6383  wf 6385  cfv 6389  (class class class)co 7222  m cmap 8517  pm cpm 8518  cc 10740  cr 10741  0cc0 10742  1c1 10743   + caddc 10745  cmin 11075   / cdiv 11502  cn 11843  0cn0 12103  cuz 12451  ...cfz 13108  ..^cfzo 13251  cexp 13648  t crest 16938  TopOpenctopn 16939  fldccnfld 20376  Topctop 21803  TopOnctopon 21820  intcnt 21927   lim climc 24772   D cdv 24773   D𝑛 cdvn 24774   Tayl ctayl 25258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5188  ax-sep 5201  ax-nul 5208  ax-pow 5267  ax-pr 5331  ax-un 7532  ax-inf2 9269  ax-cnex 10798  ax-resscn 10799  ax-1cn 10800  ax-icn 10801  ax-addcl 10802  ax-addrcl 10803  ax-mulcl 10804  ax-mulrcl 10805  ax-mulcom 10806  ax-addass 10807  ax-mulass 10808  ax-distr 10809  ax-i2m1 10810  ax-1ne0 10811  ax-1rid 10812  ax-rnegex 10813  ax-rrecex 10814  ax-cnre 10815  ax-pre-lttri 10816  ax-pre-lttrn 10817  ax-pre-ltadd 10818  ax-pre-mulgt0 10819  ax-pre-sup 10820  ax-addf 10821  ax-mulf 10822
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3417  df-sbc 3704  df-csb 3821  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-pss 3894  df-nul 4247  df-if 4449  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4829  df-int 4869  df-iun 4915  df-iin 4916  df-br 5063  df-opab 5125  df-mpt 5145  df-tr 5171  df-id 5464  df-eprel 5469  df-po 5477  df-so 5478  df-fr 5518  df-se 5519  df-we 5520  df-xp 5566  df-rel 5567  df-cnv 5568  df-co 5569  df-dm 5570  df-rn 5571  df-res 5572  df-ima 5573  df-pred 6169  df-ord 6225  df-on 6226  df-lim 6227  df-suc 6228  df-iota 6347  df-fun 6391  df-fn 6392  df-f 6393  df-f1 6394  df-fo 6395  df-f1o 6396  df-fv 6397  df-isom 6398  df-riota 7179  df-ov 7225  df-oprab 7226  df-mpo 7227  df-of 7478  df-om 7654  df-1st 7770  df-2nd 7771  df-supp 7913  df-wrecs 8056  df-recs 8117  df-rdg 8155  df-1o 8211  df-2o 8212  df-er 8400  df-map 8519  df-pm 8520  df-ixp 8588  df-en 8636  df-dom 8637  df-sdom 8638  df-fin 8639  df-fsupp 8999  df-fi 9040  df-sup 9071  df-inf 9072  df-oi 9139  df-card 9568  df-pnf 10882  df-mnf 10883  df-xr 10884  df-ltxr 10885  df-le 10886  df-sub 11077  df-neg 11078  df-div 11503  df-nn 11844  df-2 11906  df-3 11907  df-4 11908  df-5 11909  df-6 11910  df-7 11911  df-8 11912  df-9 11913  df-n0 12104  df-xnn0 12176  df-z 12190  df-dec 12307  df-uz 12452  df-q 12558  df-rp 12600  df-xneg 12717  df-xadd 12718  df-xmul 12719  df-icc 12955  df-fz 13109  df-fzo 13252  df-seq 13588  df-exp 13649  df-fac 13853  df-hash 13910  df-cj 14675  df-re 14676  df-im 14677  df-sqrt 14811  df-abs 14812  df-clim 15062  df-sum 15263  df-struct 16713  df-sets 16730  df-slot 16748  df-ndx 16758  df-base 16774  df-ress 16798  df-plusg 16828  df-mulr 16829  df-starv 16830  df-sca 16831  df-vsca 16832  df-ip 16833  df-tset 16834  df-ple 16835  df-ds 16837  df-unif 16838  df-hom 16839  df-cco 16840  df-rest 16940  df-topn 16941  df-0g 16959  df-gsum 16960  df-topgen 16961  df-pt 16962  df-prds 16965  df-xrs 17020  df-qtop 17025  df-imas 17026  df-xps 17028  df-mre 17102  df-mrc 17103  df-acs 17105  df-mgm 18127  df-sgrp 18176  df-mnd 18187  df-submnd 18232  df-grp 18381  df-minusg 18382  df-mulg 18502  df-cntz 18724  df-cmn 19185  df-abl 19186  df-mgp 19518  df-ur 19530  df-ring 19577  df-cring 19578  df-psmet 20368  df-xmet 20369  df-met 20370  df-bl 20371  df-mopn 20372  df-fbas 20373  df-fg 20374  df-cnfld 20377  df-top 21804  df-topon 21821  df-topsp 21843  df-bases 21856  df-cld 21929  df-ntr 21930  df-cls 21931  df-nei 22008  df-lp 22046  df-perf 22047  df-cn 22137  df-cnp 22138  df-haus 22225  df-tx 22472  df-hmeo 22665  df-fil 22756  df-fm 22848  df-flim 22849  df-flf 22850  df-tsms 23037  df-xms 23231  df-ms 23232  df-tms 23233  df-cncf 23788  df-limc 24776  df-dv 24777  df-dvn 24778  df-tayl 25260
This theorem is referenced by:  taylth  25280
  Copyright terms: Public domain W3C validator