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

Theorem taylthlem2 23846
Description: Lemma for taylth 23847. (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 11561 . . . . . . . . . . . 12 1 ∈ (ℤ‘0)
4 fzss1 12203 . . . . . . . . . . . 12 (1 ∈ (ℤ‘0) → (1...𝑁) ⊆ (0...𝑁))
53, 4ax-mp 5 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
6 taylthlem2.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ (1..^𝑁))
7 fzofzp1 12383 . . . . . . . . . . . 12 (𝑀 ∈ (1..^𝑁) → (𝑀 + 1) ∈ (1...𝑁))
86, 7syl 17 . . . . . . . . . . 11 (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
95, 8sseldi 3562 . . . . . . . . . 10 (𝜑 → (𝑀 + 1) ∈ (0...𝑁))
10 fznn0sub2 12267 . . . . . . . . . 10 ((𝑀 + 1) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
119, 10syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
12 elfznn0 12254 . . . . . . . . 9 ((𝑁 − (𝑀 + 1)) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
1311, 12syl 17 . . . . . . . 8 (𝜑 → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
14 dvnfre 23435 . . . . . . . 8 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
152, 1, 13, 14syl3anc 1317 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
16 reelprrecn 9881 . . . . . . . . . . . 12 ℝ ∈ {ℝ, ℂ}
1716a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ {ℝ, ℂ})
18 cnex 9870 . . . . . . . . . . . . 13 ℂ ∈ V
1918a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ∈ V)
20 reex 9880 . . . . . . . . . . . . 13 ℝ ∈ V
2120a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
22 ax-resscn 9846 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
23 fss 5952 . . . . . . . . . . . . 13 ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
242, 22, 23sylancl 692 . . . . . . . . . . . 12 (𝜑𝐹:𝐴⟶ℂ)
25 elpm2r 7735 . . . . . . . . . . . 12 (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
2619, 21, 24, 1, 25syl22anc 1318 . . . . . . . . . . 11 (𝜑𝐹 ∈ (ℂ ↑pm ℝ))
27 dvnbss 23411 . . . . . . . . . . 11 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
2817, 26, 13, 27syl3anc 1317 . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
29 fdm 5947 . . . . . . . . . . 11 (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴)
302, 29syl 17 . . . . . . . . . 10 (𝜑 → dom 𝐹 = 𝐴)
3128, 30sseqtrd 3600 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ 𝐴)
32 taylth.d . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)
33 dvn2bss 23413 . . . . . . . . . . 11 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3417, 26, 11, 33syl3anc 1317 . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3532, 34eqsstr3d 3599 . . . . . . . . 9 (𝜑𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3631, 35eqssd 3581 . . . . . . . 8 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = 𝐴)
3736feq2d 5927 . . . . . . 7 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ))
3815, 37mpbid 220 . . . . . 6 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ)
3938ffvelrnda 6249 . . . . 5 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
401sselda 3564 . . . . . 6 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ)
41 fvres 6099 . . . . . . . 8 (𝑦 ∈ ℝ → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
4241adantl 480 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
43 resubdrg 19715 . . . . . . . . . . . 12 (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
4443simpli 472 . . . . . . . . . . 11 ℝ ∈ (SubRing‘ℂfld)
4544a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ (SubRing‘ℂfld))
46 taylth.n . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
4746nnnn0d 11195 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
48 taylth.b . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
4948, 32eleqtrrd 2687 . . . . . . . . . . . 12 (𝜑𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
50 taylth.t . . . . . . . . . . . 12 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)
511, 48sseldd 3565 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
522adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐹:𝐴⟶ℝ)
531adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐴 ⊆ ℝ)
54 elfznn0 12254 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
5554adantl 480 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
56 dvnfre 23435 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑘 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
5752, 53, 55, 56syl3anc 1317 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
5816a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → ℝ ∈ {ℝ, ℂ})
5926adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐹 ∈ (ℂ ↑pm ℝ))
60 simpr 475 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁))
61 dvn2bss 23413 . . . . . . . . . . . . . . . 16 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
6258, 59, 60, 61syl3anc 1317 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
6349adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
6462, 63sseldd 3565 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑘))
6557, 64ffvelrnd 6250 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝑁)) → (((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℝ)
66 faccl 12884 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
6755, 66syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
6865, 67nndivred 10913 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝑁)) → ((((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℝ)
6917, 24, 1, 47, 49, 50, 45, 51, 68taylply2 23840 . . . . . . . . . . 11 (𝜑 → (𝑇 ∈ (Poly‘ℝ) ∧ (deg‘𝑇) ≤ 𝑁))
7069simpld 473 . . . . . . . . . 10 (𝜑𝑇 ∈ (Poly‘ℝ))
71 dvnply2 23760 . . . . . . . . . 10 ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
7245, 70, 13, 71syl3anc 1317 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
73 plyreres 23756 . . . . . . . . 9 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
7472, 73syl 17 . . . . . . . 8 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
7574ffvelrnda 6249 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) ∈ ℝ)
7642, 75eqeltrrd 2685 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
7740, 76syldan 485 . . . . 5 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
7839, 77resubcld 10306 . . . 4 ((𝜑𝑦𝐴) → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ ℝ)
79 eqid 2606 . . . 4 (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
8078, 79fmptd 6274 . . 3 (𝜑 → (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))):𝐴⟶ℝ)
8151adantr 479 . . . . . 6 ((𝜑𝑦𝐴) → 𝐵 ∈ ℝ)
8240, 81resubcld 10306 . . . . 5 ((𝜑𝑦𝐴) → (𝑦𝐵) ∈ ℝ)
83 elfzouz 12295 . . . . . . . . . 10 (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (ℤ‘1))
846, 83syl 17 . . . . . . . . 9 (𝜑𝑀 ∈ (ℤ‘1))
85 nnuz 11552 . . . . . . . . 9 ℕ = (ℤ‘1)
8684, 85syl6eleqr 2695 . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
8786nnnn0d 11195 . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
8887adantr 479 . . . . . 6 ((𝜑𝑦𝐴) → 𝑀 ∈ ℕ0)
89 1nn0 11152 . . . . . . 7 1 ∈ ℕ0
9089a1i 11 . . . . . 6 ((𝜑𝑦𝐴) → 1 ∈ ℕ0)
9188, 90nn0addcld 11199 . . . . 5 ((𝜑𝑦𝐴) → (𝑀 + 1) ∈ ℕ0)
9282, 91reexpcld 12839 . . . 4 ((𝜑𝑦𝐴) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℝ)
93 eqid 2606 . . . 4 (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) = (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))
9492, 93fmptd 6274 . . 3 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℝ)
95 retop 22304 . . . . . 6 (topGen‘ran (,)) ∈ Top
96 uniretop 22305 . . . . . . 7 ℝ = (topGen‘ran (,))
9796ntrss2 20610 . . . . . 6 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
9895, 1, 97sylancr 693 . . . . 5 (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
9946nncnd 10880 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
10086nncnd 10880 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℂ)
101 1cnd 9909 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
10299, 100, 101nppcan2d 10266 . . . . . . . . . 10 (𝜑 → ((𝑁 − (𝑀 + 1)) + 1) = (𝑁𝑀))
103102fveq2d 6089 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
10422a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
105 dvnp1 23408 . . . . . . . . . 10 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
106104, 26, 13, 105syl3anc 1317 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
107103, 106eqtr3d 2642 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
108107dmeqd 5232 . . . . . . 7 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
109 fzonnsub 12314 . . . . . . . . . . . 12 (𝑀 ∈ (1..^𝑁) → (𝑁𝑀) ∈ ℕ)
1106, 109syl 17 . . . . . . . . . . 11 (𝜑 → (𝑁𝑀) ∈ ℕ)
111110nnnn0d 11195 . . . . . . . . . 10 (𝜑 → (𝑁𝑀) ∈ ℕ0)
112 dvnbss 23411 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ dom 𝐹)
11317, 26, 111, 112syl3anc 1317 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ dom 𝐹)
114113, 30sseqtrd 3600 . . . . . . . 8 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ 𝐴)
115 elfzofz 12306 . . . . . . . . . . . . 13 (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (1...𝑁))
1166, 115syl 17 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (1...𝑁))
1175, 116sseldi 3562 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑁))
118 fznn0sub2 12267 . . . . . . . . . . 11 (𝑀 ∈ (0...𝑁) → (𝑁𝑀) ∈ (0...𝑁))
119117, 118syl 17 . . . . . . . . . 10 (𝜑 → (𝑁𝑀) ∈ (0...𝑁))
120 dvn2bss 23413 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
12117, 26, 119, 120syl3anc 1317 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
12232, 121eqsstr3d 3599 . . . . . . . 8 (𝜑𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
123114, 122eqssd 3581 . . . . . . 7 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = 𝐴)
124108, 123eqtr3d 2642 . . . . . 6 (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴)
125 fss 5952 . . . . . . . 8 ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
12638, 22, 125sylancl 692 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
127 eqid 2606 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
128127tgioo2 22343 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
129104, 126, 1, 128, 127dvbssntr 23384 . . . . . 6 (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
130124, 129eqsstr3d 3599 . . . . 5 (𝜑𝐴 ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
13198, 130eqssd 3581 . . . 4 (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)
13296isopn3 20619 . . . . 5 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
13395, 1, 132sylancr 693 . . . 4 (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
134131, 133mpbird 245 . . 3 (𝜑𝐴 ∈ (topGen‘ran (,)))
135 eqid 2606 . . 3 (𝐴 ∖ {𝐵}) = (𝐴 ∖ {𝐵})
136 difss 3695 . . . 4 (𝐴 ∖ {𝐵}) ⊆ 𝐴
13739recnd 9921 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
138 dvnf 23410 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ)
13917, 26, 111, 138syl3anc 1317 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ)
140123feq2d 5927 . . . . . . . . 9 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℂ))
141139, 140mpbid 220 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℂ)
142141ffvelrnda 6249 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
143 dvnfre 23435 . . . . . . . . . . 11 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ)
1442, 1, 111, 143syl3anc 1317 . . . . . . . . . 10 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ)
145123feq2d 5927 . . . . . . . . . 10 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℝ))
146144, 145mpbid 220 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℝ)
147146feqmptd 6141 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦)))
14838feqmptd 6141 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
149148oveq2d 6540 . . . . . . . 8 (𝜑 → (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = (ℝ D (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
150107, 147, 1493eqtr3rd 2649 . . . . . . 7 (𝜑 → (ℝ D (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦)))
15177recnd 9921 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
152 fvex 6095 . . . . . . . 8 (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ V
153152a1i 11 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ V)
15476recnd 9921 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
155 recn 9879 . . . . . . . . 9 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
156 dvnply2 23760 . . . . . . . . . . . 12 ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ))
15745, 70, 111, 156syl3anc 1317 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ))
158 plyf 23672 . . . . . . . . . . 11 (((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)):ℂ⟶ℂ)
159157, 158syl 17 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)):ℂ⟶ℂ)
160159ffvelrnda 6249 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
161155, 160sylan2 489 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
162127cnfldtopon 22325 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
163 toponmax 20482 . . . . . . . . . 10 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
164162, 163mp1i 13 . . . . . . . . 9 (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
165 df-ss 3550 . . . . . . . . . 10 (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
166104, 165sylib 206 . . . . . . . . 9 (𝜑 → (ℝ ∩ ℂ) = ℝ)
167 plyf 23672 . . . . . . . . . . 11 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
16872, 167syl 17 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
169168ffvelrnda 6249 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
170102fveq2d 6089 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑀)))
171 ssid 3583 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
172171a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ⊆ ℂ)
173 mapsspm 7751 . . . . . . . . . . . . 13 (ℂ ↑𝑚 ℂ) ⊆ (ℂ ↑pm ℂ)
174 plyf 23672 . . . . . . . . . . . . . . 15 (𝑇 ∈ (Poly‘ℝ) → 𝑇:ℂ⟶ℂ)
17570, 174syl 17 . . . . . . . . . . . . . 14 (𝜑𝑇:ℂ⟶ℂ)
17618, 18elmap 7746 . . . . . . . . . . . . . 14 (𝑇 ∈ (ℂ ↑𝑚 ℂ) ↔ 𝑇:ℂ⟶ℂ)
177175, 176sylibr 222 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ (ℂ ↑𝑚 ℂ))
178173, 177sseldi 3562 . . . . . . . . . . . 12 (𝜑𝑇 ∈ (ℂ ↑pm ℂ))
179 dvnp1 23408 . . . . . . . . . . . 12 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
180172, 178, 13, 179syl3anc 1317 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
181170, 180eqtr3d 2642 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
182159feqmptd 6141 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
183168feqmptd 6141 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
184183oveq2d 6540 . . . . . . . . . 10 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
185181, 182, 1843eqtr3rd 2649 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
186127, 17, 164, 166, 169, 160, 185dvmptres3 23439 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
18717, 154, 161, 186, 1, 128, 127, 134dvmptres 23446 . . . . . . 7 (𝜑 → (ℝ D (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
18817, 137, 142, 150, 151, 153, 187dvmptsub 23450 . . . . . 6 (𝜑 → (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))))
189188dmeqd 5232 . . . . 5 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = dom (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))))
190 ovex 6552 . . . . . 6 ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)) ∈ V
191 eqid 2606 . . . . . 6 (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
192190, 191dmmpti 5919 . . . . 5 dom (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))) = 𝐴
193189, 192syl6eq 2656 . . . 4 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = 𝐴)
194136, 193syl5sseqr 3613 . . 3 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))))
195 simpr 475 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
19651adantr 479 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℂ) → 𝐵 ∈ ℝ)
197196recnd 9921 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝐵 ∈ ℂ)
198195, 197subcld 10240 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑦𝐵) ∈ ℂ)
19987adantr 479 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑀 ∈ ℕ0)
20089a1i 11 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 1 ∈ ℕ0)
201199, 200nn0addcld 11199 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
202198, 201expcld 12822 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
203155, 202sylan2 489 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
204100adantr 479 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑀 ∈ ℂ)
205 1cnd 9909 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 1 ∈ ℂ)
206204, 205addcld 9912 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℂ)
207198, 199expcld 12822 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → ((𝑦𝐵)↑𝑀) ∈ ℂ)
208206, 207mulcld 9913 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ ℂ)
209155, 208sylan2 489 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ ℂ)
21018prid2 4238 . . . . . . . . . . 11 ℂ ∈ {ℝ, ℂ}
211210a1i 11 . . . . . . . . . 10 (𝜑 → ℂ ∈ {ℝ, ℂ})
212 simpr 475 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
213 elfznn 12193 . . . . . . . . . . . . . 14 ((𝑀 + 1) ∈ (1...𝑁) → (𝑀 + 1) ∈ ℕ)
2148, 213syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀 + 1) ∈ ℕ)
215214nnnn0d 11195 . . . . . . . . . . . 12 (𝜑 → (𝑀 + 1) ∈ ℕ0)
216215adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
217212, 216expcld 12822 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝑥↑(𝑀 + 1)) ∈ ℂ)
218 ovex 6552 . . . . . . . . . . 11 ((𝑀 + 1) · (𝑥𝑀)) ∈ V
219218a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → ((𝑀 + 1) · (𝑥𝑀)) ∈ V)
220211dvmptid 23440 . . . . . . . . . . . 12 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
221 0cnd 9886 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → 0 ∈ ℂ)
22251recnd 9921 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℂ)
223211, 222dvmptc 23441 . . . . . . . . . . . 12 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝐵)) = (𝑦 ∈ ℂ ↦ 0))
224211, 195, 205, 220, 197, 221, 223dvmptsub 23450 . . . . . . . . . . 11 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝐵))) = (𝑦 ∈ ℂ ↦ (1 − 0)))
225 1m0e1 10975 . . . . . . . . . . . 12 (1 − 0) = 1
226225mpteq2i 4660 . . . . . . . . . . 11 (𝑦 ∈ ℂ ↦ (1 − 0)) = (𝑦 ∈ ℂ ↦ 1)
227224, 226syl6eq 2656 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝐵))) = (𝑦 ∈ ℂ ↦ 1))
228 dvexp 23436 . . . . . . . . . . . 12 ((𝑀 + 1) ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
229214, 228syl 17 . . . . . . . . . . 11 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
230100, 101pncand 10241 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
231230oveq2d 6540 . . . . . . . . . . . . 13 (𝜑 → (𝑥↑((𝑀 + 1) − 1)) = (𝑥𝑀))
232231oveq2d 6540 . . . . . . . . . . . 12 (𝜑 → ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))) = ((𝑀 + 1) · (𝑥𝑀)))
233232mpteq2dv 4664 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥𝑀))))
234229, 233eqtrd 2640 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥𝑀))))
235 oveq1 6531 . . . . . . . . . 10 (𝑥 = (𝑦𝐵) → (𝑥↑(𝑀 + 1)) = ((𝑦𝐵)↑(𝑀 + 1)))
236 oveq1 6531 . . . . . . . . . . 11 (𝑥 = (𝑦𝐵) → (𝑥𝑀) = ((𝑦𝐵)↑𝑀))
237236oveq2d 6540 . . . . . . . . . 10 (𝑥 = (𝑦𝐵) → ((𝑀 + 1) · (𝑥𝑀)) = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
238211, 211, 198, 205, 217, 219, 227, 234, 235, 237dvmptco 23455 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1)))
239208mulid1d 9910 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1) = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
240239mpteq2dva 4663 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1)) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
241238, 240eqtrd 2640 . . . . . . . 8 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
242127, 17, 164, 166, 202, 208, 241dvmptres3 23439 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℝ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
24317, 203, 209, 242, 1, 128, 127, 134dvmptres 23446 . . . . . 6 (𝜑 → (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
244243dmeqd 5232 . . . . 5 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = dom (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
245 ovex 6552 . . . . . 6 ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ V
246 eqid 2606 . . . . . 6 (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) = (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
247245, 246dmmpti 5919 . . . . 5 dom (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) = 𝐴
248244, 247syl6eq 2656 . . . 4 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = 𝐴)
249136, 248syl5sseqr 3613 . . 3 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))))
25017, 24, 1, 11, 49, 50dvntaylp0 23844 . . . . . 6 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
251250oveq2d 6540 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
252126, 48ffvelrnd 6250 . . . . . 6 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) ∈ ℂ)
253252subidd 10228 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
254251, 253eqtrd 2640 . . . 4 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
255127subcn 22405 . . . . . . 7 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
256255a1i 11 . . . . . 6 (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
257 dvcn 23404 . . . . . . . 8 (((ℝ ⊆ ℂ ∧ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴cn→ℂ))
258104, 126, 1, 124, 257syl31anc 1320 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴cn→ℂ))
259148, 258eqeltrrd 2685 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴cn→ℂ))
260 plycn 23735 . . . . . . . 8 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
26172, 260syl 17 . . . . . . 7 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
2621, 22syl6ss 3576 . . . . . . . 8 (𝜑𝐴 ⊆ ℂ)
263 cncfmptid 22451 . . . . . . . 8 ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑦𝐴𝑦) ∈ (𝐴cn→ℂ))
264262, 171, 263sylancl 692 . . . . . . 7 (𝜑 → (𝑦𝐴𝑦) ∈ (𝐴cn→ℂ))
265261, 264cncfmpt1f 22452 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴cn→ℂ))
266127, 256, 259, 265cncfmpt2f 22453 . . . . 5 (𝜑 → (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) ∈ (𝐴cn→ℂ))
267 fveq2 6085 . . . . . 6 (𝑦 = 𝐵 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
268 fveq2 6085 . . . . . 6 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵))
269267, 268oveq12d 6542 . . . . 5 (𝑦 = 𝐵 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
270266, 48, 269cnmptlimc 23374 . . . 4 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) ∈ ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim 𝐵))
271254, 270eqeltrrd 2685 . . 3 (𝜑 → 0 ∈ ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim 𝐵))
272222subidd 10228 . . . . . 6 (𝜑 → (𝐵𝐵) = 0)
273272oveq1d 6539 . . . . 5 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) = (0↑(𝑀 + 1)))
2742140expd 12838 . . . . 5 (𝜑 → (0↑(𝑀 + 1)) = 0)
275273, 274eqtrd 2640 . . . 4 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) = 0)
276262sselda 3564 . . . . . . . 8 ((𝜑𝑦𝐴) → 𝑦 ∈ ℂ)
277276, 202syldan 485 . . . . . . 7 ((𝜑𝑦𝐴) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
278277, 93fmptd 6274 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℂ)
279 dvcn 23404 . . . . . 6 (((ℝ ⊆ ℂ ∧ (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = 𝐴) → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ∈ (𝐴cn→ℂ))
280104, 278, 1, 248, 279syl31anc 1320 . . . . 5 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ∈ (𝐴cn→ℂ))
281 oveq1 6531 . . . . . 6 (𝑦 = 𝐵 → (𝑦𝐵) = (𝐵𝐵))
282281oveq1d 6539 . . . . 5 (𝑦 = 𝐵 → ((𝑦𝐵)↑(𝑀 + 1)) = ((𝐵𝐵)↑(𝑀 + 1)))
283280, 48, 282cnmptlimc 23374 . . . 4 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) lim 𝐵))
284275, 283eqeltrrd 2685 . . 3 (𝜑 → 0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) lim 𝐵))
285262ssdifssd 3706 . . . . . . . . . 10 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
286285sselda 3564 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℂ)
287222adantr 479 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
288286, 287subcld 10240 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦𝐵) ∈ ℂ)
289 eldifsni 4257 . . . . . . . . . 10 (𝑦 ∈ (𝐴 ∖ {𝐵}) → 𝑦𝐵)
290289adantl 480 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦𝐵)
291286, 287, 290subne0d 10249 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦𝐵) ≠ 0)
292214adantr 479 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
293292nnzd 11310 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℤ)
294288, 291, 293expne0d 12828 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑(𝑀 + 1)) ≠ 0)
295294necomd 2833 . . . . . 6 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑦𝐵)↑(𝑀 + 1)))
296295neneqd 2783 . . . . 5 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑦𝐵)↑(𝑀 + 1)))
297296nrexdv 2980 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
298 df-ima 5038 . . . . . 6 ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵}))
299298eleq2i 2676 . . . . 5 (0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})))
300 resmpt 5353 . . . . . . 7 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦𝐵)↑(𝑀 + 1))))
301136, 300ax-mp 5 . . . . . 6 ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦𝐵)↑(𝑀 + 1)))
302 ovex 6552 . . . . . 6 ((𝑦𝐵)↑(𝑀 + 1)) ∈ V
303301, 302elrnmpti 5281 . . . . 5 (0 ∈ ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
304299, 303bitri 262 . . . 4 (0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
305297, 304sylnibr 317 . . 3 (𝜑 → ¬ 0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})))
306100adantr 479 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℂ)
307 1cnd 9909 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 1 ∈ ℂ)
308306, 307addcld 9912 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
309286, 207syldan 485 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑𝑀) ∈ ℂ)
310292nnne0d 10909 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
31186adantr 479 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ)
312311nnzd 11310 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
313288, 291, 312expne0d 12828 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑𝑀) ≠ 0)
314308, 309, 310, 313mulne0d 10525 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ≠ 0)
315314necomd 2833 . . . . . 6 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
316315neneqd 2783 . . . . 5 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
317316nrexdv 2980 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
318243imaeq1d 5368 . . . . . . 7 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})))
319 df-ima 5038 . . . . . . 7 ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))
320318, 319syl6eq 2656 . . . . . 6 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})))
321320eleq2d 2669 . . . . 5 (𝜑 → (0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))))
322 resmpt 5353 . . . . . . 7 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
323136, 322ax-mp 5 . . . . . 6 ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
324323, 245elrnmpti 5281 . . . . 5 (0 ∈ ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
325321, 324syl6bb 274 . . . 4 (𝜑 → (0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
326317, 325mtbird 313 . . 3 (𝜑 → ¬ 0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})))
327 eldifi 3690 . . . . . . . 8 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐴)
328141ffvelrnda 6249 . . . . . . . 8 ((𝜑𝑥𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
329327, 328sylan2 489 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
3301ssdifssd 3706 . . . . . . . . . 10 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℝ)
331330sselda 3564 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ)
332331recnd 9921 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
333159ffvelrnda 6249 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
334332, 333syldan 485 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
335329, 334subcld 10240 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) ∈ ℂ)
33651adantr 479 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℝ)
337331, 336resubcld 10306 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℝ)
33887adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ0)
339337, 338reexpcld 12839 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ∈ ℝ)
340339recnd 9921 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ∈ ℂ)
341336recnd 9921 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
342332, 341subcld 10240 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℂ)
343 eldifsni 4257 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐵)
344343adantl 480 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥𝐵)
345332, 341, 344subne0d 10249 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ≠ 0)
346338nn0zd 11309 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
347342, 345, 346expne0d 12828 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ≠ 0)
348335, 340, 347divcld 10647 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) ∈ ℂ)
349214nnrecred 10910 . . . . . . 7 (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
350349recnd 9921 . . . . . 6 (𝜑 → (1 / (𝑀 + 1)) ∈ ℂ)
351350adantr 479 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (1 / (𝑀 + 1)) ∈ ℂ)
352 txtopon 21143 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
353162, 162, 352mp2an 703 . . . . . . 7 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
354353toponunii 20486 . . . . . . . 8 (ℂ × ℂ) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
355354restid 15860 . . . . . . 7 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)) → (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ)) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)))
356353, 355ax-mp 5 . . . . . 6 (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ)) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
357356eqcomi 2615 . . . . 5 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
358 taylthlem2.i . . . . 5 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀))) lim 𝐵))
359 limcresi 23369 . . . . . . 7 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵) ⊆ (((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵)
360 resmpt 5353 . . . . . . . . 9 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))))
361136, 360ax-mp 5 . . . . . . . 8 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1)))
362361oveq1i 6534 . . . . . . 7 (((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵)
363359, 362sseqtri 3596 . . . . . 6 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵) ⊆ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵)
364 cncfmptc 22450 . . . . . . . 8 (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝐴 ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑥𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴cn→ℝ))
365349, 262, 104, 364syl3anc 1317 . . . . . . 7 (𝜑 → (𝑥𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴cn→ℝ))
366 eqidd 2607 . . . . . . 7 (𝑥 = 𝐵 → (1 / (𝑀 + 1)) = (1 / (𝑀 + 1)))
367365, 48, 366cnmptlimc 23374 . . . . . 6 (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵))
368363, 367sseldi 3562 . . . . 5 (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵))
369127mulcn 22406 . . . . . 6 · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
370 0cn 9885 . . . . . . 7 0 ∈ ℂ
371 opelxpi 5059 . . . . . . 7 ((0 ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
372370, 350, 371sylancr 693 . . . . . 6 (𝜑 → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
373354cncnpi 20831 . . . . . 6 (( · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ)) → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
374369, 372, 373sylancr 693 . . . . 5 (𝜑 → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
375348, 351, 172, 172, 127, 357, 358, 368, 374limccnp2 23376 . . . 4 (𝜑 → (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim 𝐵))
376350mul02d 10082 . . . 4 (𝜑 → (0 · (1 / (𝑀 + 1))) = 0)
377188fveq1d 6087 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥))
378 fveq2 6085 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥))
379 fveq2 6085 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥))
380378, 379oveq12d 6542 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
381 ovex 6552 . . . . . . . . . . 11 ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) ∈ V
382380, 191, 381fvmpt 6173 . . . . . . . . . 10 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
383327, 382syl 17 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
384377, 383sylan9eq 2660 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
385243fveq1d 6087 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥))
386 oveq1 6531 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦𝐵) = (𝑥𝐵))
387386oveq1d 6539 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝑦𝐵)↑𝑀) = ((𝑥𝐵)↑𝑀))
388387oveq2d 6540 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
389 ovex 6552 . . . . . . . . . . . 12 ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)) ∈ V
390388, 246, 389fvmpt 6173 . . . . . . . . . . 11 (𝑥𝐴 → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
391327, 390syl 17 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
392385, 391sylan9eq 2660 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
393214adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
394393nncnd 10880 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
395394, 340mulcomd 9914 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)) = (((𝑥𝐵)↑𝑀) · (𝑀 + 1)))
396392, 395eqtrd 2640 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = (((𝑥𝐵)↑𝑀) · (𝑀 + 1)))
397384, 396oveq12d 6542 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / (((𝑥𝐵)↑𝑀) · (𝑀 + 1))))
398393nnne0d 10909 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
399335, 340, 394, 347, 398divdiv1d 10678 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) / (𝑀 + 1)) = (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / (((𝑥𝐵)↑𝑀) · (𝑀 + 1))))
400348, 394, 398divrecd 10650 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) / (𝑀 + 1)) = ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
401397, 399, 4003eqtr2rd 2647 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥)))
402401mpteq2dva 4663 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))))
403402oveq1d 6539 . . . 4 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))) lim 𝐵))
404375, 376, 4033eltr3d 2698 . . 3 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))) lim 𝐵))
4051, 80, 94, 134, 48, 135, 194, 249, 271, 284, 305, 326, 404lhop 23497 . 2 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) lim 𝐵))
406327adantl 480 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥𝐴)
407 fveq2 6085 . . . . . . . 8 (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥))
408 fveq2 6085 . . . . . . . 8 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))
409407, 408oveq12d 6542 . . . . . . 7 (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
410 ovex 6552 . . . . . . 7 ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) ∈ V
411409, 79, 410fvmpt 6173 . . . . . 6 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
412406, 411syl 17 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
413386oveq1d 6539 . . . . . . 7 (𝑦 = 𝑥 → ((𝑦𝐵)↑(𝑀 + 1)) = ((𝑥𝐵)↑(𝑀 + 1)))
414 ovex 6552 . . . . . . 7 ((𝑥𝐵)↑(𝑀 + 1)) ∈ V
415413, 93, 414fvmpt 6173 . . . . . 6 (𝑥𝐴 → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥𝐵)↑(𝑀 + 1)))
416406, 415syl 17 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥𝐵)↑(𝑀 + 1)))
417412, 416oveq12d 6542 . . . 4 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1))))
418417mpteq2dva 4663 . . 3 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))))
419418oveq1d 6539 . 2 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))) lim 𝐵))
420405, 419eleqtrd 2686 1 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))) lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2776  wrex 2893  Vcvv 3169  cdif 3533  cin 3535  wss 3536  {csn 4121  {cpr 4123  cop 4127   class class class wbr 4574  cmpt 4634   × cxp 5023  dom cdm 5025  ran crn 5026  cres 5027  cima 5028  wf 5783  cfv 5787  (class class class)co 6524  𝑚 cmap 7718  pm cpm 7719  cc 9787  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   · cmul 9794  cle 9928  cmin 10114   / cdiv 10530  cn 10864  0cn0 11136  cuz 11516  (,)cioo 11999  ...cfz 12149  ..^cfzo 12286  cexp 12674  !cfa 12874  t crest 15847  TopOpenctopn 15848  topGenctg 15864  DivRingcdr 18513  SubRingcsubrg 18542  fldccnfld 19510  fldcrefld 19711  Topctop 20456  TopOnctopon 20457  intcnt 20570   Cn ccn 20777   CnP ccnp 20778   ×t ctx 21112  cnccncf 22415   lim climc 23346   D cdv 23347   D𝑛 cdvn 23348  Polycply 23658  degcdgr 23661   Tayl ctayl 23825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868  ax-mulf 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-iin 4449  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-of 6769  df-om 6932  df-1st 7033  df-2nd 7034  df-supp 7157  df-tpos 7213  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-2o 7422  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-ixp 7769  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-fsupp 8133  df-fi 8174  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-4 10925  df-5 10926  df-6 10927  df-7 10928  df-8 10929  df-9 10930  df-n0 11137  df-z 11208  df-dec 11323  df-uz 11517  df-q 11618  df-rp 11662  df-xneg 11775  df-xadd 11776  df-xmul 11777  df-ioo 12003  df-ioc 12004  df-ico 12005  df-icc 12006  df-fz 12150  df-fzo 12287  df-fl 12407  df-seq 12616  df-exp 12675  df-fac 12875  df-hash 12932  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-clim 14010  df-rlim 14011  df-sum 14208  df-struct 15640  df-ndx 15641  df-slot 15642  df-base 15643  df-sets 15644  df-ress 15645  df-plusg 15724  df-mulr 15725  df-starv 15726  df-sca 15727  df-vsca 15728  df-ip 15729  df-tset 15730  df-ple 15731  df-ds 15734  df-unif 15735  df-hom 15736  df-cco 15737  df-rest 15849  df-topn 15850  df-0g 15868  df-gsum 15869  df-topgen 15870  df-pt 15871  df-prds 15874  df-xrs 15928  df-qtop 15933  df-imas 15934  df-xps 15936  df-mre 16012  df-mrc 16013  df-acs 16015  df-mgm 17008  df-sgrp 17050  df-mnd 17061  df-submnd 17102  df-grp 17191  df-minusg 17192  df-mulg 17307  df-subg 17357  df-cntz 17516  df-cmn 17961  df-abl 17962  df-mgp 18256  df-ur 18268  df-ring 18315  df-cring 18316  df-oppr 18389  df-dvdsr 18407  df-unit 18408  df-invr 18438  df-dvr 18449  df-drng 18515  df-subrg 18544  df-psmet 19502  df-xmet 19503  df-met 19504  df-bl 19505  df-mopn 19506  df-fbas 19507  df-fg 19508  df-cnfld 19511  df-refld 19712  df-top 20460  df-bases 20461  df-topon 20462  df-topsp 20463  df-cld 20572  df-ntr 20573  df-cls 20574  df-nei 20651  df-lp 20689  df-perf 20690  df-cn 20780  df-cnp 20781  df-haus 20868  df-cmp 20939  df-tx 21114  df-hmeo 21307  df-fil 21399  df-fm 21491  df-flim 21492  df-flf 21493  df-tsms 21679  df-xms 21873  df-ms 21874  df-tms 21875  df-cncf 22417  df-0p 23157  df-limc 23350  df-dv 23351  df-dvn 23352  df-ply 23662  df-idp 23663  df-coe 23664  df-dgr 23665  df-tayl 23827
This theorem is referenced by:  taylth  23847
  Copyright terms: Public domain W3C validator