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

Theorem taylthlem2 24975
 Description: Lemma for taylth 24976. (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 13010 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
4 taylthlem2.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ (1..^𝑁))
5 fzofzp1 13141 . . . . . . . . . . . 12 (𝑀 ∈ (1..^𝑁) → (𝑀 + 1) ∈ (1...𝑁))
64, 5syl 17 . . . . . . . . . . 11 (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
73, 6sseldi 3952 . . . . . . . . . 10 (𝜑 → (𝑀 + 1) ∈ (0...𝑁))
8 fznn0sub2 13021 . . . . . . . . . 10 ((𝑀 + 1) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
97, 8syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
10 elfznn0 13007 . . . . . . . . 9 ((𝑁 − (𝑀 + 1)) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
119, 10syl 17 . . . . . . . 8 (𝜑 → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
12 dvnfre 24561 . . . . . . . 8 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
132, 1, 11, 12syl3anc 1368 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
14 reelprrecn 10628 . . . . . . . . . . . 12 ℝ ∈ {ℝ, ℂ}
1514a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ {ℝ, ℂ})
16 cnex 10617 . . . . . . . . . . . . 13 ℂ ∈ V
1716a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ∈ V)
18 reex 10627 . . . . . . . . . . . . 13 ℝ ∈ V
1918a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
20 ax-resscn 10593 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
21 fss 6518 . . . . . . . . . . . . 13 ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
222, 20, 21sylancl 589 . . . . . . . . . . . 12 (𝜑𝐹:𝐴⟶ℂ)
23 elpm2r 8421 . . . . . . . . . . . 12 (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
2417, 19, 22, 1, 23syl22anc 837 . . . . . . . . . . 11 (𝜑𝐹 ∈ (ℂ ↑pm ℝ))
25 dvnbss 24537 . . . . . . . . . . 11 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
2615, 24, 11, 25syl3anc 1368 . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
272, 26fssdmd 6520 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ 𝐴)
28 taylth.d . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)
29 dvn2bss 24539 . . . . . . . . . . 11 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3015, 24, 9, 29syl3anc 1368 . . . . . . . . . 10 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3128, 30eqsstrrd 3993 . . . . . . . . 9 (𝜑𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
3227, 31eqssd 3971 . . . . . . . 8 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = 𝐴)
3332feq2d 6490 . . . . . . 7 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ))
3413, 33mpbid 235 . . . . . 6 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ)
3534ffvelrnda 6843 . . . . 5 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
361sselda 3954 . . . . . 6 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ)
37 fvres 6681 . . . . . . . 8 (𝑦 ∈ ℝ → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
3837adantl 485 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
39 resubdrg 20755 . . . . . . . . . . . 12 (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
4039simpli 487 . . . . . . . . . . 11 ℝ ∈ (SubRing‘ℂfld)
4140a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ (SubRing‘ℂfld))
42 taylth.n . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
4342nnnn0d 11955 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
44 taylth.b . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
4544, 28eleqtrrd 2919 . . . . . . . . . . . 12 (𝜑𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
46 taylth.t . . . . . . . . . . . 12 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)
471, 44sseldd 3955 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
48 elfznn0 13007 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
49 dvnfre 24561 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑘 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
502, 1, 48, 49syl2an3an 1419 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
51 simpr 488 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁))
52 dvn2bss 24539 . . . . . . . . . . . . . . . 16 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
5314, 24, 51, 52mp3an2ani 1465 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
5445adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
5553, 54sseldd 3955 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑘))
5650, 55ffvelrnd 6844 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝑁)) → (((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℝ)
5748adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
5857faccld 13652 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
5956, 58nndivred 11691 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝑁)) → ((((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℝ)
6015, 22, 1, 43, 45, 46, 41, 47, 59taylply2 24969 . . . . . . . . . . 11 (𝜑 → (𝑇 ∈ (Poly‘ℝ) ∧ (deg‘𝑇) ≤ 𝑁))
6160simpld 498 . . . . . . . . . 10 (𝜑𝑇 ∈ (Poly‘ℝ))
62 dvnply2 24889 . . . . . . . . . 10 ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
6341, 61, 11, 62syl3anc 1368 . . . . . . . . 9 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
64 plyreres 24885 . . . . . . . . 9 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
6563, 64syl 17 . . . . . . . 8 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
6665ffvelrnda 6843 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) ∈ ℝ)
6738, 66eqeltrrd 2917 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
6836, 67syldan 594 . . . . 5 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
6935, 68resubcld 11067 . . . 4 ((𝜑𝑦𝐴) → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ ℝ)
7069fmpttd 6871 . . 3 (𝜑 → (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))):𝐴⟶ℝ)
7147adantr 484 . . . . . 6 ((𝜑𝑦𝐴) → 𝐵 ∈ ℝ)
7236, 71resubcld 11067 . . . . 5 ((𝜑𝑦𝐴) → (𝑦𝐵) ∈ ℝ)
73 elfzouz 13049 . . . . . . . . . 10 (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (ℤ‘1))
744, 73syl 17 . . . . . . . . 9 (𝜑𝑀 ∈ (ℤ‘1))
75 nnuz 12281 . . . . . . . . 9 ℕ = (ℤ‘1)
7674, 75eleqtrrdi 2927 . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
7776nnnn0d 11955 . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
7877adantr 484 . . . . . 6 ((𝜑𝑦𝐴) → 𝑀 ∈ ℕ0)
79 1nn0 11913 . . . . . . 7 1 ∈ ℕ0
8079a1i 11 . . . . . 6 ((𝜑𝑦𝐴) → 1 ∈ ℕ0)
8178, 80nn0addcld 11959 . . . . 5 ((𝜑𝑦𝐴) → (𝑀 + 1) ∈ ℕ0)
8272, 81reexpcld 13535 . . . 4 ((𝜑𝑦𝐴) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℝ)
8382fmpttd 6871 . . 3 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℝ)
84 retop 23373 . . . . . 6 (topGen‘ran (,)) ∈ Top
85 uniretop 23374 . . . . . . 7 ℝ = (topGen‘ran (,))
8685ntrss2 21668 . . . . . 6 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
8784, 1, 86sylancr 590 . . . . 5 (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
8842nncnd 11653 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
8976nncnd 11653 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℂ)
90 1cnd 10635 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
9188, 89, 90nppcan2d 11022 . . . . . . . . . 10 (𝜑 → ((𝑁 − (𝑀 + 1)) + 1) = (𝑁𝑀))
9291fveq2d 6666 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
9320a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
94 dvnp1 24534 . . . . . . . . . 10 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
9593, 24, 11, 94syl3anc 1368 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
9692, 95eqtr3d 2861 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
9796dmeqd 5762 . . . . . . 7 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
98 fzonnsub 13069 . . . . . . . . . . . 12 (𝑀 ∈ (1..^𝑁) → (𝑁𝑀) ∈ ℕ)
994, 98syl 17 . . . . . . . . . . 11 (𝜑 → (𝑁𝑀) ∈ ℕ)
10099nnnn0d 11955 . . . . . . . . . 10 (𝜑 → (𝑁𝑀) ∈ ℕ0)
101 dvnbss 24537 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ dom 𝐹)
10215, 24, 100, 101syl3anc 1368 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ dom 𝐹)
1032, 102fssdmd 6520 . . . . . . . 8 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) ⊆ 𝐴)
104 elfzofz 13060 . . . . . . . . . . . . 13 (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (1...𝑁))
1054, 104syl 17 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (1...𝑁))
1063, 105sseldi 3952 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑁))
107 fznn0sub2 13021 . . . . . . . . . . 11 (𝑀 ∈ (0...𝑁) → (𝑁𝑀) ∈ (0...𝑁))
108106, 107syl 17 . . . . . . . . . 10 (𝜑 → (𝑁𝑀) ∈ (0...𝑁))
109 dvn2bss 24539 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
11015, 24, 108, 109syl3anc 1368 . . . . . . . . 9 (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
11128, 110eqsstrrd 3993 . . . . . . . 8 (𝜑𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)))
112103, 111eqssd 3971 . . . . . . 7 (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = 𝐴)
11397, 112eqtr3d 2861 . . . . . 6 (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴)
114 fss 6518 . . . . . . . 8 ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
11534, 20, 114sylancl 589 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
116 eqid 2824 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
117116tgioo2 23414 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
11893, 115, 1, 117, 116dvbssntr 24509 . . . . . 6 (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
119113, 118eqsstrrd 3993 . . . . 5 (𝜑𝐴 ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
12087, 119eqssd 3971 . . . 4 (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)
12185isopn3 21677 . . . . 5 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
12284, 1, 121sylancr 590 . . . 4 (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
123120, 122mpbird 260 . . 3 (𝜑𝐴 ∈ (topGen‘ran (,)))
124 eqid 2824 . . 3 (𝐴 ∖ {𝐵}) = (𝐴 ∖ {𝐵})
125 difss 4095 . . . 4 (𝐴 ∖ {𝐵}) ⊆ 𝐴
12635recnd 10668 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
127 dvnf 24536 . . . . . . . . . 10 ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ)
12815, 24, 100, 127syl3anc 1368 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ)
129112feq2d 6490 . . . . . . . . 9 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℂ))
130128, 129mpbid 235 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℂ)
131130ffvelrnda 6843 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
132 dvnfre 24561 . . . . . . . . . . 11 ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ)
1332, 1, 100, 132syl3anc 1368 . . . . . . . . . 10 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ)
134112feq2d 6490 . . . . . . . . . 10 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁𝑀))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℝ))
135133, 134mpbid 235 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)):𝐴⟶ℝ)
136135feqmptd 6725 . . . . . . . 8 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁𝑀)) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦)))
13734feqmptd 6725 . . . . . . . . 9 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
138137oveq2d 7166 . . . . . . . 8 (𝜑 → (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = (ℝ D (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
13996, 136, 1383eqtr3rd 2868 . . . . . . 7 (𝜑 → (ℝ D (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦)))
14068recnd 10668 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
141 fvexd 6677 . . . . . . 7 ((𝜑𝑦𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ V)
14267recnd 10668 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
143 recn 10626 . . . . . . . . 9 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
144 dvnply2 24889 . . . . . . . . . . . 12 ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁𝑀) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ))
14541, 61, 100, 144syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ))
146 plyf 24801 . . . . . . . . . . 11 (((ℂ D𝑛 𝑇)‘(𝑁𝑀)) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)):ℂ⟶ℂ)
147145, 146syl 17 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)):ℂ⟶ℂ)
148147ffvelrnda 6843 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
149143, 148sylan2 595 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) ∈ ℂ)
150116cnfldtopon 23394 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
151 toponmax 21537 . . . . . . . . . 10 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
152150, 151mp1i 13 . . . . . . . . 9 (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
153 df-ss 3937 . . . . . . . . . 10 (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
15493, 153sylib 221 . . . . . . . . 9 (𝜑 → (ℝ ∩ ℂ) = ℝ)
155 plyf 24801 . . . . . . . . . . 11 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
15663, 155syl 17 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
157156ffvelrnda 6843 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
15891fveq2d 6666 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℂ D𝑛 𝑇)‘(𝑁𝑀)))
159 ssid 3976 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
160159a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ⊆ ℂ)
161 mapsspm 8437 . . . . . . . . . . . . 13 (ℂ ↑m ℂ) ⊆ (ℂ ↑pm ℂ)
162 plyf 24801 . . . . . . . . . . . . . . 15 (𝑇 ∈ (Poly‘ℝ) → 𝑇:ℂ⟶ℂ)
16361, 162syl 17 . . . . . . . . . . . . . 14 (𝜑𝑇:ℂ⟶ℂ)
16416, 16elmap 8432 . . . . . . . . . . . . . 14 (𝑇 ∈ (ℂ ↑m ℂ) ↔ 𝑇:ℂ⟶ℂ)
165163, 164sylibr 237 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ (ℂ ↑m ℂ))
166161, 165sseldi 3952 . . . . . . . . . . . 12 (𝜑𝑇 ∈ (ℂ ↑pm ℂ))
167 dvnp1 24534 . . . . . . . . . . . 12 ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
168160, 166, 11, 167syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
169158, 168eqtr3d 2861 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
170147feqmptd 6725 . . . . . . . . . 10 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁𝑀)) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
171156feqmptd 6725 . . . . . . . . . . 11 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
172171oveq2d 7166 . . . . . . . . . 10 (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
173169, 170, 1723eqtr3rd 2868 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
174116, 15, 152, 154, 157, 148, 173dvmptres3 24565 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
17515, 142, 149, 174, 1, 117, 116, 123dvmptres 24572 . . . . . . 7 (𝜑 → (ℝ D (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
17615, 126, 131, 139, 140, 141, 175dvmptsub 24576 . . . . . 6 (𝜑 → (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))))
177176dmeqd 5762 . . . . 5 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = dom (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))))
178 ovex 7183 . . . . . 6 ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)) ∈ V
179 eqid 2824 . . . . . 6 (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))
180178, 179dmmpti 6482 . . . . 5 dom (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦))) = 𝐴
181177, 180syl6eq 2875 . . . 4 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = 𝐴)
182125, 181sseqtrrid 4007 . . 3 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))))
183 simpr 488 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
18447adantr 484 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℂ) → 𝐵 ∈ ℝ)
185184recnd 10668 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝐵 ∈ ℂ)
186183, 185subcld 10996 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑦𝐵) ∈ ℂ)
18777adantr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑀 ∈ ℕ0)
18879a1i 11 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 1 ∈ ℕ0)
189187, 188nn0addcld 11959 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
190186, 189expcld 13518 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
191143, 190sylan2 595 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
19289adantr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝑀 ∈ ℂ)
193 1cnd 10635 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 1 ∈ ℂ)
194192, 193addcld 10659 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℂ)
195186, 187expcld 13518 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → ((𝑦𝐵)↑𝑀) ∈ ℂ)
196194, 195mulcld 10660 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ ℂ)
197143, 196sylan2 595 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ ℂ)
19816prid2 4685 . . . . . . . . . . 11 ℂ ∈ {ℝ, ℂ}
199198a1i 11 . . . . . . . . . 10 (𝜑 → ℂ ∈ {ℝ, ℂ})
200 simpr 488 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
201 elfznn 12943 . . . . . . . . . . . . . 14 ((𝑀 + 1) ∈ (1...𝑁) → (𝑀 + 1) ∈ ℕ)
2026, 201syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀 + 1) ∈ ℕ)
203202nnnn0d 11955 . . . . . . . . . . . 12 (𝜑 → (𝑀 + 1) ∈ ℕ0)
204203adantr 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
205200, 204expcld 13518 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝑥↑(𝑀 + 1)) ∈ ℂ)
206 ovexd 7185 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → ((𝑀 + 1) · (𝑥𝑀)) ∈ V)
207199dvmptid 24566 . . . . . . . . . . . 12 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
208 0cnd 10633 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℂ) → 0 ∈ ℂ)
20947recnd 10668 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℂ)
210199, 209dvmptc 24567 . . . . . . . . . . . 12 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝐵)) = (𝑦 ∈ ℂ ↦ 0))
211199, 183, 193, 207, 185, 208, 210dvmptsub 24576 . . . . . . . . . . 11 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝐵))) = (𝑦 ∈ ℂ ↦ (1 − 0)))
212 1m0e1 11758 . . . . . . . . . . . 12 (1 − 0) = 1
213212mpteq2i 5145 . . . . . . . . . . 11 (𝑦 ∈ ℂ ↦ (1 − 0)) = (𝑦 ∈ ℂ ↦ 1)
214211, 213syl6eq 2875 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝐵))) = (𝑦 ∈ ℂ ↦ 1))
215 dvexp 24562 . . . . . . . . . . . 12 ((𝑀 + 1) ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
216202, 215syl 17 . . . . . . . . . . 11 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
21789, 90pncand 10997 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
218217oveq2d 7166 . . . . . . . . . . . . 13 (𝜑 → (𝑥↑((𝑀 + 1) − 1)) = (𝑥𝑀))
219218oveq2d 7166 . . . . . . . . . . . 12 (𝜑 → ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))) = ((𝑀 + 1) · (𝑥𝑀)))
220219mpteq2dv 5149 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥𝑀))))
221216, 220eqtrd 2859 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥𝑀))))
222 oveq1 7157 . . . . . . . . . 10 (𝑥 = (𝑦𝐵) → (𝑥↑(𝑀 + 1)) = ((𝑦𝐵)↑(𝑀 + 1)))
223 oveq1 7157 . . . . . . . . . . 11 (𝑥 = (𝑦𝐵) → (𝑥𝑀) = ((𝑦𝐵)↑𝑀))
224223oveq2d 7166 . . . . . . . . . 10 (𝑥 = (𝑦𝐵) → ((𝑀 + 1) · (𝑥𝑀)) = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
225199, 199, 186, 193, 205, 206, 214, 221, 222, 224dvmptco 24581 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1)))
226196mulid1d 10657 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1) = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
227226mpteq2dva 5148 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) · 1)) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
228225, 227eqtrd 2859 . . . . . . . 8 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
229116, 15, 152, 154, 190, 196, 228dvmptres3 24565 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℝ ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
23015, 191, 197, 229, 1, 117, 116, 123dvmptres 24572 . . . . . 6 (𝜑 → (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
231230dmeqd 5762 . . . . 5 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = dom (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
232 ovex 7183 . . . . . 6 ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ∈ V
233 eqid 2824 . . . . . 6 (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) = (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
234232, 233dmmpti 6482 . . . . 5 dom (𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) = 𝐴
235231, 234syl6eq 2875 . . . 4 (𝜑 → dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = 𝐴)
236125, 235sseqtrrid 4007 . . 3 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))))
23715, 22, 1, 9, 45, 46dvntaylp0 24973 . . . . . 6 (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
238237oveq2d 7166 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
239115, 44ffvelrnd 6844 . . . . . 6 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) ∈ ℂ)
240239subidd 10984 . . . . 5 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
241238, 240eqtrd 2859 . . . 4 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
242116subcn 23477 . . . . . . 7 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
243242a1i 11 . . . . . 6 (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
244 dvcn 24530 . . . . . . . 8 (((ℝ ⊆ ℂ ∧ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴cn→ℂ))
24593, 115, 1, 113, 244syl31anc 1370 . . . . . . 7 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴cn→ℂ))
246137, 245eqeltrrd 2917 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴cn→ℂ))
247 plycn 24864 . . . . . . . 8 (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
24863, 247syl 17 . . . . . . 7 (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
2491, 20sstrdi 3966 . . . . . . . 8 (𝜑𝐴 ⊆ ℂ)
250 cncfmptid 23524 . . . . . . . 8 ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑦𝐴𝑦) ∈ (𝐴cn→ℂ))
251249, 159, 250sylancl 589 . . . . . . 7 (𝜑 → (𝑦𝐴𝑦) ∈ (𝐴cn→ℂ))
252248, 251cncfmpt1f 23525 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴cn→ℂ))
253116, 243, 246, 252cncfmpt2f 23526 . . . . 5 (𝜑 → (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) ∈ (𝐴cn→ℂ))
254 fveq2 6662 . . . . . 6 (𝑦 = 𝐵 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
255 fveq2 6662 . . . . . 6 (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵))
256254, 255oveq12d 7168 . . . . 5 (𝑦 = 𝐵 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
257253, 44, 256cnmptlimc 24499 . . . 4 (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) ∈ ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim 𝐵))
258241, 257eqeltrrd 2917 . . 3 (𝜑 → 0 ∈ ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim 𝐵))
259209subidd 10984 . . . . . 6 (𝜑 → (𝐵𝐵) = 0)
260259oveq1d 7165 . . . . 5 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) = (0↑(𝑀 + 1)))
2612020expd 13511 . . . . 5 (𝜑 → (0↑(𝑀 + 1)) = 0)
262260, 261eqtrd 2859 . . . 4 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) = 0)
263249sselda 3954 . . . . . . . 8 ((𝜑𝑦𝐴) → 𝑦 ∈ ℂ)
264263, 190syldan 594 . . . . . . 7 ((𝜑𝑦𝐴) → ((𝑦𝐵)↑(𝑀 + 1)) ∈ ℂ)
265264fmpttd 6871 . . . . . 6 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℂ)
266 dvcn 24530 . . . . . 6 (((ℝ ⊆ ℂ ∧ (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) = 𝐴) → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ∈ (𝐴cn→ℂ))
26793, 265, 1, 235, 266syl31anc 1370 . . . . 5 (𝜑 → (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ∈ (𝐴cn→ℂ))
268 oveq1 7157 . . . . . 6 (𝑦 = 𝐵 → (𝑦𝐵) = (𝐵𝐵))
269268oveq1d 7165 . . . . 5 (𝑦 = 𝐵 → ((𝑦𝐵)↑(𝑀 + 1)) = ((𝐵𝐵)↑(𝑀 + 1)))
270267, 44, 269cnmptlimc 24499 . . . 4 (𝜑 → ((𝐵𝐵)↑(𝑀 + 1)) ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) lim 𝐵))
271262, 270eqeltrrd 2917 . . 3 (𝜑 → 0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) lim 𝐵))
272249ssdifssd 4106 . . . . . . . . . 10 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
273272sselda 3954 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℂ)
274209adantr 484 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
275273, 274subcld 10996 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦𝐵) ∈ ℂ)
276 eldifsni 4708 . . . . . . . . . 10 (𝑦 ∈ (𝐴 ∖ {𝐵}) → 𝑦𝐵)
277276adantl 485 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦𝐵)
278273, 274, 277subne0d 11005 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦𝐵) ≠ 0)
279202adantr 484 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
280279nnzd 12086 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℤ)
281275, 278, 280expne0d 13524 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑(𝑀 + 1)) ≠ 0)
282281necomd 3069 . . . . . 6 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑦𝐵)↑(𝑀 + 1)))
283282neneqd 3019 . . . . 5 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑦𝐵)↑(𝑀 + 1)))
284283nrexdv 3263 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
285 df-ima 5556 . . . . . 6 ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵}))
286285eleq2i 2907 . . . . 5 (0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})))
287 resmpt 5893 . . . . . . 7 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦𝐵)↑(𝑀 + 1))))
288125, 287ax-mp 5 . . . . . 6 ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦𝐵)↑(𝑀 + 1)))
289 ovex 7183 . . . . . 6 ((𝑦𝐵)↑(𝑀 + 1)) ∈ V
290288, 289elrnmpti 5820 . . . . 5 (0 ∈ ran ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
291286, 290bitri 278 . . . 4 (0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦𝐵)↑(𝑀 + 1)))
292284, 291sylnibr 332 . . 3 (𝜑 → ¬ 0 ∈ ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})))
29389adantr 484 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℂ)
294 1cnd 10635 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 1 ∈ ℂ)
295293, 294addcld 10659 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
296273, 195syldan 594 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑𝑀) ∈ ℂ)
297279nnne0d 11687 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
29876adantr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ)
299298nnzd 12086 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
300275, 278, 299expne0d 13524 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐵)↑𝑀) ≠ 0)
301295, 296, 297, 300mulne0d 11291 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) ≠ 0)
302301necomd 3069 . . . . . 6 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
303302neneqd 3019 . . . . 5 ((𝜑𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
304303nrexdv 3263 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
305230imaeq1d 5916 . . . . . . 7 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})))
306 df-ima 5556 . . . . . . 7 ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))
307305, 306syl6eq 2875 . . . . . 6 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})))
308307eleq2d 2901 . . . . 5 (𝜑 → (0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))))
309 resmpt 5893 . . . . . . 7 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
310125, 309ax-mp 5 . . . . . 6 ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
311310, 232elrnmpti 5820 . . . . 5 (0 ∈ ran ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))
312308, 311syl6bb 290 . . . 4 (𝜑 → (0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦𝐵)↑𝑀))))
313304, 312mtbird 328 . . 3 (𝜑 → ¬ 0 ∈ ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})))
314 eldifi 4090 . . . . . . . 8 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐴)
315130ffvelrnda 6843 . . . . . . . 8 ((𝜑𝑥𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
316314, 315sylan2 595 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
3171ssdifssd 4106 . . . . . . . . . 10 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℝ)
318317sselda 3954 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ)
319318recnd 10668 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
320147ffvelrnda 6843 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
321319, 320syldan 594 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥) ∈ ℂ)
322316, 321subcld 10996 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) ∈ ℂ)
32347adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℝ)
324318, 323resubcld 11067 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℝ)
32577adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ0)
326324, 325reexpcld 13535 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ∈ ℝ)
327326recnd 10668 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ∈ ℂ)
328323recnd 10668 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
329319, 328subcld 10996 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ∈ ℂ)
330 eldifsni 4708 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥𝐵)
331330adantl 485 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥𝐵)
332319, 328, 331subne0d 11005 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥𝐵) ≠ 0)
333325nn0zd 12085 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
334329, 332, 333expne0d 13524 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥𝐵)↑𝑀) ≠ 0)
335322, 327, 334divcld 11415 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) ∈ ℂ)
336202nnrecred 11688 . . . . . . 7 (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
337336recnd 10668 . . . . . 6 (𝜑 → (1 / (𝑀 + 1)) ∈ ℂ)
338337adantr 484 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (1 / (𝑀 + 1)) ∈ ℂ)
339 txtopon 22202 . . . . . . 7 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
340150, 150, 339mp2an 691 . . . . . 6 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
341340toponrestid 21532 . . . . 5 ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
342 taylthlem2.i . . . . 5 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀))) lim 𝐵))
343 limcresi 24494 . . . . . . 7 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵) ⊆ (((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵)
344 resmpt 5893 . . . . . . . . 9 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))))
345125, 344ax-mp 5 . . . . . . . 8 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1)))
346345oveq1i 7160 . . . . . . 7 (((𝑥𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵)
347343, 346sseqtri 3990 . . . . . 6 ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵) ⊆ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵)
348 cncfmptc 23523 . . . . . . . 8 (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝐴 ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑥𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴cn→ℝ))
349336, 249, 93, 348syl3anc 1368 . . . . . . 7 (𝜑 → (𝑥𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴cn→ℝ))
350 eqidd 2825 . . . . . . 7 (𝑥 = 𝐵 → (1 / (𝑀 + 1)) = (1 / (𝑀 + 1)))
351349, 44, 350cnmptlimc 24499 . . . . . 6 (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥𝐴 ↦ (1 / (𝑀 + 1))) lim 𝐵))
352347, 351sseldi 3952 . . . . 5 (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim 𝐵))
353116mulcn 23478 . . . . . 6 · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
354 0cn 10632 . . . . . . 7 0 ∈ ℂ
355 opelxpi 5580 . . . . . . 7 ((0 ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
356354, 337, 355sylancr 590 . . . . . 6 (𝜑 → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
357340toponunii 21527 . . . . . . 7 (ℂ × ℂ) = ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
358357cncnpi 21889 . . . . . 6 (( · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ)) → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
359353, 356, 358sylancr 590 . . . . 5 (𝜑 → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
360335, 338, 160, 160, 116, 341, 342, 352, 359limccnp2 24501 . . . 4 (𝜑 → (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim 𝐵))
361337mul02d 10837 . . . 4 (𝜑 → (0 · (1 / (𝑀 + 1))) = 0)
362176fveq1d 6664 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥))
363 fveq2 6662 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥))
364 fveq2 6662 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥))
365363, 364oveq12d 7168 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
366 ovex 7183 . . . . . . . . . . 11 ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) ∈ V
367365, 179, 366fvmpt 6760 . . . . . . . . . 10 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
368314, 367syl 17 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
369362, 368sylan9eq 2879 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)))
370230fveq1d 6664 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥))
371 oveq1 7157 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦𝐵) = (𝑥𝐵))
372371oveq1d 7165 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝑦𝐵)↑𝑀) = ((𝑥𝐵)↑𝑀))
373372oveq2d 7166 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
374 ovex 7183 . . . . . . . . . . . 12 ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)) ∈ V
375373, 233, 374fvmpt 6760 . . . . . . . . . . 11 (𝑥𝐴 → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
376314, 375syl 17 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦𝐴 ↦ ((𝑀 + 1) · ((𝑦𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
377370, 376sylan9eq 2879 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)))
378202adantr 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
379378nncnd 11653 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
380379, 327mulcomd 10661 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑥𝐵)↑𝑀)) = (((𝑥𝐵)↑𝑀) · (𝑀 + 1)))
381377, 380eqtrd 2859 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥) = (((𝑥𝐵)↑𝑀) · (𝑀 + 1)))
382369, 381oveq12d 7168 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / (((𝑥𝐵)↑𝑀) · (𝑀 + 1))))
383378nnne0d 11687 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
384322, 327, 379, 334, 383divdiv1d 11446 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) / (𝑀 + 1)) = (((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / (((𝑥𝐵)↑𝑀) · (𝑀 + 1))))
385335, 379, 383divrecd 11418 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) / (𝑀 + 1)) = ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
386382, 384, 3853eqtr2rd 2866 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥)))
387386mpteq2dva 5148 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))))
388387oveq1d 7165 . . . 4 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁𝑀))‘𝑥)) / ((𝑥𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))) lim 𝐵))
389360, 361, 3883eltr3d 2930 . . 3 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))))‘𝑥))) lim 𝐵))
3901, 70, 83, 123, 44, 124, 182, 236, 258, 271, 292, 313, 389lhop 24625 . 2 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) lim 𝐵))
391314adantl 485 . . . . . 6 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥𝐴)
392 fveq2 6662 . . . . . . . 8 (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥))
393 fveq2 6662 . . . . . . . 8 (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))
394392, 393oveq12d 7168 . . . . . . 7 (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
395 eqid 2824 . . . . . . 7 (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
396 ovex 7183 . . . . . . 7 ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) ∈ V
397394, 395, 396fvmpt 6760 . . . . . 6 (𝑥𝐴 → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
398391, 397syl 17 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
399371oveq1d 7165 . . . . . . 7 (𝑦 = 𝑥 → ((𝑦𝐵)↑(𝑀 + 1)) = ((𝑥𝐵)↑(𝑀 + 1)))
400 eqid 2824 . . . . . . 7 (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1))) = (𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))
401 ovex 7183 . . . . . . 7 ((𝑥𝐵)↑(𝑀 + 1)) ∈ V
402399, 400, 401fvmpt 6760 . . . . . 6 (𝑥𝐴 → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥𝐵)↑(𝑀 + 1)))
403391, 402syl 17 . . . . 5 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥𝐵)↑(𝑀 + 1)))
404398, 403oveq12d 7168 . . . 4 ((𝜑𝑥 ∈ (𝐴 ∖ {𝐵})) → (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1))))
405404mpteq2dva 5148 . . 3 (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))))
406405oveq1d 7165 . 2 (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦𝐴 ↦ ((𝑦𝐵)↑(𝑀 + 1)))‘𝑥))) lim 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))) lim 𝐵))
407390, 406eleqtrd 2918 1 (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥𝐵)↑(𝑀 + 1)))) lim 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  ∃wrex 3134  Vcvv 3481   ∖ cdif 3917   ∩ cin 3919   ⊆ wss 3920  {csn 4551  {cpr 4553  ⟨cop 4557   class class class wbr 5053   ↦ cmpt 5133   × cxp 5541  dom cdm 5543  ran crn 5544   ↾ cres 5545   “ cima 5546  ⟶wf 6340  ‘cfv 6344  (class class class)co 7150   ↑m cmap 8403   ↑pm cpm 8404  ℂcc 10534  ℝcr 10535  0cc0 10536  1c1 10537   + caddc 10539   · cmul 10541   ≤ cle 10675   − cmin 10869   / cdiv 11296  ℕcn 11637  ℕ0cn0 11897  ℤ≥cuz 12243  (,)cioo 12738  ...cfz 12897  ..^cfzo 13040  ↑cexp 13437  !cfa 13641  TopOpenctopn 16698  topGenctg 16714  DivRingcdr 19505  SubRingcsubrg 19534  ℂfldccnfld 20548  ℝfldcrefld 20751  Topctop 21504  TopOnctopon 21521  intcnt 21628   Cn ccn 21835   CnP ccnp 21836   ×t ctx 22171  –cn→ccncf 23487   limℂ climc 24471   D cdv 24472   D𝑛 cdvn 24473  Polycply 24787  degcdgr 24790   Tayl ctayl 24954 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7456  ax-inf2 9102  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613  ax-pre-sup 10614  ax-addf 10615  ax-mulf 10616 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3483  df-sbc 3760  df-csb 3868  df-dif 3923  df-un 3925  df-in 3927  df-ss 3937  df-pss 3939  df-nul 4278  df-if 4452  df-pw 4525  df-sn 4552  df-pr 4554  df-tp 4556  df-op 4558  df-uni 4826  df-int 4864  df-iun 4908  df-iin 4909  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-isom 6353  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7404  df-om 7576  df-1st 7685  df-2nd 7686  df-supp 7828  df-tpos 7889  df-wrecs 7944  df-recs 8005  df-rdg 8043  df-1o 8099  df-2o 8100  df-oadd 8103  df-er 8286  df-map 8405  df-pm 8406  df-ixp 8459  df-en 8507  df-dom 8508  df-sdom 8509  df-fin 8510  df-fsupp 8832  df-fi 8873  df-sup 8904  df-inf 8905  df-oi 8972  df-card 9366  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-div 11297  df-nn 11638  df-2 11700  df-3 11701  df-4 11702  df-5 11703  df-6 11704  df-7 11705  df-8 11706  df-9 11707  df-n0 11898  df-xnn0 11968  df-z 11982  df-dec 12099  df-uz 12244  df-q 12349  df-rp 12390  df-xneg 12507  df-xadd 12508  df-xmul 12509  df-ioo 12742  df-ioc 12743  df-ico 12744  df-icc 12745  df-fz 12898  df-fzo 13041  df-fl 13169  df-seq 13377  df-exp 13438  df-fac 13642  df-hash 13699  df-cj 14461  df-re 14462  df-im 14463  df-sqrt 14597  df-abs 14598  df-clim 14848  df-rlim 14849  df-sum 15046  df-struct 16488  df-ndx 16489  df-slot 16490  df-base 16492  df-sets 16493  df-ress 16494  df-plusg 16581  df-mulr 16582  df-starv 16583  df-sca 16584  df-vsca 16585  df-ip 16586  df-tset 16587  df-ple 16588  df-ds 16590  df-unif 16591  df-hom 16592  df-cco 16593  df-rest 16699  df-topn 16700  df-0g 16718  df-gsum 16719  df-topgen 16720  df-pt 16721  df-prds 16724  df-xrs 16778  df-qtop 16783  df-imas 16784  df-xps 16786  df-mre 16860  df-mrc 16861  df-acs 16863  df-mgm 17855  df-sgrp 17904  df-mnd 17915  df-submnd 17960  df-grp 18109  df-minusg 18110  df-mulg 18228  df-subg 18279  df-cntz 18450  df-cmn 18911  df-abl 18912  df-mgp 19243  df-ur 19255  df-ring 19302  df-cring 19303  df-oppr 19379  df-dvdsr 19397  df-unit 19398  df-invr 19428  df-dvr 19439  df-drng 19507  df-subrg 19536  df-psmet 20540  df-xmet 20541  df-met 20542  df-bl 20543  df-mopn 20544  df-fbas 20545  df-fg 20546  df-cnfld 20549  df-refld 20752  df-top 21505  df-topon 21522  df-topsp 21544  df-bases 21557  df-cld 21630  df-ntr 21631  df-cls 21632  df-nei 21709  df-lp 21747  df-perf 21748  df-cn 21838  df-cnp 21839  df-haus 21926  df-cmp 21998  df-tx 22173  df-hmeo 22366  df-fil 22457  df-fm 22549  df-flim 22550  df-flf 22551  df-tsms 22738  df-xms 22933  df-ms 22934  df-tms 22935  df-cncf 23489  df-0p 24280  df-limc 24475  df-dv 24476  df-dvn 24477  df-ply 24791  df-idp 24792  df-coe 24793  df-dgr 24794  df-tayl 24956 This theorem is referenced by:  taylth  24976
 Copyright terms: Public domain W3C validator