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

Theorem taylthlem2 24109
Description: Lemma for taylth 24110. (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 1eluzge0 11717 . . . . . . . . . . . 12 1 ∈ (ℤ‘0)
4 fzss1 12365 . . . . . . . . . . . 12 (1 ∈ (ℤ‘0) → (1...𝑁) ⊆ (0...𝑁))
53, 4ax-mp 5 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
6 taylthlem2.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ (1..^𝑁))
7 fzofzp1 12549 . . . . . . . . . . . 12 (𝑀 ∈ (1..^𝑁) → (𝑀 + 1) ∈ (1...𝑁))
86, 7syl 17 . . . . . . . . . . 11 (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
95, 8sseldi 3593 . . . . . . . . . 10 (𝜑 → (𝑀 + 1) ∈ (0...𝑁))
10 fznn0sub2 12430 . . . . . . . . . 10 ((𝑀 + 1) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
119, 10syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
12 elfznn0 12417 . . . . . . . . 9 ((𝑁 − (𝑀 + 1)) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
1311, 12syl 17 . . . . . . . 8 (𝜑 → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
14 dvnfre 23696 . . . . . . . 8 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
152, 1, 13, 14syl3anc 1324 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
16 reelprrecn 10013 . . . . . . . . . . . 12 ℝ ∈ {ℝ, ℂ}
1716a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ {ℝ, ℂ})
18 cnex 10002 . . . . . . . . . . . . 13 ℂ ∈ V
1918a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ∈ V)
20 reex 10012 . . . . . . . . . . . . 13 ℝ ∈ V
2120a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
22 ax-resscn 9978 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
23 fss 6043 . . . . . . . . . . . . 13 ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
242, 22, 23sylancl 693 . . . . . . . . . . . 12 (𝜑𝐹:𝐴⟶ℂ)
25 elpm2r 7860 . . . . . . . . . . . 12 (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
2619, 21, 24, 1, 25syl22anc 1325 . . . . . . . . . . 11 (𝜑𝐹 ∈ (ℂ ↑pm ℝ))
27 dvnbss 23672 . . . . . . . . . . 11 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
2817, 26, 13, 27syl3anc 1324 . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
29 fdm 6038 . . . . . . . . . . 11 (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴)
302, 29syl 17 . . . . . . . . . 10 (𝜑 → dom 𝐹 = 𝐴)
3128, 30sseqtrd 3633 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ 𝐴)
32 taylth.d . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)
33 dvn2bss 23674 . . . . . . . . . . 11 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3417, 26, 11, 33syl3anc 1324 . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3532, 34eqsstr3d 3632 . . . . . . . . 9 (𝜑𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3631, 35eqssd 3612 . . . . . . . 8 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = 𝐴)
3736feq2d 6018 . . . . . . 7 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ))
3815, 37mpbid 222 . . . . . 6 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ)
3938ffvelrnda 6345 . . . . 5 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
401sselda 3595 . . . . . 6 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ)
41 fvres 6194 . . . . . . . 8 (𝑦 ∈ ℝ → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
4241adantl 482 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
43 resubdrg 19935 . . . . . . . . . . . 12 (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
4443simpli 474 . . . . . . . . . . 11 ℝ ∈ (SubRing‘ℂfld)
4544a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ (SubRing‘ℂfld))
46 taylth.n . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
4746nnnn0d 11336 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
48 taylth.b . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
4948, 32eleqtrrd 2702 . . . . . . . . . . . 12 (𝜑𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
50 taylth.t . . . . . . . . . . . 12 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)
511, 48sseldd 3596 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
522adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐹:𝐴⟶ℝ)
531adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐴 ⊆ ℝ)
54 elfznn0 12417 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
5554adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
56 dvnfre 23696 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑘 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
5752, 53, 55, 56syl3anc 1324 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
5816a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → ℝ ∈ {ℝ, ℂ})
5926adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐹 ∈ (ℂ ↑pm ℝ))
60 simpr 477 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁))
61 dvn2bss 23674 . . . . . . . . . . . . . . . 16 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
6258, 59, 60, 61syl3anc 1324 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
6349adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
6462, 63sseldd 3596 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑘))
6557, 64ffvelrnd 6346 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝑁)) → (((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℝ)
66 faccl 13053 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
6755, 66syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
6865, 67nndivred 11054 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝑁)) → ((((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℝ)
6917, 24, 1, 47, 49, 50, 45, 51, 68taylply2 24103 . . . . . . . . . . 11 (𝜑 → (𝑇 ∈ (Poly‘ℝ) ∧ (deg‘𝑇) ≤ 𝑁))
7069simpld 475 . . . . . . . . . 10 (𝜑𝑇 ∈ (Poly‘ℝ))
71 dvnply2 24023 . . . . . . . . . 10 ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
7245, 70, 13, 71syl3anc 1324 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
73 plyreres 24019 . . . . . . . . 9 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
7472, 73syl 17 . . . . . . . 8 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
7574ffvelrnda 6345 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) ∈ ℝ)
7642, 75eqeltrrd 2700 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
7740, 76syldan 487 . . . . 5 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
7839, 77resubcld 10443 . . . 4 ((𝜑𝑦𝐴) → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ ℝ)
79 eqid 2620 . . . 4 (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
8078, 79fmptd 6371 . . 3 (𝜑 → (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))):𝐴⟶ℝ)
8151adantr 481 . . . . . 6 ((𝜑𝑦𝐴) → 𝐵 ∈ ℝ)
8240, 81resubcld 10443 . . . . 5 ((𝜑𝑦𝐴) → (𝑦𝐵) ∈ ℝ)
83 elfzouz 12458 . . . . . . . . . 10 (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (ℤ‘1))
846, 83syl 17 . . . . . . . . 9 (𝜑𝑀 ∈ (ℤ‘1))
85 nnuz 11708 . . . . . . . . 9 ℕ = (ℤ‘1)
8684, 85syl6eleqr 2710 . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
8786nnnn0d 11336 . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
8887adantr 481 . . . . . 6 ((𝜑𝑦𝐴) → 𝑀 ∈ ℕ0)
89 1nn0 11293 . . . . . . 7 1 ∈ ℕ0
9089a1i 11 . . . . . 6 ((𝜑𝑦𝐴) → 1 ∈ ℕ0)
9188, 90nn0addcld 11340 . . . . 5 ((𝜑𝑦𝐴) → (𝑀 + 1) ∈ ℕ0)
9282, 91reexpcld 13008 . . . 4 ((𝜑𝑦𝐴) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℝ)
93 eqid 2620 . . . 4 (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) = (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))
9492, 93fmptd 6371 . . 3 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℝ)
95 retop 22546 . . . . . 6 (topGen‘ran (,)) ∈ Top
96 uniretop 22547 . . . . . . 7 ℝ = (topGen‘ran (,))
9796ntrss2 20842 . . . . . 6 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
9895, 1, 97sylancr 694 . . . . 5 (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
9946nncnd 11021 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
10086nncnd 11021 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℂ)
101 1cnd 10041 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
10299, 100, 101nppcan2d 10403 . . . . . . . . . 10 (𝜑 → ((𝑁 − (𝑀 + 1)) + 1) = (𝑁𝑀))
103102fveq2d 6182 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
10422a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
105 dvnp1 23669 . . . . . . . . . 10 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
106104, 26, 13, 105syl3anc 1324 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
107103, 106eqtr3d 2656 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
108107dmeqd 5315 . . . . . . 7 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
109 fzonnsub 12477 . . . . . . . . . . . 12 (𝑀 ∈ (1..^𝑁) → (𝑁𝑀) ∈ ℕ)
1106, 109syl 17 . . . . . . . . . . 11 (𝜑 → (𝑁𝑀) ∈ ℕ)
111110nnnn0d 11336 . . . . . . . . . 10 (𝜑 → (𝑁𝑀) ∈ ℕ0)
112 dvnbss 23672 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ dom 𝐹)
11317, 26, 111, 112syl3anc 1324 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ dom 𝐹)
114113, 30sseqtrd 3633 . . . . . . . 8 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ 𝐴)
115 elfzofz 12469 . . . . . . . . . . . . 13 (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (1...𝑁))
1166, 115syl 17 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (1...𝑁))
1175, 116sseldi 3593 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑁))
118 fznn0sub2 12430 . . . . . . . . . . 11 (𝑀 ∈ (0...𝑁) → (𝑁𝑀) ∈ (0...𝑁))
119117, 118syl 17 . . . . . . . . . 10 (𝜑 → (𝑁𝑀) ∈ (0...𝑁))
120 dvn2bss 23674 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
12117, 26, 119, 120syl3anc 1324 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
12232, 121eqsstr3d 3632 . . . . . . . 8 (𝜑𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
123114, 122eqssd 3612 . . . . . . 7 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = 𝐴)
124108, 123eqtr3d 2656 . . . . . 6 (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴)
125 fss 6043 . . . . . . . 8 ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
12638, 22, 125sylancl 693 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
127 eqid 2620 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
128127tgioo2 22587 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
129104, 126, 1, 128, 127dvbssntr 23645 . . . . . 6 (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
130124, 129eqsstr3d 3632 . . . . 5 (𝜑𝐴 ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
13198, 130eqssd 3612 . . . 4 (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)
13296isopn3 20851 . . . . 5 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
13395, 1, 132sylancr 694 . . . 4 (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
134131, 133mpbird 247 . . 3 (𝜑𝐴 ∈ (topGen‘ran (,)))
135 eqid 2620 . . 3 (𝐴 ∖ {𝐵}) = (𝐴 ∖ {𝐵})
136 difss 3729 . . . 4 (𝐴 ∖ {𝐵}) ⊆ 𝐴
13739recnd 10053 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
138 dvnf 23671 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ)
13917, 26, 111, 138syl3anc 1324 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ)
140123feq2d 6018 . . . . . . . . 9 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℂ))
141139, 140mpbid 222 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℂ)
142141ffvelrnda 6345 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
143 dvnfre 23696 . . . . . . . . . . 11 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ)
1442, 1, 111, 143syl3anc 1324 . . . . . . . . . 10 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ)
145123feq2d 6018 . . . . . . . . . 10 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℝ))
146144, 145mpbid 222 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℝ)
147146feqmptd 6236 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦)))
14838feqmptd 6236 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
149148oveq2d 6651 . . . . . . . 8 (𝜑 → (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = (ℝ D (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
150107, 147, 1493eqtr3rd 2663 . . . . . . 7 (𝜑 → (ℝ D (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦)))
15177recnd 10053 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
152 fvexd 6190 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ V)
15376recnd 10053 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
154 recn 10011 . . . . . . . . 9 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
155 dvnply2 24023 . . . . . . . . . . . 12 ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ))
15645, 70, 111, 155syl3anc 1324 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ))
157 plyf 23935 . . . . . . . . . . 11 (((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)):ℂ⟶ℂ)
158156, 157syl 17 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)):ℂ⟶ℂ)
159158ffvelrnda 6345 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
160154, 159sylan2 491 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
161127cnfldtopon 22567 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
162 toponmax 20711 . . . . . . . . . 10 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
163161, 162mp1i 13 . . . . . . . . 9 (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
164 df-ss 3581 . . . . . . . . . 10 (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
165104, 164sylib 208 . . . . . . . . 9 (𝜑 → (ℝ ∩ ℂ) = ℝ)
166 plyf 23935 . . . . . . . . . . 11 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
16772, 166syl 17 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
168167ffvelrnda 6345 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
169102fveq2d 6182 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑀)))
170 ssid 3616 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
171170a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ⊆ ℂ)
172 mapsspm 7876 . . . . . . . . . . . . 13 (ℂ ↑𝑚 ℂ) ⊆ (ℂ ↑pm ℂ)
173 plyf 23935 . . . . . . . . . . . . . . 15 (𝑇 ∈ (Poly‘ℝ) → 𝑇:ℂ⟶ℂ)
17470, 173syl 17 . . . . . . . . . . . . . 14 (𝜑𝑇:ℂ⟶ℂ)
17518, 18elmap 7871 . . . . . . . . . . . . . 14 (𝑇 ∈ (ℂ ↑𝑚 ℂ) ↔ 𝑇:ℂ⟶ℂ)
176174, 175sylibr 224 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ (ℂ ↑𝑚 ℂ))
177172, 176sseldi 3593 . . . . . . . . . . . 12 (𝜑𝑇 ∈ (ℂ ↑pm ℂ))
178 dvnp1 23669 . . . . . . . . . . . 12 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
179171, 177, 13, 178syl3anc 1324 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
180169, 179eqtr3d 2656 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
181158feqmptd 6236 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
182167feqmptd 6236 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
183182oveq2d 6651 . . . . . . . . . 10 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
184180, 181, 1833eqtr3rd 2663 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
185127, 17, 163, 165, 168, 159, 184dvmptres3 23700 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
18617, 153, 160, 185, 1, 128, 127, 134dvmptres 23707 . . . . . . 7 (𝜑 → (ℝ D (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
18717, 137, 142, 150, 151, 152, 186dvmptsub 23711 . . . . . 6 (𝜑 → (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))))
188187dmeqd 5315 . . . . 5 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = dom (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))))
189 ovex 6663 . . . . . 6 ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)) ∈ V
190 eqid 2620 . . . . . 6 (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
191189, 190dmmpti 6010 . . . . 5 dom (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))) = 𝐴
192188, 191syl6eq 2670 . . . 4 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = 𝐴)
193136, 192syl5sseqr 3646 . . 3 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))))
194 simpr 477 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
19551adantr 481 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℂ) → 𝐵 ∈ ℝ)
196195recnd 10053 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝐵 ∈ ℂ)
197194, 196subcld 10377 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑦𝐵) ∈ ℂ)
19887adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑀 ∈ ℕ0)
19989a1i 11 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 1 ∈ ℕ0)
200198, 199nn0addcld 11340 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
201197, 200expcld 12991 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
202154, 201sylan2 491 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
203100adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑀 ∈ ℂ)
204 1cnd 10041 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 1 ∈ ℂ)
205203, 204addcld 10044 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℂ)
206197, 198expcld 12991 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → ((𝑦𝐵)↑𝑀) ∈ ℂ)
207205, 206mulcld 10045 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ ℂ)
208154, 207sylan2 491 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ ℂ)
20918prid2 4289 . . . . . . . . . . 11 ℂ ∈ {ℝ, ℂ}
210209a1i 11 . . . . . . . . . 10 (𝜑 → ℂ ∈ {ℝ, ℂ})
211 simpr 477 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
212 elfznn 12355 . . . . . . . . . . . . . 14 ((𝑀 + 1) ∈ (1...𝑁) → (𝑀 + 1) ∈ ℕ)
2138, 212syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀 + 1) ∈ ℕ)
214213nnnn0d 11336 . . . . . . . . . . . 12 (𝜑 → (𝑀 + 1) ∈ ℕ0)
215214adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
216211, 215expcld 12991 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝑥↑(𝑀 + 1)) ∈ ℂ)
217 ovexd 6665 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → ((𝑀 + 1) · (𝑥𝑀)) ∈ V)
218210dvmptid 23701 . . . . . . . . . . . 12 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
219 0cnd 10018 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → 0 ∈ ℂ)
22051recnd 10053 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℂ)
221210, 220dvmptc 23702 . . . . . . . . . . . 12 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝐵)) = (𝑦 ∈ ℂ ↦ 0))
222210, 194, 204, 218, 196, 219, 221dvmptsub 23711 . . . . . . . . . . 11 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝐵))) = (𝑦 ∈ ℂ ↦ (1 − 0)))
223 1m0e1 11116 . . . . . . . . . . . 12 (1 − 0) = 1
224223mpteq2i 4732 . . . . . . . . . . 11 (𝑦 ∈ ℂ ↦ (1 − 0)) = (𝑦 ∈ ℂ ↦ 1)
225222, 224syl6eq 2670 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝐵))) = (𝑦 ∈ ℂ ↦ 1))
226 dvexp 23697 . . . . . . . . . . . 12 ((𝑀 + 1) ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
227213, 226syl 17 . . . . . . . . . . 11 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
228100, 101pncand 10378 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
229228oveq2d 6651 . . . . . . . . . . . . 13 (𝜑 → (𝑥↑((𝑀 + 1) − 1)) = (𝑥𝑀))
230229oveq2d 6651 . . . . . . . . . . . 12 (𝜑 → ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))) = ((𝑀 + 1) · (𝑥𝑀)))
231230mpteq2dv 4736 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥𝑀))))
232227, 231eqtrd 2654 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥𝑀))))
233 oveq1 6642 . . . . . . . . . 10 (𝑥 = (𝑦𝐵) → (𝑥↑(𝑀 + 1)) = ((𝑦𝐵)↑(𝑀 + 1)))
234 oveq1 6642 . . . . . . . . . . 11 (𝑥 = (𝑦𝐵) → (𝑥𝑀) = ((𝑦𝐵)↑𝑀))
235234oveq2d 6651 . . . . . . . . . 10 (𝑥 = (𝑦𝐵) → ((𝑀 + 1) · (𝑥𝑀)) = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
236210, 210, 197, 204, 216, 217, 225, 232, 233, 235dvmptco 23716 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1)))
237207mulid1d 10042 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1) = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
238237mpteq2dva 4735 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1)) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
239236, 238eqtrd 2654 . . . . . . . 8 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
240127, 17, 163, 165, 201, 207, 239dvmptres3 23700 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℝ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
24117, 202, 208, 240, 1, 128, 127, 134dvmptres 23707 . . . . . 6 (𝜑 → (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
242241dmeqd 5315 . . . . 5 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = dom (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
243 ovex 6663 . . . . . 6 ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ V
244 eqid 2620 . . . . . 6 (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) = (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
245243, 244dmmpti 6010 . . . . 5 dom (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) = 𝐴
246242, 245syl6eq 2670 . . . 4 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = 𝐴)
247136, 246syl5sseqr 3646 . . 3 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))))
24817, 24, 1, 11, 49, 50dvntaylp0 24107 . . . . . 6 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
249248oveq2d 6651 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
250126, 48ffvelrnd 6346 . . . . . 6 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) ∈ ℂ)
251250subidd 10365 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
252249, 251eqtrd 2654 . . . 4 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
253127subcn 22650 . . . . . . 7 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
254253a1i 11 . . . . . 6 (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
255 dvcn 23665 . . . . . . . 8 (((ℝ ⊆ ℂ ∧ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴cn→ℂ))
256104, 126, 1, 124, 255syl31anc 1327 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴cn→ℂ))
257148, 256eqeltrrd 2700 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴cn→ℂ))
258 plycn 23998 . . . . . . . 8 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
25972, 258syl 17 . . . . . . 7 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
2601, 22syl6ss 3607 . . . . . . . 8 (𝜑𝐴 ⊆ ℂ)
261 cncfmptid 22696 . . . . . . . 8 ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑦𝐴𝑦) ∈ (𝐴cn→ℂ))
262260, 170, 261sylancl 693 . . . . . . 7 (𝜑 → (𝑦𝐴𝑦) ∈ (𝐴cn→ℂ))
263259, 262cncfmpt1f 22697 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴cn→ℂ))
264127, 254, 257, 263cncfmpt2f 22698 . . . . 5 (𝜑 → (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) ∈ (𝐴cn→ℂ))
265 fveq2 6178 . . . . . 6 (𝑦 = 𝐵 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
266 fveq2 6178 . . . . . 6 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵))
267265, 266oveq12d 6653 . . . . 5 (𝑦 = 𝐵 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
268264, 48, 267cnmptlimc 23635 . . . 4 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) ∈ ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim 𝐵))
269252, 268eqeltrrd 2700 . . 3 (𝜑 → 0 ∈ ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim 𝐵))
270220subidd 10365 . . . . . 6 (𝜑 → (𝐵𝐵) = 0)
271270oveq1d 6650 . . . . 5 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) = (0↑(𝑀 + 1)))
2722130expd 13007 . . . . 5 (𝜑 → (0↑(𝑀 + 1)) = 0)
273271, 272eqtrd 2654 . . . 4 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) = 0)
274260sselda 3595 . . . . . . . 8 ((𝜑𝑦𝐴) → 𝑦 ∈ ℂ)
275274, 201syldan 487 . . . . . . 7 ((𝜑𝑦𝐴) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
276275, 93fmptd 6371 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℂ)
277 dvcn 23665 . . . . . 6 (((ℝ ⊆ ℂ ∧ (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = 𝐴) → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ∈ (𝐴cn→ℂ))
278104, 276, 1, 246, 277syl31anc 1327 . . . . 5 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ∈ (𝐴cn→ℂ))
279 oveq1 6642 . . . . . 6 (𝑦 = 𝐵 → (𝑦𝐵) = (𝐵𝐵))
280279oveq1d 6650 . . . . 5 (𝑦 = 𝐵 → ((𝑦𝐵)↑(𝑀 + 1)) = ((𝐵𝐵)↑(𝑀 + 1)))
281278, 48, 280cnmptlimc 23635 . . . 4 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) lim 𝐵))
282273, 281eqeltrrd 2700 . . 3 (𝜑 → 0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) lim 𝐵))
283260ssdifssd 3740 . . . . . . . . . 10 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
284283sselda 3595 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℂ)
285220adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
286284, 285subcld 10377 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦𝐵) ∈ ℂ)
287 eldifsni 4311 . . . . . . . . . 10 (𝑦 ∈ (𝐴 ∖ {𝐵}) → 𝑦𝐵)
288287adantl 482 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦𝐵)
289284, 285, 288subne0d 10386 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦𝐵) ≠ 0)
290213adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
291290nnzd 11466 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℤ)
292286, 289, 291expne0d 12997 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑(𝑀 + 1)) ≠ 0)
293292necomd 2846 . . . . . 6 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑦𝐵)↑(𝑀 + 1)))
294293neneqd 2796 . . . . 5 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑦𝐵)↑(𝑀 + 1)))
295294nrexdv 2998 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
296 df-ima 5117 . . . . . 6 ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵}))
297296eleq2i 2691 . . . . 5 (0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})))
298 resmpt 5437 . . . . . . 7 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦𝐵)↑(𝑀 + 1))))
299136, 298ax-mp 5 . . . . . 6 ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦𝐵)↑(𝑀 + 1)))
300 ovex 6663 . . . . . 6 ((𝑦𝐵)↑(𝑀 + 1)) ∈ V
301299, 300elrnmpti 5365 . . . . 5 (0 ∈ ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
302297, 301bitri 264 . . . 4 (0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
303295, 302sylnibr 319 . . 3 (𝜑 → ¬ 0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})))
304100adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℂ)
305 1cnd 10041 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 1 ∈ ℂ)
306304, 305addcld 10044 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
307284, 206syldan 487 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑𝑀) ∈ ℂ)
308290nnne0d 11050 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
30986adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ)
310309nnzd 11466 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
311286, 289, 310expne0d 12997 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑𝑀) ≠ 0)
312306, 307, 308, 311mulne0d 10664 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ≠ 0)
313312necomd 2846 . . . . . 6 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
314313neneqd 2796 . . . . 5 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
315314nrexdv 2998 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
316241imaeq1d 5453 . . . . . . 7 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})))
317 df-ima 5117 . . . . . . 7 ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))
318316, 317syl6eq 2670 . . . . . 6 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})))
319318eleq2d 2685 . . . . 5 (𝜑 → (0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))))
320 resmpt 5437 . . . . . . 7 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
321136, 320ax-mp 5 . . . . . 6 ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
322321, 243elrnmpti 5365 . . . . 5 (0 ∈ ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
323319, 322syl6bb 276 . . . 4 (𝜑 → (0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
324315, 323mtbird 315 . . 3 (𝜑 → ¬ 0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})))
325 eldifi 3724 . . . . . . . 8 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐴)
326141ffvelrnda 6345 . . . . . . . 8 ((𝜑𝑥𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
327325, 326sylan2 491 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
3281ssdifssd 3740 . . . . . . . . . 10 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℝ)
329328sselda 3595 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ)
330329recnd 10053 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
331158ffvelrnda 6345 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
332330, 331syldan 487 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
333327, 332subcld 10377 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) ∈ ℂ)
33451adantr 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℝ)
335329, 334resubcld 10443 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℝ)
33687adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ0)
337335, 336reexpcld 13008 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ∈ ℝ)
338337recnd 10053 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ∈ ℂ)
339334recnd 10053 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
340330, 339subcld 10377 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℂ)
341 eldifsni 4311 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐵)
342341adantl 482 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥𝐵)
343330, 339, 342subne0d 10386 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ≠ 0)
344336nn0zd 11465 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
345340, 343, 344expne0d 12997 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ≠ 0)
346333, 338, 345divcld 10786 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) ∈ ℂ)
347213nnrecred 11051 . . . . . . 7 (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
348347recnd 10053 . . . . . 6 (𝜑 → (1 / (𝑀 + 1)) ∈ ℂ)
349348adantr 481 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (1 / (𝑀 + 1)) ∈ ℂ)
350 txtopon 21375 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
351161, 161, 350mp2an 707 . . . . . . 7 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
352351toponunii 20702 . . . . . . . 8 (ℂ × ℂ) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
353352restid 16075 . . . . . . 7 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)) → (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ)) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)))
354351, 353ax-mp 5 . . . . . 6 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ)) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
355354eqcomi 2629 . . . . 5 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
356 taylthlem2.i . . . . 5 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀))) lim 𝐵))
357 limcresi 23630 . . . . . . 7 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵) ⊆ (((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵)
358 resmpt 5437 . . . . . . . . 9 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))))
359136, 358ax-mp 5 . . . . . . . 8 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1)))
360359oveq1i 6645 . . . . . . 7 (((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵)
361357, 360sseqtri 3629 . . . . . 6 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵) ⊆ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵)
362 cncfmptc 22695 . . . . . . . 8 (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝐴 ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑥𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴cn→ℝ))
363347, 260, 104, 362syl3anc 1324 . . . . . . 7 (𝜑 → (𝑥𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴cn→ℝ))
364 eqidd 2621 . . . . . . 7 (𝑥 = 𝐵 → (1 / (𝑀 + 1)) = (1 / (𝑀 + 1)))
365363, 48, 364cnmptlimc 23635 . . . . . 6 (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵))
366361, 365sseldi 3593 . . . . 5 (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵))
367127mulcn 22651 . . . . . 6 · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
368 0cn 10017 . . . . . . 7 0 ∈ ℂ
369 opelxpi 5138 . . . . . . 7 ((0 ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
370368, 348, 369sylancr 694 . . . . . 6 (𝜑 → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
371352cncnpi 21063 . . . . . 6 (( · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ)) → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
372367, 370, 371sylancr 694 . . . . 5 (𝜑 → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
373346, 349, 171, 171, 127, 355, 356, 366, 372limccnp2 23637 . . . 4 (𝜑 → (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim 𝐵))
374348mul02d 10219 . . . 4 (𝜑 → (0 · (1 / (𝑀 + 1))) = 0)
375187fveq1d 6180 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥))
376 fveq2 6178 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥))
377 fveq2 6178 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥))
378376, 377oveq12d 6653 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
379 ovex 6663 . . . . . . . . . . 11 ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) ∈ V
380378, 190, 379fvmpt 6269 . . . . . . . . . 10 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
381325, 380syl 17 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
382375, 381sylan9eq 2674 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
383241fveq1d 6180 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥))
384 oveq1 6642 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦𝐵) = (𝑥𝐵))
385384oveq1d 6650 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝑦𝐵)↑𝑀) = ((𝑥𝐵)↑𝑀))
386385oveq2d 6651 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
387 ovex 6663 . . . . . . . . . . . 12 ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)) ∈ V
388386, 244, 387fvmpt 6269 . . . . . . . . . . 11 (𝑥𝐴 → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
389325, 388syl 17 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
390383, 389sylan9eq 2674 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
391213adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
392391nncnd 11021 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
393392, 338mulcomd 10046 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)) = (((𝑥𝐵)↑𝑀) · (𝑀 + 1)))
394390, 393eqtrd 2654 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = (((𝑥𝐵)↑𝑀) · (𝑀 + 1)))
395382, 394oveq12d 6653 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / (((𝑥𝐵)↑𝑀) · (𝑀 + 1))))
396391nnne0d 11050 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
397333, 338, 392, 345, 396divdiv1d 10817 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) / (𝑀 + 1)) = (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / (((𝑥𝐵)↑𝑀) · (𝑀 + 1))))
398346, 392, 396divrecd 10789 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) / (𝑀 + 1)) = ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
399395, 397, 3983eqtr2rd 2661 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥)))
400399mpteq2dva 4735 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))))
401400oveq1d 6650 . . . 4 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))) lim 𝐵))
402373, 374, 4013eltr3d 2713 . . 3 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))) lim 𝐵))
4031, 80, 94, 134, 48, 135, 193, 247, 269, 282, 303, 324, 402lhop 23760 . 2 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) lim 𝐵))
404325adantl 482 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥𝐴)
405 fveq2 6178 . . . . . . . 8 (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥))
406 fveq2 6178 . . . . . . . 8 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))
407405, 406oveq12d 6653 . . . . . . 7 (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
408 ovex 6663 . . . . . . 7 ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) ∈ V
409407, 79, 408fvmpt 6269 . . . . . 6 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
410404, 409syl 17 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
411384oveq1d 6650 . . . . . . 7 (𝑦 = 𝑥 → ((𝑦𝐵)↑(𝑀 + 1)) = ((𝑥𝐵)↑(𝑀 + 1)))
412 ovex 6663 . . . . . . 7 ((𝑥𝐵)↑(𝑀 + 1)) ∈ V
413411, 93, 412fvmpt 6269 . . . . . 6 (𝑥𝐴 → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥𝐵)↑(𝑀 + 1)))
414404, 413syl 17 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥𝐵)↑(𝑀 + 1)))
415410, 414oveq12d 6653 . . . 4 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1))))
416415mpteq2dva 4735 . . 3 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))))
417416oveq1d 6650 . 2 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))) lim 𝐵))
418403, 417eleqtrd 2701 1 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))) lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  wne 2791  wrex 2910  Vcvv 3195  cdif 3564  cin 3566  wss 3567  {csn 4168  {cpr 4170  cop 4174   class class class wbr 4644  cmpt 4720   × cxp 5102  dom cdm 5104  ran crn 5105  cres 5106  cima 5107  wf 5872  cfv 5876  (class class class)co 6635  𝑚 cmap 7842  pm cpm 7843  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926  cle 10060  cmin 10251   / cdiv 10669  cn 11005  0cn0 11277  cuz 11672  (,)cioo 12160  ...cfz 12311  ..^cfzo 12449  cexp 12843  !cfa 13043  t crest 16062  TopOpenctopn 16063  topGenctg 16079  DivRingcdr 18728  SubRingcsubrg 18757  fldccnfld 19727  fldcrefld 19931  Topctop 20679  TopOnctopon 20696  intcnt 20802   Cn ccn 21009   CnP ccnp 21010   ×t ctx 21344  cnccncf 22660   lim climc 23607   D cdv 23608   D𝑛 cdvn 23609  Polycply 23921  degcdgr 23924   Tayl ctayl 24088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999  ax-addf 10000  ax-mulf 10001
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-supp 7281  df-tpos 7337  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-ixp 7894  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fsupp 8261  df-fi 8302  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-xnn0 11349  df-z 11363  df-dec 11479  df-uz 11673  df-q 11774  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ioo 12164  df-ioc 12165  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-fac 13044  df-hash 13101  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-clim 14200  df-rlim 14201  df-sum 14398  df-struct 15840  df-ndx 15841  df-slot 15842  df-base 15844  df-sets 15845  df-ress 15846  df-plusg 15935  df-mulr 15936  df-starv 15937  df-sca 15938  df-vsca 15939  df-ip 15940  df-tset 15941  df-ple 15942  df-ds 15945  df-unif 15946  df-hom 15947  df-cco 15948  df-rest 16064  df-topn 16065  df-0g 16083  df-gsum 16084  df-topgen 16085  df-pt 16086  df-prds 16089  df-xrs 16143  df-qtop 16148  df-imas 16149  df-xps 16151  df-mre 16227  df-mrc 16228  df-acs 16230  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-submnd 17317  df-grp 17406  df-minusg 17407  df-mulg 17522  df-subg 17572  df-cntz 17731  df-cmn 18176  df-abl 18177  df-mgp 18471  df-ur 18483  df-ring 18530  df-cring 18531  df-oppr 18604  df-dvdsr 18622  df-unit 18623  df-invr 18653  df-dvr 18664  df-drng 18730  df-subrg 18759  df-psmet 19719  df-xmet 19720  df-met 19721  df-bl 19722  df-mopn 19723  df-fbas 19724  df-fg 19725  df-cnfld 19728  df-refld 19932  df-top 20680  df-topon 20697  df-topsp 20718  df-bases 20731  df-cld 20804  df-ntr 20805  df-cls 20806  df-nei 20883  df-lp 20921  df-perf 20922  df-cn 21012  df-cnp 21013  df-haus 21100  df-cmp 21171  df-tx 21346  df-hmeo 21539  df-fil 21631  df-fm 21723  df-flim 21724  df-flf 21725  df-tsms 21911  df-xms 22106  df-ms 22107  df-tms 22108  df-cncf 22662  df-0p 23418  df-limc 23611  df-dv 23612  df-dvn 23613  df-ply 23925  df-idp 23926  df-coe 23927  df-dgr 23928  df-tayl 24090
This theorem is referenced by:  taylth  24110
  Copyright terms: Public domain W3C validator