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

Theorem taylthlem1 26302
Description: Lemma for taylth 26305. 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 26305 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 13558 . . . 4 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
31, 2sylib 217 . . 3 (𝜑𝑁 ∈ (1...𝑁))
4 oveq2 7423 . . . . . . . . . . . 12 (𝑚 = 1 → (𝑁𝑚) = (𝑁 − 1))
54fveq2d 6896 . . . . . . . . . . 11 (𝑚 = 1 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
65fveq1d 6894 . . . . . . . . . 10 (𝑚 = 1 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
74fveq2d 6896 . . . . . . . . . . 11 (𝑚 = 1 → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 1)))
87fveq1d 6894 . . . . . . . . . 10 (𝑚 = 1 → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
96, 8oveq12d 7433 . . . . . . . . 9 (𝑚 = 1 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
10 oveq2 7423 . . . . . . . . 9 (𝑚 = 1 → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑1))
119, 10oveq12d 7433 . . . . . . . 8 (𝑚 = 1 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1)))
1211mpteq2dv 5245 . . . . . . 7 (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))))
1312oveq1d 7430 . . . . . 6 (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵))
1413eleq2d 2815 . . . . 5 (𝑚 = 1 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵)))
1514imbi2d 340 . . . 4 (𝑚 = 1 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵))))
16 oveq2 7423 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (𝑁𝑚) = (𝑁𝑛))
1716fveq2d 6896 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁𝑛)))
1817fveq1d 6894 . . . . . . . . . . 11 (𝑚 = 𝑛 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥))
1916fveq2d 6896 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑛)))
2019fveq1d 6894 . . . . . . . . . . 11 (𝑚 = 𝑛 → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥))
2118, 20oveq12d 7433 . . . . . . . . . 10 (𝑚 = 𝑛 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)))
22 oveq2 7423 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑𝑛))
2321, 22oveq12d 7433 . . . . . . . . 9 (𝑚 = 𝑛 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛)))
2423mpteq2dv 5245 . . . . . . . 8 (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛))))
25 fveq2 6892 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦))
26 fveq2 6892 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦))
2725, 26oveq12d 7433 . . . . . . . . . 10 (𝑥 = 𝑦 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)))
28 oveq1 7422 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥𝐵) = (𝑦𝐵))
2928oveq1d 7430 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥𝐵)↑𝑛) = ((𝑦𝐵)↑𝑛))
3027, 29oveq12d 7433 . . . . . . . . 9 (𝑥 = 𝑦 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛)) = (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛)))
3130cbvmptv 5256 . . . . . . . 8 (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑥)) / ((𝑥𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛)))
3224, 31eqtrdi 2784 . . . . . . 7 (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))))
3332oveq1d 7430 . . . . . 6 (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵))
3433eleq2d 2815 . . . . 5 (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵)))
3534imbi2d 340 . . . 4 (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵))))
36 oveq2 7423 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (𝑁𝑚) = (𝑁 − (𝑛 + 1)))
3736fveq2d 6896 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1))))
3837fveq1d 6894 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥))
3936fveq2d 6896 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1))))
4039fveq1d 6894 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))
4138, 40oveq12d 7433 . . . . . . . . 9 (𝑚 = (𝑛 + 1) → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)))
42 oveq2 7423 . . . . . . . . 9 (𝑚 = (𝑛 + 1) → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑(𝑛 + 1)))
4341, 42oveq12d 7433 . . . . . . . 8 (𝑚 = (𝑛 + 1) → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1))))
4443mpteq2dv 5245 . . . . . . 7 (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))))
4544oveq1d 7430 . . . . . 6 (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))
4645eleq2d 2815 . . . . 5 (𝑚 = (𝑛 + 1) → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵)))
4746imbi2d 340 . . . 4 (𝑚 = (𝑛 + 1) → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵))))
48 oveq2 7423 . . . . . . . . . . . 12 (𝑚 = 𝑁 → (𝑁𝑚) = (𝑁𝑁))
4948fveq2d 6896 . . . . . . . . . . 11 (𝑚 = 𝑁 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁𝑁)))
5049fveq1d 6894 . . . . . . . . . 10 (𝑚 = 𝑁 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥))
5148fveq2d 6896 . . . . . . . . . . 11 (𝑚 = 𝑁 → ((ℂ D𝑛 𝑇)‘(𝑁𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑁)))
5251fveq1d 6894 . . . . . . . . . 10 (𝑚 = 𝑁 → (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥))
5350, 52oveq12d 7433 . . . . . . . . 9 (𝑚 = 𝑁 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)))
54 oveq2 7423 . . . . . . . . 9 (𝑚 = 𝑁 → ((𝑥𝐵)↑𝑚) = ((𝑥𝐵)↑𝑁))
5553, 54oveq12d 7433 . . . . . . . 8 (𝑚 = 𝑁 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁)))
5655mpteq2dv 5245 . . . . . . 7 (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))))
5756oveq1d 7430 . . . . . 6 (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵))
5857eleq2d 2815 . . . . 5 (𝑚 = 𝑁 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵)))
5958imbi2d 340 . . . 4 (𝑚 = 𝑁 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑚))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑚))‘𝑥)) / ((𝑥𝐵)↑𝑚))) lim 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵))))
60 taylthlem1.b . . . . . . . . . . . 12 (𝜑𝐵𝐴)
61 fveq2 6892 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵))
62 fveq2 6892 . . . . . . . . . . . . . 14 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) = (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵))
6361, 62oveq12d 7433 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)))
64 eqid 2728 . . . . . . . . . . . . 13 (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))) = (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
65 ovex 7448 . . . . . . . . . . . . 13 ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)) ∈ V
6663, 64, 65fvmpt 7000 . . . . . . . . . . . 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 12557 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℕ0)
72 nn0uz 12889 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
7371, 72eleqtrdi 2839 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (ℤ‘0))
74 eluzfz2b 13537 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘0) ↔ 𝑁 ∈ (0...𝑁))
7573, 74sylib 217 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (0...𝑁))
76 taylthlem1.d . . . . . . . . . . . . . 14 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) = 𝐴)
7760, 76eleqtrrd 2832 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))
78 taylthlem1.t . . . . . . . . . . . . 13 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
7968, 69, 70, 75, 77, 78dvntaylp0 26301 . . . . . . . . . . . 12 (𝜑 → (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵))
8079oveq2d 7431 . . . . . . . . . . 11 (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)))
81 cnex 11214 . . . . . . . . . . . . . . . 16 ℂ ∈ V
8281a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℂ ∈ V)
83 elpm2r 8858 . . . . . . . . . . . . . . 15 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆))
8482, 68, 69, 70, 83syl22anc 838 . . . . . . . . . . . . . 14 (𝜑𝐹 ∈ (ℂ ↑pm 𝑆))
85 dvnf 25851 . . . . . . . . . . . . . 14 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ 𝑁 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ)
8668, 84, 71, 85syl3anc 1369 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ)
8786, 77ffvelcdmd 7090 . . . . . . . . . . . 12 (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ)
8887subidd 11584 . . . . . . . . . . 11 (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) = 0)
8967, 80, 883eqtrd 2772 . . . . . . . . . 10 (𝜑 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0)
90 funmpt 6586 . . . . . . . . . . 11 Fun (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
91 ovex 7448 . . . . . . . . . . . . 13 ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)) ∈ V
9291, 64dmmpti 6694 . . . . . . . . . . . 12 dom (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))) = 𝐴
9360, 92eleqtrrdi 2840 . . . . . . . . . . 11 (𝜑𝐵 ∈ dom (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))))
94 funbrfvb 6947 . . . . . . . . . . 11 ((Fun (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))) ∧ 𝐵 ∈ dom (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))) → (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0))
9590, 93, 94sylancr 586 . . . . . . . . . 10 (𝜑 → (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0))
9689, 95mpbid 231 . . . . . . . . 9 (𝜑𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0)
97 nnm1nn0 12538 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
981, 97syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 − 1) ∈ ℕ0)
99 dvnf 25851 . . . . . . . . . . . . . 14 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
10068, 84, 98, 99syl3anc 1369 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
101 dvnbss 25852 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0) → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
10268, 84, 98, 101syl3anc 1369 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
10369, 102fssdmd 6736 . . . . . . . . . . . . . . 15 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴)
104 fzo0end 13751 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
105 elfzofz 13675 . . . . . . . . . . . . . . . . . 18 ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁))
1061, 104, 1053syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 − 1) ∈ (0...𝑁))
107 dvn2bss 25854 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
10868, 84, 106, 107syl3anc 1369 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
10976, 108eqsstrrd 4018 . . . . . . . . . . . . . . 15 (𝜑𝐴 ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))
110103, 109eqssd 3996 . . . . . . . . . . . . . 14 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = 𝐴)
111110feq2d 6703 . . . . . . . . . . . . 13 (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ))
112100, 111mpbid 231 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)
113112ffvelcdmda 7089 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
11476feq2d 6703 . . . . . . . . . . . . 13 (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ))
11586, 114mpbid 231 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ)
116115ffvelcdmda 7089 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ)
1171nncnd 12253 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
118 1cnd 11234 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
119117, 118npcand 11600 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
120119fveq2d 6896 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D𝑛 𝐹)‘𝑁))
121 recnprss 25827 . . . . . . . . . . . . . . 15 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
12268, 121syl 17 . . . . . . . . . . . . . 14 (𝜑𝑆 ⊆ ℂ)
123 dvnp1 25849 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
124122, 84, 98, 123syl3anc 1369 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
125120, 124eqtr3d 2770 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
126115feqmptd 6962 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦)))
127112feqmptd 6962 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))
128127oveq2d 7431 . . . . . . . . . . . 12 (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))))
129125, 126, 1283eqtr3rd 2777 . . . . . . . . . . 11 (𝜑 → (𝑆 D (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦)))
13070, 122sstrd 3989 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℂ)
131130sselda 3979 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝑦 ∈ ℂ)
132 1nn0 12513 . . . . . . . . . . . . . . . 16 1 ∈ ℕ0
133132a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℕ0)
134 elpm2r 8858 . . . . . . . . . . . . . . . . . . . 20 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴𝑆)) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑pm 𝑆))
13582, 68, 112, 70, 134syl22anc 838 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑pm 𝑆))
136 dvn1 25850 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
137122, 135, 136syl2anc 583 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))))
138124, 120eqtr3d 2770 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁))
139137, 138eqtrd 2768 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D𝑛 𝐹)‘𝑁))
140139dmeqd 5903 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
14177, 140eleqtrrd 2832 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1))
142 eqid 2728 . . . . . . . . . . . . . . 15 (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵)
14368, 112, 70, 133, 141, 142taylpf 26294 . . . . . . . . . . . . . 14 (𝜑 → (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)
144118, 117pncan3d 11599 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 + (𝑁 − 1)) = 𝑁)
145144oveq1d 7430 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
14678, 145eqtr4id 2787 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))
147146oveq2d 7431 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℂ D𝑛 𝑇) = (ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)))
148147fveq1d 6894 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)))
149144fveq2d 6896 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁))
150149dmeqd 5903 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
15177, 150eleqtrrd 2832 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))))
15268, 69, 70, 98, 133, 151dvntaylp 26300 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵))
153148, 152eqtrd 2768 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵))
154153feq1d 6702 . . . . . . . . . . . . . 14 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔ (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ))
155143, 154mpbird 257 . . . . . . . . . . . . 13 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ)
156155ffvelcdmda 7089 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
157131, 156syldan 590 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
158 0nn0 12512 . . . . . . . . . . . . . . . 16 0 ∈ ℕ0
159158a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℕ0)
160 elpm2r 8858 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴𝑆)) → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆))
16182, 68, 115, 70, 160syl22anc 838 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆))
162 dvn0 25848 . . . . . . . . . . . . . . . . . 18 ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁))
163122, 161, 162syl2anc 583 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁))
164163dmeqd 5903 . . . . . . . . . . . . . . . 16 (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
16577, 164eleqtrrd 2832 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0))
166 eqid 2728 . . . . . . . . . . . . . . 15 (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵)
16768, 115, 70, 159, 165, 166taylpf 26294 . . . . . . . . . . . . . 14 (𝜑 → (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)
168117addlidd 11440 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (0 + 𝑁) = 𝑁)
169168oveq1d 7430 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
170169, 78eqtr4di 2786 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇)
171170oveq2d 7431 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℂ D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D𝑛 𝑇))
172171fveq1d 6894 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D𝑛 𝑇)‘𝑁))
173168fveq2d 6896 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D𝑛 𝐹)‘𝑁))
174173dmeqd 5903 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
17577, 174eleqtrrd 2832 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)))
17668, 69, 70, 71, 159, 175dvntaylp 26300 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℂ D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵))
177172, 176eqtr3d 2770 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵))
178177feq1d 6702 . . . . . . . . . . . . . 14 (𝜑 → (((ℂ D𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ))
179167, 178mpbird 257 . . . . . . . . . . . . 13 (𝜑 → ((ℂ D𝑛 𝑇)‘𝑁):ℂ⟶ℂ)
180179ffvelcdmda 7089 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
181131, 180syldan 590 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
182122sselda 3979 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → 𝑦 ∈ ℂ)
183182, 156syldan 590 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
184182, 180syldan 590 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
185 eqid 2728 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
186185cnfldtopon 24693 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
187 toponmax 22822 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
188186, 187mp1i 13 . . . . . . . . . . . . 13 (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
189 df-ss 3962 . . . . . . . . . . . . . 14 (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆)
190122, 189sylib 217 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∩ ℂ) = 𝑆)
191 ssid 4001 . . . . . . . . . . . . . . . . 17 ℂ ⊆ ℂ
192191a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ℂ ⊆ ℂ)
193 mapsspm 8889 . . . . . . . . . . . . . . . . 17 (ℂ ↑m ℂ) ⊆ (ℂ ↑pm ℂ)
19468, 69, 70, 71, 77, 78taylpf 26294 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:ℂ⟶ℂ)
19581, 81elmap 8884 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ (ℂ ↑m ℂ) ↔ 𝑇:ℂ⟶ℂ)
196194, 195sylibr 233 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ (ℂ ↑m ℂ))
197193, 196sselid 3977 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ (ℂ ↑pm ℂ))
198 dvnp1 25849 . . . . . . . . . . . . . . . 16 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ) ∧ (𝑁 − 1) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))))
199192, 197, 98, 198syl3anc 1369 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))))
200119fveq2d 6896 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ D𝑛 𝑇)‘𝑁))
201199, 200eqtr3d 2770 . . . . . . . . . . . . . 14 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ D𝑛 𝑇)‘𝑁))
202155feqmptd 6962 . . . . . . . . . . . . . . 15 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
203202oveq2d 7431 . . . . . . . . . . . . . 14 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))
204179feqmptd 6962 . . . . . . . . . . . . . 14 (𝜑 → ((ℂ D𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
205201, 203, 2043eqtr3d 2776 . . . . . . . . . . . . 13 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
206185, 68, 188, 190, 156, 180, 205dvmptres3 25882 . . . . . . . . . . . 12 (𝜑 → (𝑆 D (𝑦𝑆 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦𝑆 ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
207 eqid 2728 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
208 resttopon 23059 . . . . . . . . . . . . . . . 16 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
209186, 122, 208sylancr 586 . . . . . . . . . . . . . . 15 (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
210 topontop 22809 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
211209, 210syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
212 toponuni 22810 . . . . . . . . . . . . . . . 16 (((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
213209, 212syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
21470, 213sseqtrd 4019 . . . . . . . . . . . . . 14 (𝜑𝐴 ((TopOpen‘ℂfld) ↾t 𝑆))
215 eqid 2728 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
216215ntrss2 22955 . . . . . . . . . . . . . 14 ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝐴 ((TopOpen‘ℂfld) ↾t 𝑆)) → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴)
217211, 214, 216syl2anc 583 . . . . . . . . . . . . 13 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴)
218138dmeqd 5903 . . . . . . . . . . . . . . 15 (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁))
219218, 76eqtrd 2768 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = 𝐴)
220122, 112, 70, 207, 185dvbssntr 25823 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) ⊆ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴))
221219, 220eqsstrrd 4018 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴))
222217, 221eqssd 3996 . . . . . . . . . . . 12 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) = 𝐴)
22368, 183, 184, 206, 70, 207, 185, 222dvmptres2 25888 . . . . . . . . . . 11 (𝜑 → (𝑆 D (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))
22468, 113, 116, 129, 157, 181, 223dvmptsub 25893 . . . . . . . . . 10 (𝜑 → (𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦))))
225224breqd 5154 . . . . . . . . 9 (𝜑 → (𝐵(𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛 𝑇)‘𝑁)‘𝑦)))0))
22696, 225mpbird 257 . . . . . . . 8 (𝜑𝐵(𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0)
227 eqid 2728 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵)))
228113, 157subcld 11596 . . . . . . . . . 10 ((𝜑𝑦𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ)
229228fmpttd 7120 . . . . . . . . 9 (𝜑 → (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ)
230207, 185, 227, 122, 229, 70eldv 25821 . . . . . . . 8 (𝜑 → (𝐵(𝑆 D (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ (𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵))))
231226, 230mpbid 231 . . . . . . 7 (𝜑 → (𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵)))
232231simprd 495 . . . . . 6 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵))
233 eldifi 4123 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐴)
234 fveq2 6892 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
235 fveq2 6892 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
236234, 235oveq12d 7433 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
237 eqid 2728 . . . . . . . . . . . . 13 (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
238 ovex 7448 . . . . . . . . . . . . 13 ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V
239236, 237, 238fvmpt 7000 . . . . . . . . . . . 12 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
240 fveq2 6892 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
241 fveq2 6892 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵))
242240, 241oveq12d 7433 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
243 ovex 7448 . . . . . . . . . . . . . . 15 ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V
244242, 237, 243fvmpt 7000 . . . . . . . . . . . . . 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 26301 . . . . . . . . . . . . . 14 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
247246oveq2d 7431 . . . . . . . . . . . . 13 (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)))
248112, 60ffvelcdmd 7090 . . . . . . . . . . . . . 14 (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ)
249248subidd 11584 . . . . . . . . . . . . 13 (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0)
250245, 247, 2493eqtrd 2772 . . . . . . . . . . . 12 (𝜑 → ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0)
251239, 250oveqan12rd 7435 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0))
252112ffvelcdmda 7089 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
253130sselda 3979 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑥 ∈ ℂ)
254155ffvelcdmda 7089 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
255253, 254syldan 590 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
256252, 255subcld 11596 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ)
257256subid1d 11585 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
258251, 257eqtr2d 2769 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
259233, 258sylan2 592 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
260130ssdifssd 4139 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
261260sselda 3979 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
262130, 60sseldd 3980 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
263262adantr 480 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
264261, 263subcld 11596 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℂ)
265264exp1d 14132 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑1) = (𝑥𝐵))
266259, 265oveq12d 7433 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1)) = ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵)))
267266mpteq2dva 5243 . . . . . . 7 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))))
268267oveq1d 7430 . . . . . 6 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥𝐵)↑1))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥𝐵))) lim 𝐵))
269232, 268eleqtrrd 2832 . . . . 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 456 . . . . . 6 ((𝜑𝑛 ∈ (1..^𝑁)) → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑛))‘𝑦)) / ((𝑦𝐵)↑𝑛))) lim 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑛 + 1)))) lim 𝐵)))
273272expcom 413 . . . . 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 13777 . . 3 (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵)))
2763, 275mpcom 38 . 2 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵))
277117subidd 11584 . . . . . . . . . 10 (𝜑 → (𝑁𝑁) = 0)
278277fveq2d 6896 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑁)) = ((𝑆 D𝑛 𝐹)‘0))
279 dvn0 25848 . . . . . . . . . 10 ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
280122, 84, 279syl2anc 583 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
281278, 280eqtrd 2768 . . . . . . . 8 (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁𝑁)) = 𝐹)
282281fveq1d 6894 . . . . . . 7 (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) = (𝐹𝑥))
283277fveq2d 6896 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑁)) = ((ℂ D𝑛 𝑇)‘0))
284 dvn0 25848 . . . . . . . . . 10 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ)) → ((ℂ D𝑛 𝑇)‘0) = 𝑇)
285191, 197, 284sylancr 586 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘0) = 𝑇)
286283, 285eqtrd 2768 . . . . . . . 8 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑁)) = 𝑇)
287286fveq1d 6894 . . . . . . 7 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥) = (𝑇𝑥))
288282, 287oveq12d 7433 . . . . . 6 (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) = ((𝐹𝑥) − (𝑇𝑥)))
289288oveq1d 7430 . . . . 5 (𝜑 → (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁)) = (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁)))
290289mpteq2dv 5245 . . . 4 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁))))
291 taylthlem1.r . . . 4 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑥) − (𝑇𝑥)) / ((𝑥𝐵)↑𝑁)))
292290, 291eqtr4di 2786 . . 3 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) = 𝑅)
293292oveq1d 7430 . 2 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁𝑁))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑁))‘𝑥)) / ((𝑥𝐵)↑𝑁))) lim 𝐵) = (𝑅 lim 𝐵))
294276, 293eleqtrd 2831 1 (𝜑 → 0 ∈ (𝑅 lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1534  wcel 2099  Vcvv 3470  cdif 3942  cin 3944  wss 3945  {csn 4625  {cpr 4627   cuni 4904   class class class wbr 5143  cmpt 5226  dom cdm 5673  Fun wfun 6537  wf 6539  cfv 6543  (class class class)co 7415  m cmap 8839  pm cpm 8840  cc 11131  cr 11132  0cc0 11133  1c1 11134   + caddc 11136  cmin 11469   / cdiv 11896  cn 12237  0cn0 12497  cuz 12847  ...cfz 13511  ..^cfzo 13654  cexp 14053  t crest 17396  TopOpenctopn 17397  fldccnfld 21273  Topctop 22789  TopOnctopon 22806  intcnt 22915   lim climc 25785   D cdv 25786   D𝑛 cdvn 25787   Tayl ctayl 26281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211  ax-addf 11212
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-iin 4995  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-of 7680  df-om 7866  df-1st 7988  df-2nd 7989  df-supp 8161  df-frecs 8281  df-wrecs 8312  df-recs 8386  df-rdg 8425  df-1o 8481  df-2o 8482  df-er 8719  df-map 8841  df-pm 8842  df-ixp 8911  df-en 8959  df-dom 8960  df-sdom 8961  df-fin 8962  df-fsupp 9381  df-fi 9429  df-sup 9460  df-inf 9461  df-oi 9528  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-4 12302  df-5 12303  df-6 12304  df-7 12305  df-8 12306  df-9 12307  df-n0 12498  df-xnn0 12570  df-z 12584  df-dec 12703  df-uz 12848  df-q 12958  df-rp 13002  df-xneg 13119  df-xadd 13120  df-xmul 13121  df-icc 13358  df-fz 13512  df-fzo 13655  df-seq 13994  df-exp 14054  df-fac 14260  df-hash 14317  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-clim 15459  df-sum 15660  df-struct 17110  df-sets 17127  df-slot 17145  df-ndx 17157  df-base 17175  df-ress 17204  df-plusg 17240  df-mulr 17241  df-starv 17242  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ds 17249  df-unif 17250  df-hom 17251  df-cco 17252  df-rest 17398  df-topn 17399  df-0g 17417  df-gsum 17418  df-topgen 17419  df-pt 17420  df-prds 17423  df-xrs 17478  df-qtop 17483  df-imas 17484  df-xps 17486  df-mre 17560  df-mrc 17561  df-acs 17563  df-mgm 18594  df-sgrp 18673  df-mnd 18689  df-submnd 18735  df-grp 18887  df-minusg 18888  df-mulg 19018  df-cntz 19262  df-cmn 19731  df-abl 19732  df-mgp 20069  df-ur 20116  df-ring 20169  df-cring 20170  df-psmet 21265  df-xmet 21266  df-met 21267  df-bl 21268  df-mopn 21269  df-fbas 21270  df-fg 21271  df-cnfld 21274  df-top 22790  df-topon 22807  df-topsp 22829  df-bases 22843  df-cld 22917  df-ntr 22918  df-cls 22919  df-nei 22996  df-lp 23034  df-perf 23035  df-cn 23125  df-cnp 23126  df-haus 23213  df-tx 23460  df-hmeo 23653  df-fil 23744  df-fm 23836  df-flim 23837  df-flf 23838  df-tsms 24025  df-xms 24220  df-ms 24221  df-tms 24222  df-cncf 24792  df-limc 25789  df-dv 25790  df-dvn 25791  df-tayl 26283
This theorem is referenced by:  taylth  26305
  Copyright terms: Public domain W3C validator