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

Theorem taylthlem2 24364
Description: Lemma for taylth 24365. (Contributed by Mario Carneiro, 1-Jan-2017.)
Hypotheses
Ref Expression
taylth.f (𝜑𝐹:𝐴⟶ℝ)
taylth.a (𝜑𝐴 ⊆ ℝ)
taylth.d (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)
taylth.n (𝜑𝑁 ∈ ℕ)
taylth.b (𝜑𝐵𝐴)
taylth.t 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)
taylthlem2.m (𝜑𝑀 ∈ (1..^𝑁))
taylthlem2.i (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀))) lim 𝐵))
Assertion
Ref Expression
taylthlem2 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))) lim 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝑀   𝑥,𝑇   𝑥,𝑁   𝜑,𝑥

Proof of Theorem taylthlem2
Dummy variables 𝑦 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 taylth.a . . 3 (𝜑𝐴 ⊆ ℝ)
2 taylth.f . . . . . . . 8 (𝜑𝐹:𝐴⟶ℝ)
3 fz1ssfz0 12678 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
4 taylthlem2.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ (1..^𝑁))
5 fzofzp1 12808 . . . . . . . . . . . 12 (𝑀 ∈ (1..^𝑁) → (𝑀 + 1) ∈ (1...𝑁))
64, 5syl 17 . . . . . . . . . . 11 (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
73, 6sseldi 3807 . . . . . . . . . 10 (𝜑 → (𝑀 + 1) ∈ (0...𝑁))
8 fznn0sub2 12689 . . . . . . . . . 10 ((𝑀 + 1) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
97, 8syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
10 elfznn0 12675 . . . . . . . . 9 ((𝑁 − (𝑀 + 1)) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
119, 10syl 17 . . . . . . . 8 (𝜑 → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
12 dvnfre 23951 . . . . . . . 8 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
132, 1, 11, 12syl3anc 1483 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
14 reelprrecn 10322 . . . . . . . . . . . 12 ℝ ∈ {ℝ, ℂ}
1514a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ {ℝ, ℂ})
16 cnex 10311 . . . . . . . . . . . . 13 ℂ ∈ V
1716a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ∈ V)
18 reex 10321 . . . . . . . . . . . . 13 ℝ ∈ V
1918a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
20 ax-resscn 10287 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
21 fss 6278 . . . . . . . . . . . . 13 ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
222, 20, 21sylancl 576 . . . . . . . . . . . 12 (𝜑𝐹:𝐴⟶ℂ)
23 elpm2r 8119 . . . . . . . . . . . 12 (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
2417, 19, 22, 1, 23syl22anc 858 . . . . . . . . . . 11 (𝜑𝐹 ∈ (ℂ ↑pm ℝ))
25 dvnbss 23927 . . . . . . . . . . 11 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
2615, 24, 11, 25syl3anc 1483 . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
272, 26fssdmd 6280 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ 𝐴)
28 taylth.d . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)
29 dvn2bss 23929 . . . . . . . . . . 11 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3015, 24, 9, 29syl3anc 1483 . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3128, 30eqsstr3d 3848 . . . . . . . . 9 (𝜑𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3227, 31eqssd 3826 . . . . . . . 8 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = 𝐴)
3332feq2d 6251 . . . . . . 7 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ))
3413, 33mpbid 223 . . . . . 6 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ)
3534ffvelrnda 6590 . . . . 5 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
361sselda 3809 . . . . . 6 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ)
37 fvres 6436 . . . . . . . 8 (𝑦 ∈ ℝ → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
3837adantl 469 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
39 resubdrg 20182 . . . . . . . . . . . 12 (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
4039simpli 472 . . . . . . . . . . 11 ℝ ∈ (SubRing‘ℂfld)
4140a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ (SubRing‘ℂfld))
42 taylth.n . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
4342nnnn0d 11636 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
44 taylth.b . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
4544, 28eleqtrrd 2899 . . . . . . . . . . . 12 (𝜑𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
46 taylth.t . . . . . . . . . . . 12 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)
471, 44sseldd 3810 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
482adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐹:𝐴⟶ℝ)
491adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐴 ⊆ ℝ)
50 elfznn0 12675 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
5150adantl 469 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
52 dvnfre 23951 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑘 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
5348, 49, 51, 52syl3anc 1483 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
5414a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → ℝ ∈ {ℝ, ℂ})
5524adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐹 ∈ (ℂ ↑pm ℝ))
56 simpr 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁))
57 dvn2bss 23929 . . . . . . . . . . . . . . . 16 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
5854, 55, 56, 57syl3anc 1483 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
5945adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
6058, 59sseldd 3810 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑘))
6153, 60ffvelrnd 6591 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝑁)) → (((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℝ)
62 faccl 13309 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
6351, 62syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
6461, 63nndivred 11366 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝑁)) → ((((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℝ)
6515, 22, 1, 43, 45, 46, 41, 47, 64taylply2 24358 . . . . . . . . . . 11 (𝜑 → (𝑇 ∈ (Poly‘ℝ) ∧ (deg‘𝑇) ≤ 𝑁))
6665simpld 484 . . . . . . . . . 10 (𝜑𝑇 ∈ (Poly‘ℝ))
67 dvnply2 24278 . . . . . . . . . 10 ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
6841, 66, 11, 67syl3anc 1483 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
69 plyreres 24274 . . . . . . . . 9 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
7068, 69syl 17 . . . . . . . 8 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
7170ffvelrnda 6590 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) ∈ ℝ)
7238, 71eqeltrrd 2897 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
7336, 72syldan 581 . . . . 5 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
7435, 73resubcld 10752 . . . 4 ((𝜑𝑦𝐴) → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ ℝ)
7574fmpttd 6616 . . 3 (𝜑 → (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))):𝐴⟶ℝ)
7647adantr 468 . . . . . 6 ((𝜑𝑦𝐴) → 𝐵 ∈ ℝ)
7736, 76resubcld 10752 . . . . 5 ((𝜑𝑦𝐴) → (𝑦𝐵) ∈ ℝ)
78 elfzouz 12717 . . . . . . . . . 10 (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (ℤ‘1))
794, 78syl 17 . . . . . . . . 9 (𝜑𝑀 ∈ (ℤ‘1))
80 nnuz 11960 . . . . . . . . 9 ℕ = (ℤ‘1)
8179, 80syl6eleqr 2907 . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
8281nnnn0d 11636 . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
8382adantr 468 . . . . . 6 ((𝜑𝑦𝐴) → 𝑀 ∈ ℕ0)
84 1nn0 11594 . . . . . . 7 1 ∈ ℕ0
8584a1i 11 . . . . . 6 ((𝜑𝑦𝐴) → 1 ∈ ℕ0)
8683, 85nn0addcld 11640 . . . . 5 ((𝜑𝑦𝐴) → (𝑀 + 1) ∈ ℕ0)
8777, 86reexpcld 13267 . . . 4 ((𝜑𝑦𝐴) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℝ)
8887fmpttd 6616 . . 3 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℝ)
89 retop 22798 . . . . . 6 (topGen‘ran (,)) ∈ Top
90 uniretop 22799 . . . . . . 7 ℝ = (topGen‘ran (,))
9190ntrss2 21095 . . . . . 6 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
9289, 1, 91sylancr 577 . . . . 5 (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
9342nncnd 11332 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
9481nncnd 11332 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℂ)
95 1cnd 10329 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
9693, 94, 95nppcan2d 10712 . . . . . . . . . 10 (𝜑 → ((𝑁 − (𝑀 + 1)) + 1) = (𝑁𝑀))
9796fveq2d 6421 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
9820a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
99 dvnp1 23924 . . . . . . . . . 10 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
10098, 24, 11, 99syl3anc 1483 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
10197, 100eqtr3d 2853 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
102101dmeqd 5540 . . . . . . 7 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
103 fzonnsub 12736 . . . . . . . . . . . 12 (𝑀 ∈ (1..^𝑁) → (𝑁𝑀) ∈ ℕ)
1044, 103syl 17 . . . . . . . . . . 11 (𝜑 → (𝑁𝑀) ∈ ℕ)
105104nnnn0d 11636 . . . . . . . . . 10 (𝜑 → (𝑁𝑀) ∈ ℕ0)
106 dvnbss 23927 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ dom 𝐹)
10715, 24, 105, 106syl3anc 1483 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ dom 𝐹)
1082, 107fssdmd 6280 . . . . . . . 8 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ 𝐴)
109 elfzofz 12728 . . . . . . . . . . . . 13 (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (1...𝑁))
1104, 109syl 17 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (1...𝑁))
1113, 110sseldi 3807 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑁))
112 fznn0sub2 12689 . . . . . . . . . . 11 (𝑀 ∈ (0...𝑁) → (𝑁𝑀) ∈ (0...𝑁))
113111, 112syl 17 . . . . . . . . . 10 (𝜑 → (𝑁𝑀) ∈ (0...𝑁))
114 dvn2bss 23929 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
11515, 24, 113, 114syl3anc 1483 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
11628, 115eqsstr3d 3848 . . . . . . . 8 (𝜑𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
117108, 116eqssd 3826 . . . . . . 7 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = 𝐴)
118102, 117eqtr3d 2853 . . . . . 6 (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴)
119 fss 6278 . . . . . . . 8 ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
12034, 20, 119sylancl 576 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
121 eqid 2817 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
122121tgioo2 22839 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
12398, 120, 1, 122, 121dvbssntr 23900 . . . . . 6 (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
124118, 123eqsstr3d 3848 . . . . 5 (𝜑𝐴 ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
12592, 124eqssd 3826 . . . 4 (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)
12690isopn3 21104 . . . . 5 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
12789, 1, 126sylancr 577 . . . 4 (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
128125, 127mpbird 248 . . 3 (𝜑𝐴 ∈ (topGen‘ran (,)))
129 eqid 2817 . . 3 (𝐴 ∖ {𝐵}) = (𝐴 ∖ {𝐵})
130 difss 3947 . . . 4 (𝐴 ∖ {𝐵}) ⊆ 𝐴
13135recnd 10362 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
132 dvnf 23926 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ)
13315, 24, 105, 132syl3anc 1483 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ)
134117feq2d 6251 . . . . . . . . 9 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℂ))
135133, 134mpbid 223 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℂ)
136135ffvelrnda 6590 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
137 dvnfre 23951 . . . . . . . . . . 11 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ)
1382, 1, 105, 137syl3anc 1483 . . . . . . . . . 10 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ)
139117feq2d 6251 . . . . . . . . . 10 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℝ))
140138, 139mpbid 223 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℝ)
141140feqmptd 6479 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦)))
14234feqmptd 6479 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
143142oveq2d 6899 . . . . . . . 8 (𝜑 → (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = (ℝ D (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
144101, 141, 1433eqtr3rd 2860 . . . . . . 7 (𝜑 → (ℝ D (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦)))
14573recnd 10362 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
146 fvexd 6432 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ V)
14772recnd 10362 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
148 recn 10320 . . . . . . . . 9 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
149 dvnply2 24278 . . . . . . . . . . . 12 ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ))
15041, 66, 105, 149syl3anc 1483 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ))
151 plyf 24190 . . . . . . . . . . 11 (((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)):ℂ⟶ℂ)
152150, 151syl 17 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)):ℂ⟶ℂ)
153152ffvelrnda 6590 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
154148, 153sylan2 582 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
155121cnfldtopon 22819 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
156 toponmax 20964 . . . . . . . . . 10 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
157155, 156mp1i 13 . . . . . . . . 9 (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
158 df-ss 3794 . . . . . . . . . 10 (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
15998, 158sylib 209 . . . . . . . . 9 (𝜑 → (ℝ ∩ ℂ) = ℝ)
160 plyf 24190 . . . . . . . . . . 11 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
16168, 160syl 17 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
162161ffvelrnda 6590 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
16396fveq2d 6421 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑀)))
164 ssid 3831 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
165164a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ⊆ ℂ)
166 mapsspm 8135 . . . . . . . . . . . . 13 (ℂ ↑𝑚 ℂ) ⊆ (ℂ ↑pm ℂ)
167 plyf 24190 . . . . . . . . . . . . . . 15 (𝑇 ∈ (Poly‘ℝ) → 𝑇:ℂ⟶ℂ)
16866, 167syl 17 . . . . . . . . . . . . . 14 (𝜑𝑇:ℂ⟶ℂ)
16916, 16elmap 8130 . . . . . . . . . . . . . 14 (𝑇 ∈ (ℂ ↑𝑚 ℂ) ↔ 𝑇:ℂ⟶ℂ)
170168, 169sylibr 225 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ (ℂ ↑𝑚 ℂ))
171166, 170sseldi 3807 . . . . . . . . . . . 12 (𝜑𝑇 ∈ (ℂ ↑pm ℂ))
172 dvnp1 23924 . . . . . . . . . . . 12 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
173165, 171, 11, 172syl3anc 1483 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
174163, 173eqtr3d 2853 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
175152feqmptd 6479 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
176161feqmptd 6479 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
177176oveq2d 6899 . . . . . . . . . 10 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
178174, 175, 1773eqtr3rd 2860 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
179121, 15, 157, 159, 162, 153, 178dvmptres3 23955 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
18015, 147, 154, 179, 1, 122, 121, 128dvmptres 23962 . . . . . . 7 (𝜑 → (ℝ D (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
18115, 131, 136, 144, 145, 146, 180dvmptsub 23966 . . . . . 6 (𝜑 → (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))))
182181dmeqd 5540 . . . . 5 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = dom (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))))
183 ovex 6915 . . . . . 6 ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)) ∈ V
184 eqid 2817 . . . . . 6 (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
185183, 184dmmpti 6243 . . . . 5 dom (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))) = 𝐴
186182, 185syl6eq 2867 . . . 4 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = 𝐴)
187130, 186syl5sseqr 3862 . . 3 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))))
188 simpr 473 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
18947adantr 468 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℂ) → 𝐵 ∈ ℝ)
190189recnd 10362 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝐵 ∈ ℂ)
191188, 190subcld 10686 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑦𝐵) ∈ ℂ)
19282adantr 468 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑀 ∈ ℕ0)
19384a1i 11 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 1 ∈ ℕ0)
194192, 193nn0addcld 11640 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
195191, 194expcld 13250 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
196148, 195sylan2 582 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
19794adantr 468 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑀 ∈ ℂ)
198 1cnd 10329 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 1 ∈ ℂ)
199197, 198addcld 10353 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℂ)
200191, 192expcld 13250 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → ((𝑦𝐵)↑𝑀) ∈ ℂ)
201199, 200mulcld 10354 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ ℂ)
202148, 201sylan2 582 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ ℂ)
20316prid2 4500 . . . . . . . . . . 11 ℂ ∈ {ℝ, ℂ}
204203a1i 11 . . . . . . . . . 10 (𝜑 → ℂ ∈ {ℝ, ℂ})
205 simpr 473 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
206 elfznn 12612 . . . . . . . . . . . . . 14 ((𝑀 + 1) ∈ (1...𝑁) → (𝑀 + 1) ∈ ℕ)
2076, 206syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀 + 1) ∈ ℕ)
208207nnnn0d 11636 . . . . . . . . . . . 12 (𝜑 → (𝑀 + 1) ∈ ℕ0)
209208adantr 468 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
210205, 209expcld 13250 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝑥↑(𝑀 + 1)) ∈ ℂ)
211 ovexd 6917 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → ((𝑀 + 1) · (𝑥𝑀)) ∈ V)
212204dvmptid 23956 . . . . . . . . . . . 12 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
213 0cnd 10327 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → 0 ∈ ℂ)
21447recnd 10362 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℂ)
215204, 214dvmptc 23957 . . . . . . . . . . . 12 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝐵)) = (𝑦 ∈ ℂ ↦ 0))
216204, 188, 198, 212, 190, 213, 215dvmptsub 23966 . . . . . . . . . . 11 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝐵))) = (𝑦 ∈ ℂ ↦ (1 − 0)))
217 1m0e1 11440 . . . . . . . . . . . 12 (1 − 0) = 1
218217mpteq2i 4946 . . . . . . . . . . 11 (𝑦 ∈ ℂ ↦ (1 − 0)) = (𝑦 ∈ ℂ ↦ 1)
219216, 218syl6eq 2867 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝐵))) = (𝑦 ∈ ℂ ↦ 1))
220 dvexp 23952 . . . . . . . . . . . 12 ((𝑀 + 1) ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
221207, 220syl 17 . . . . . . . . . . 11 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
22294, 95pncand 10687 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
223222oveq2d 6899 . . . . . . . . . . . . 13 (𝜑 → (𝑥↑((𝑀 + 1) − 1)) = (𝑥𝑀))
224223oveq2d 6899 . . . . . . . . . . . 12 (𝜑 → ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))) = ((𝑀 + 1) · (𝑥𝑀)))
225224mpteq2dv 4950 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥𝑀))))
226221, 225eqtrd 2851 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥𝑀))))
227 oveq1 6890 . . . . . . . . . 10 (𝑥 = (𝑦𝐵) → (𝑥↑(𝑀 + 1)) = ((𝑦𝐵)↑(𝑀 + 1)))
228 oveq1 6890 . . . . . . . . . . 11 (𝑥 = (𝑦𝐵) → (𝑥𝑀) = ((𝑦𝐵)↑𝑀))
229228oveq2d 6899 . . . . . . . . . 10 (𝑥 = (𝑦𝐵) → ((𝑀 + 1) · (𝑥𝑀)) = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
230204, 204, 191, 198, 210, 211, 219, 226, 227, 229dvmptco 23971 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1)))
231201mulid1d 10351 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1) = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
232231mpteq2dva 4949 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1)) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
233230, 232eqtrd 2851 . . . . . . . 8 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
234121, 15, 157, 159, 195, 201, 233dvmptres3 23955 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℝ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
23515, 196, 202, 234, 1, 122, 121, 128dvmptres 23962 . . . . . 6 (𝜑 → (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
236235dmeqd 5540 . . . . 5 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = dom (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
237 ovex 6915 . . . . . 6 ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ V
238 eqid 2817 . . . . . 6 (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) = (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
239237, 238dmmpti 6243 . . . . 5 dom (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) = 𝐴
240236, 239syl6eq 2867 . . . 4 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = 𝐴)
241130, 240syl5sseqr 3862 . . 3 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))))
24215, 22, 1, 9, 45, 46dvntaylp0 24362 . . . . . 6 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
243242oveq2d 6899 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
244120, 44ffvelrnd 6591 . . . . . 6 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) ∈ ℂ)
245244subidd 10674 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
246243, 245eqtrd 2851 . . . 4 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
247121subcn 22902 . . . . . . 7 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
248247a1i 11 . . . . . 6 (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
249 dvcn 23920 . . . . . . . 8 (((ℝ ⊆ ℂ ∧ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴cn→ℂ))
25098, 120, 1, 118, 249syl31anc 1485 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴cn→ℂ))
251142, 250eqeltrrd 2897 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴cn→ℂ))
252 plycn 24253 . . . . . . . 8 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
25368, 252syl 17 . . . . . . 7 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
2541, 20syl6ss 3821 . . . . . . . 8 (𝜑𝐴 ⊆ ℂ)
255 cncfmptid 22948 . . . . . . . 8 ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑦𝐴𝑦) ∈ (𝐴cn→ℂ))
256254, 164, 255sylancl 576 . . . . . . 7 (𝜑 → (𝑦𝐴𝑦) ∈ (𝐴cn→ℂ))
257253, 256cncfmpt1f 22949 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴cn→ℂ))
258121, 248, 251, 257cncfmpt2f 22950 . . . . 5 (𝜑 → (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) ∈ (𝐴cn→ℂ))
259 fveq2 6417 . . . . . 6 (𝑦 = 𝐵 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
260 fveq2 6417 . . . . . 6 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵))
261259, 260oveq12d 6901 . . . . 5 (𝑦 = 𝐵 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
262258, 44, 261cnmptlimc 23890 . . . 4 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) ∈ ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim 𝐵))
263246, 262eqeltrrd 2897 . . 3 (𝜑 → 0 ∈ ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim 𝐵))
264214subidd 10674 . . . . . 6 (𝜑 → (𝐵𝐵) = 0)
265264oveq1d 6898 . . . . 5 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) = (0↑(𝑀 + 1)))
2662070expd 13266 . . . . 5 (𝜑 → (0↑(𝑀 + 1)) = 0)
267265, 266eqtrd 2851 . . . 4 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) = 0)
268254sselda 3809 . . . . . . . 8 ((𝜑𝑦𝐴) → 𝑦 ∈ ℂ)
269268, 195syldan 581 . . . . . . 7 ((𝜑𝑦𝐴) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
270269fmpttd 6616 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℂ)
271 dvcn 23920 . . . . . 6 (((ℝ ⊆ ℂ ∧ (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = 𝐴) → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ∈ (𝐴cn→ℂ))
27298, 270, 1, 240, 271syl31anc 1485 . . . . 5 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ∈ (𝐴cn→ℂ))
273 oveq1 6890 . . . . . 6 (𝑦 = 𝐵 → (𝑦𝐵) = (𝐵𝐵))
274273oveq1d 6898 . . . . 5 (𝑦 = 𝐵 → ((𝑦𝐵)↑(𝑀 + 1)) = ((𝐵𝐵)↑(𝑀 + 1)))
275272, 44, 274cnmptlimc 23890 . . . 4 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) lim 𝐵))
276267, 275eqeltrrd 2897 . . 3 (𝜑 → 0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) lim 𝐵))
277254ssdifssd 3958 . . . . . . . . . 10 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
278277sselda 3809 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℂ)
279214adantr 468 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
280278, 279subcld 10686 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦𝐵) ∈ ℂ)
281 eldifsni 4523 . . . . . . . . . 10 (𝑦 ∈ (𝐴 ∖ {𝐵}) → 𝑦𝐵)
282281adantl 469 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦𝐵)
283278, 279, 282subne0d 10695 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦𝐵) ≠ 0)
284207adantr 468 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
285284nnzd 11766 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℤ)
286280, 283, 285expne0d 13256 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑(𝑀 + 1)) ≠ 0)
287286necomd 3044 . . . . . 6 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑦𝐵)↑(𝑀 + 1)))
288287neneqd 2994 . . . . 5 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑦𝐵)↑(𝑀 + 1)))
289288nrexdv 3199 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
290 df-ima 5337 . . . . . 6 ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵}))
291290eleq2i 2888 . . . . 5 (0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})))
292 resmpt 5667 . . . . . . 7 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦𝐵)↑(𝑀 + 1))))
293130, 292ax-mp 5 . . . . . 6 ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦𝐵)↑(𝑀 + 1)))
294 ovex 6915 . . . . . 6 ((𝑦𝐵)↑(𝑀 + 1)) ∈ V
295293, 294elrnmpti 5590 . . . . 5 (0 ∈ ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
296291, 295bitri 266 . . . 4 (0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
297289, 296sylnibr 320 . . 3 (𝜑 → ¬ 0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})))
29894adantr 468 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℂ)
299 1cnd 10329 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 1 ∈ ℂ)
300298, 299addcld 10353 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
301278, 200syldan 581 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑𝑀) ∈ ℂ)
302284nnne0d 11362 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
30381adantr 468 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ)
304303nnzd 11766 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
305280, 283, 304expne0d 13256 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑𝑀) ≠ 0)
306300, 301, 302, 305mulne0d 10973 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ≠ 0)
307306necomd 3044 . . . . . 6 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
308307neneqd 2994 . . . . 5 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
309308nrexdv 3199 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
310235imaeq1d 5688 . . . . . . 7 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})))
311 df-ima 5337 . . . . . . 7 ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))
312310, 311syl6eq 2867 . . . . . 6 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})))
313312eleq2d 2882 . . . . 5 (𝜑 → (0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))))
314 resmpt 5667 . . . . . . 7 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
315130, 314ax-mp 5 . . . . . 6 ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
316315, 237elrnmpti 5590 . . . . 5 (0 ∈ ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
317313, 316syl6bb 278 . . . 4 (𝜑 → (0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
318309, 317mtbird 316 . . 3 (𝜑 → ¬ 0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})))
319 eldifi 3942 . . . . . . . 8 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐴)
320135ffvelrnda 6590 . . . . . . . 8 ((𝜑𝑥𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
321319, 320sylan2 582 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
3221ssdifssd 3958 . . . . . . . . . 10 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℝ)
323322sselda 3809 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ)
324323recnd 10362 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
325152ffvelrnda 6590 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
326324, 325syldan 581 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
327321, 326subcld 10686 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) ∈ ℂ)
32847adantr 468 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℝ)
329323, 328resubcld 10752 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℝ)
33082adantr 468 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ0)
331329, 330reexpcld 13267 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ∈ ℝ)
332331recnd 10362 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ∈ ℂ)
333328recnd 10362 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
334324, 333subcld 10686 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℂ)
335 eldifsni 4523 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐵)
336335adantl 469 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥𝐵)
337324, 333, 336subne0d 10695 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ≠ 0)
338330nn0zd 11765 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
339334, 337, 338expne0d 13256 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ≠ 0)
340327, 332, 339divcld 11095 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) ∈ ℂ)
341207nnrecred 11363 . . . . . . 7 (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
342341recnd 10362 . . . . . 6 (𝜑 → (1 / (𝑀 + 1)) ∈ ℂ)
343342adantr 468 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (1 / (𝑀 + 1)) ∈ ℂ)
344 txtopon 21628 . . . . . . 7 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
345155, 155, 344mp2an 675 . . . . . 6 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
346345toponrestid 20959 . . . . 5 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
347 taylthlem2.i . . . . 5 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀))) lim 𝐵))
348 limcresi 23885 . . . . . . 7 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵) ⊆ (((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵)
349 resmpt 5667 . . . . . . . . 9 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))))
350130, 349ax-mp 5 . . . . . . . 8 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1)))
351350oveq1i 6893 . . . . . . 7 (((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵)
352348, 351sseqtri 3845 . . . . . 6 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵) ⊆ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵)
353 cncfmptc 22947 . . . . . . . 8 (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝐴 ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑥𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴cn→ℝ))
354341, 254, 98, 353syl3anc 1483 . . . . . . 7 (𝜑 → (𝑥𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴cn→ℝ))
355 eqidd 2818 . . . . . . 7 (𝑥 = 𝐵 → (1 / (𝑀 + 1)) = (1 / (𝑀 + 1)))
356354, 44, 355cnmptlimc 23890 . . . . . 6 (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵))
357352, 356sseldi 3807 . . . . 5 (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵))
358121mulcn 22903 . . . . . 6 · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
359 0cn 10326 . . . . . . 7 0 ∈ ℂ
360 opelxpi 5361 . . . . . . 7 ((0 ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
361359, 342, 360sylancr 577 . . . . . 6 (𝜑 → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
362345toponunii 20954 . . . . . . 7 (ℂ × ℂ) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
363362cncnpi 21316 . . . . . 6 (( · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ)) → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
364358, 361, 363sylancr 577 . . . . 5 (𝜑 → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
365340, 343, 165, 165, 121, 346, 347, 357, 364limccnp2 23892 . . . 4 (𝜑 → (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim 𝐵))
366342mul02d 10528 . . . 4 (𝜑 → (0 · (1 / (𝑀 + 1))) = 0)
367181fveq1d 6419 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥))
368 fveq2 6417 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥))
369 fveq2 6417 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥))
370368, 369oveq12d 6901 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
371 ovex 6915 . . . . . . . . . . 11 ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) ∈ V
372370, 184, 371fvmpt 6512 . . . . . . . . . 10 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
373319, 372syl 17 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
374367, 373sylan9eq 2871 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
375235fveq1d 6419 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥))
376 oveq1 6890 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦𝐵) = (𝑥𝐵))
377376oveq1d 6898 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝑦𝐵)↑𝑀) = ((𝑥𝐵)↑𝑀))
378377oveq2d 6899 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
379 ovex 6915 . . . . . . . . . . . 12 ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)) ∈ V
380378, 238, 379fvmpt 6512 . . . . . . . . . . 11 (𝑥𝐴 → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
381319, 380syl 17 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
382375, 381sylan9eq 2871 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
383207adantr 468 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
384383nncnd 11332 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
385384, 332mulcomd 10355 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)) = (((𝑥𝐵)↑𝑀) · (𝑀 + 1)))
386382, 385eqtrd 2851 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = (((𝑥𝐵)↑𝑀) · (𝑀 + 1)))
387374, 386oveq12d 6901 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / (((𝑥𝐵)↑𝑀) · (𝑀 + 1))))
388383nnne0d 11362 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
389327, 332, 384, 339, 388divdiv1d 11126 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) / (𝑀 + 1)) = (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / (((𝑥𝐵)↑𝑀) · (𝑀 + 1))))
390340, 384, 388divrecd 11098 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) / (𝑀 + 1)) = ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
391387, 389, 3903eqtr2rd 2858 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥)))
392391mpteq2dva 4949 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))))
393392oveq1d 6898 . . . 4 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))) lim 𝐵))
394365, 366, 3933eltr3d 2910 . . 3 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))) lim 𝐵))
3951, 75, 88, 128, 44, 129, 187, 241, 263, 276, 297, 318, 394lhop 24015 . 2 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) lim 𝐵))
396319adantl 469 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥𝐴)
397 fveq2 6417 . . . . . . . 8 (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥))
398 fveq2 6417 . . . . . . . 8 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))
399397, 398oveq12d 6901 . . . . . . 7 (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
400 eqid 2817 . . . . . . 7 (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
401 ovex 6915 . . . . . . 7 ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) ∈ V
402399, 400, 401fvmpt 6512 . . . . . 6 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
403396, 402syl 17 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
404376oveq1d 6898 . . . . . . 7 (𝑦 = 𝑥 → ((𝑦𝐵)↑(𝑀 + 1)) = ((𝑥𝐵)↑(𝑀 + 1)))
405 eqid 2817 . . . . . . 7 (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) = (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))
406 ovex 6915 . . . . . . 7 ((𝑥𝐵)↑(𝑀 + 1)) ∈ V
407404, 405, 406fvmpt 6512 . . . . . 6 (𝑥𝐴 → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥𝐵)↑(𝑀 + 1)))
408396, 407syl 17 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥𝐵)↑(𝑀 + 1)))
409403, 408oveq12d 6901 . . . 4 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1))))
410409mpteq2dva 4949 . . 3 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))))
411410oveq1d 6898 . 2 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))) lim 𝐵))
412395, 411eleqtrd 2898 1 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))) lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2157  wne 2989  wrex 3108  Vcvv 3402  cdif 3777  cin 3779  wss 3780  {csn 4381  {cpr 4383  cop 4387   class class class wbr 4855  cmpt 4934   × cxp 5322  dom cdm 5324  ran crn 5325  cres 5326  cima 5327  wf 6106  cfv 6110  (class class class)co 6883  𝑚 cmap 8101  pm cpm 8102  cc 10228  cr 10229  0cc0 10230  1c1 10231   + caddc 10233   · cmul 10235  cle 10369  cmin 10560   / cdiv 10978  cn 11314  0cn0 11578  cuz 11923  (,)cioo 12412  ...cfz 12568  ..^cfzo 12708  cexp 13102  !cfa 13299  TopOpenctopn 16306  topGenctg 16322  DivRingcdr 18970  SubRingcsubrg 18999  fldccnfld 19973  fldcrefld 20178  Topctop 20931  TopOnctopon 20948  intcnt 21055   Cn ccn 21262   CnP ccnp 21263   ×t ctx 21597  cnccncf 22912   lim climc 23862   D cdv 23863   D𝑛 cdvn 23864  Polycply 24176  degcdgr 24179   Tayl ctayl 24343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7188  ax-inf2 8794  ax-cnex 10286  ax-resscn 10287  ax-1cn 10288  ax-icn 10289  ax-addcl 10290  ax-addrcl 10291  ax-mulcl 10292  ax-mulrcl 10293  ax-mulcom 10294  ax-addass 10295  ax-mulass 10296  ax-distr 10297  ax-i2m1 10298  ax-1ne0 10299  ax-1rid 10300  ax-rnegex 10301  ax-rrecex 10302  ax-cnre 10303  ax-pre-lttri 10304  ax-pre-lttrn 10305  ax-pre-ltadd 10306  ax-pre-mulgt0 10307  ax-pre-sup 10308  ax-addf 10309  ax-mulf 10310
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5906  df-ord 5952  df-on 5953  df-lim 5954  df-suc 5955  df-iota 6073  df-fun 6112  df-fn 6113  df-f 6114  df-f1 6115  df-fo 6116  df-f1o 6117  df-fv 6118  df-isom 6119  df-riota 6844  df-ov 6886  df-oprab 6887  df-mpt2 6888  df-of 7136  df-om 7305  df-1st 7407  df-2nd 7408  df-supp 7539  df-tpos 7596  df-wrecs 7651  df-recs 7713  df-rdg 7751  df-1o 7805  df-2o 7806  df-oadd 7809  df-er 7988  df-map 8103  df-pm 8104  df-ixp 8155  df-en 8202  df-dom 8203  df-sdom 8204  df-fin 8205  df-fsupp 8524  df-fi 8565  df-sup 8596  df-inf 8597  df-oi 8663  df-card 9057  df-cda 9284  df-pnf 10370  df-mnf 10371  df-xr 10372  df-ltxr 10373  df-le 10374  df-sub 10562  df-neg 10563  df-div 10979  df-nn 11315  df-2 11375  df-3 11376  df-4 11377  df-5 11378  df-6 11379  df-7 11380  df-8 11381  df-9 11382  df-n0 11579  df-xnn0 11649  df-z 11663  df-dec 11779  df-uz 11924  df-q 12027  df-rp 12066  df-xneg 12181  df-xadd 12182  df-xmul 12183  df-ioo 12416  df-ioc 12417  df-ico 12418  df-icc 12419  df-fz 12569  df-fzo 12709  df-fl 12836  df-seq 13044  df-exp 13103  df-fac 13300  df-hash 13357  df-cj 14081  df-re 14082  df-im 14083  df-sqrt 14217  df-abs 14218  df-clim 14461  df-rlim 14462  df-sum 14659  df-struct 16089  df-ndx 16090  df-slot 16091  df-base 16093  df-sets 16094  df-ress 16095  df-plusg 16185  df-mulr 16186  df-starv 16187  df-sca 16188  df-vsca 16189  df-ip 16190  df-tset 16191  df-ple 16192  df-ds 16194  df-unif 16195  df-hom 16196  df-cco 16197  df-rest 16307  df-topn 16308  df-0g 16326  df-gsum 16327  df-topgen 16328  df-pt 16329  df-prds 16332  df-xrs 16386  df-qtop 16391  df-imas 16392  df-xps 16394  df-mre 16470  df-mrc 16471  df-acs 16473  df-mgm 17466  df-sgrp 17508  df-mnd 17519  df-submnd 17560  df-grp 17649  df-minusg 17650  df-mulg 17765  df-subg 17812  df-cntz 17970  df-cmn 18415  df-abl 18416  df-mgp 18711  df-ur 18723  df-ring 18770  df-cring 18771  df-oppr 18844  df-dvdsr 18862  df-unit 18863  df-invr 18893  df-dvr 18904  df-drng 18972  df-subrg 19001  df-psmet 19965  df-xmet 19966  df-met 19967  df-bl 19968  df-mopn 19969  df-fbas 19970  df-fg 19971  df-cnfld 19974  df-refld 20179  df-top 20932  df-topon 20949  df-topsp 20971  df-bases 20984  df-cld 21057  df-ntr 21058  df-cls 21059  df-nei 21136  df-lp 21174  df-perf 21175  df-cn 21265  df-cnp 21266  df-haus 21353  df-cmp 21424  df-tx 21599  df-hmeo 21792  df-fil 21883  df-fm 21975  df-flim 21976  df-flf 21977  df-tsms 22163  df-xms 22358  df-ms 22359  df-tms 22360  df-cncf 22914  df-0p 23673  df-limc 23866  df-dv 23867  df-dvn 23868  df-ply 24180  df-idp 24181  df-coe 24182  df-dgr 24183  df-tayl 24345
This theorem is referenced by:  taylth  24365
  Copyright terms: Public domain W3C validator