Metamath Proof Explorer


Theorem tayl0

Description: The Taylor series is always defined at the basepoint, with value equal to the value of the function. (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses taylfval.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
taylfval.f ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
taylfval.a ( 𝜑𝐴𝑆 )
taylfval.n ( 𝜑 → ( 𝑁 ∈ ℕ0𝑁 = +∞ ) )
taylfval.b ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
taylfval.t 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
Assertion tayl0 ( 𝜑 → ( 𝐵 ∈ dom 𝑇 ∧ ( 𝑇𝐵 ) = ( 𝐹𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 taylfval.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 taylfval.f ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
3 taylfval.a ( 𝜑𝐴𝑆 )
4 taylfval.n ( 𝜑 → ( 𝑁 ∈ ℕ0𝑁 = +∞ ) )
5 taylfval.b ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
6 taylfval.t 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7 recnprss ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
8 1 7 syl ( 𝜑𝑆 ⊆ ℂ )
9 3 8 sstrd ( 𝜑𝐴 ⊆ ℂ )
10 fveq2 ( 𝑘 = 0 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) )
11 10 dmeqd ( 𝑘 = 0 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) = dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) )
12 11 eleq2d ( 𝑘 = 0 → ( 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ↔ 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) )
13 5 ralrimiva ( 𝜑 → ∀ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
14 elxnn0 ( 𝑁 ∈ ℕ0* ↔ ( 𝑁 ∈ ℕ0𝑁 = +∞ ) )
15 0xr 0 ∈ ℝ*
16 15 a1i ( 𝑁 ∈ ℕ0* → 0 ∈ ℝ* )
17 xnn0xr ( 𝑁 ∈ ℕ0*𝑁 ∈ ℝ* )
18 xnn0ge0 ( 𝑁 ∈ ℕ0* → 0 ≤ 𝑁 )
19 lbicc2 ( ( 0 ∈ ℝ*𝑁 ∈ ℝ* ∧ 0 ≤ 𝑁 ) → 0 ∈ ( 0 [,] 𝑁 ) )
20 16 17 18 19 syl3anc ( 𝑁 ∈ ℕ0* → 0 ∈ ( 0 [,] 𝑁 ) )
21 14 20 sylbir ( ( 𝑁 ∈ ℕ0𝑁 = +∞ ) → 0 ∈ ( 0 [,] 𝑁 ) )
22 4 21 syl ( 𝜑 → 0 ∈ ( 0 [,] 𝑁 ) )
23 0zd ( 𝜑 → 0 ∈ ℤ )
24 22 23 elind ( 𝜑 → 0 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
25 12 13 24 rspcdva ( 𝜑𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) )
26 cnex ℂ ∈ V
27 26 a1i ( 𝜑 → ℂ ∈ V )
28 elpm2r ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
29 27 1 2 3 28 syl22anc ( 𝜑𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
30 dvn0 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
31 8 29 30 syl2anc ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
32 31 dmeqd ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = dom 𝐹 )
33 2 fdmd ( 𝜑 → dom 𝐹 = 𝐴 )
34 32 33 eqtrd ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐴 )
35 25 34 eleqtrd ( 𝜑𝐵𝐴 )
36 9 35 sseldd ( 𝜑𝐵 ∈ ℂ )
37 cnfldbas ℂ = ( Base ‘ ℂfld )
38 cnfld0 0 = ( 0g ‘ ℂfld )
39 cnring fld ∈ Ring
40 ringmnd ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
41 39 40 mp1i ( 𝜑 → ℂfld ∈ Mnd )
42 ovex ( 0 [,] 𝑁 ) ∈ V
43 42 inex1 ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V
44 43 a1i ( 𝜑 → ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V )
45 1 adantr ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑆 ∈ { ℝ , ℂ } )
46 29 adantr ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
47 simpr ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
48 47 elin2d ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑘 ∈ ℤ )
49 47 elin1d ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑘 ∈ ( 0 [,] 𝑁 ) )
50 nn0re ( 𝑁 ∈ ℕ0𝑁 ∈ ℝ )
51 50 rexrd ( 𝑁 ∈ ℕ0𝑁 ∈ ℝ* )
52 id ( 𝑁 = +∞ → 𝑁 = +∞ )
53 pnfxr +∞ ∈ ℝ*
54 52 53 eqeltrdi ( 𝑁 = +∞ → 𝑁 ∈ ℝ* )
55 51 54 jaoi ( ( 𝑁 ∈ ℕ0𝑁 = +∞ ) → 𝑁 ∈ ℝ* )
56 4 55 syl ( 𝜑𝑁 ∈ ℝ* )
57 56 adantr ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑁 ∈ ℝ* )
58 elicc1 ( ( 0 ∈ ℝ*𝑁 ∈ ℝ* ) → ( 𝑘 ∈ ( 0 [,] 𝑁 ) ↔ ( 𝑘 ∈ ℝ* ∧ 0 ≤ 𝑘𝑘𝑁 ) ) )
59 15 57 58 sylancr ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( 𝑘 ∈ ( 0 [,] 𝑁 ) ↔ ( 𝑘 ∈ ℝ* ∧ 0 ≤ 𝑘𝑘𝑁 ) ) )
60 49 59 mpbid ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( 𝑘 ∈ ℝ* ∧ 0 ≤ 𝑘𝑘𝑁 ) )
61 60 simp2d ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 0 ≤ 𝑘 )
62 elnn0z ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ) )
63 48 61 62 sylanbrc ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑘 ∈ ℕ0 )
64 dvnf ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
65 45 46 63 64 syl3anc ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
66 65 5 ffvelrnd ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) ∈ ℂ )
67 63 faccld ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
68 67 nncnd ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
69 67 nnne0d ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
70 66 68 69 divcld ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
71 0cnd ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 0 ∈ ℂ )
72 71 63 expcld ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( 0 ↑ 𝑘 ) ∈ ℂ )
73 70 72 mulcld ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ∈ ℂ )
74 73 fmpttd ( 𝜑 → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) : ( ( 0 [,] 𝑁 ) ∩ ℤ ) ⟶ ℂ )
75 eldifi ( 𝑘 ∈ ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∖ { 0 } ) → 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
76 75 63 sylan2 ( ( 𝜑𝑘 ∈ ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∖ { 0 } ) ) → 𝑘 ∈ ℕ0 )
77 eldifsni ( 𝑘 ∈ ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∖ { 0 } ) → 𝑘 ≠ 0 )
78 77 adantl ( ( 𝜑𝑘 ∈ ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∖ { 0 } ) ) → 𝑘 ≠ 0 )
79 elnnne0 ( 𝑘 ∈ ℕ ↔ ( 𝑘 ∈ ℕ0𝑘 ≠ 0 ) )
80 76 78 79 sylanbrc ( ( 𝜑𝑘 ∈ ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∖ { 0 } ) ) → 𝑘 ∈ ℕ )
81 80 0expd ( ( 𝜑𝑘 ∈ ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∖ { 0 } ) ) → ( 0 ↑ 𝑘 ) = 0 )
82 81 oveq2d ( ( 𝜑𝑘 ∈ ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∖ { 0 } ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 0 ) )
83 70 mul01d ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 0 ) = 0 )
84 75 83 sylan2 ( ( 𝜑𝑘 ∈ ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∖ { 0 } ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 0 ) = 0 )
85 82 84 eqtrd ( ( 𝜑𝑘 ∈ ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∖ { 0 } ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) = 0 )
86 zex ℤ ∈ V
87 86 inex2 ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V
88 87 a1i ( 𝜑 → ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V )
89 85 88 suppss2 ( 𝜑 → ( ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) supp 0 ) ⊆ { 0 } )
90 37 38 41 44 24 74 89 gsumpt ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ) = ( ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ‘ 0 ) )
91 10 fveq1d ( 𝑘 = 0 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) = ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) )
92 fveq2 ( 𝑘 = 0 → ( ! ‘ 𝑘 ) = ( ! ‘ 0 ) )
93 fac0 ( ! ‘ 0 ) = 1
94 92 93 eqtrdi ( 𝑘 = 0 → ( ! ‘ 𝑘 ) = 1 )
95 91 94 oveq12d ( 𝑘 = 0 → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) = ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) / 1 ) )
96 oveq2 ( 𝑘 = 0 → ( 0 ↑ 𝑘 ) = ( 0 ↑ 0 ) )
97 0exp0e1 ( 0 ↑ 0 ) = 1
98 96 97 eqtrdi ( 𝑘 = 0 → ( 0 ↑ 𝑘 ) = 1 )
99 95 98 oveq12d ( 𝑘 = 0 → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) / 1 ) · 1 ) )
100 eqid ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) )
101 ovex ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) / 1 ) · 1 ) ∈ V
102 99 100 101 fvmpt ( 0 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) → ( ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ‘ 0 ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) / 1 ) · 1 ) )
103 24 102 syl ( 𝜑 → ( ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ‘ 0 ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) / 1 ) · 1 ) )
104 31 fveq1d ( 𝜑 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) = ( 𝐹𝐵 ) )
105 104 oveq1d ( 𝜑 → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) / 1 ) = ( ( 𝐹𝐵 ) / 1 ) )
106 2 35 ffvelrnd ( 𝜑 → ( 𝐹𝐵 ) ∈ ℂ )
107 106 div1d ( 𝜑 → ( ( 𝐹𝐵 ) / 1 ) = ( 𝐹𝐵 ) )
108 105 107 eqtrd ( 𝜑 → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) / 1 ) = ( 𝐹𝐵 ) )
109 108 oveq1d ( 𝜑 → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) / 1 ) · 1 ) = ( ( 𝐹𝐵 ) · 1 ) )
110 106 mulid1d ( 𝜑 → ( ( 𝐹𝐵 ) · 1 ) = ( 𝐹𝐵 ) )
111 109 110 eqtrd ( 𝜑 → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ‘ 𝐵 ) / 1 ) · 1 ) = ( 𝐹𝐵 ) )
112 90 103 111 3eqtrd ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ) = ( 𝐹𝐵 ) )
113 ringcmn ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
114 39 113 mp1i ( 𝜑 → ℂfld ∈ CMnd )
115 cnfldtps fld ∈ TopSp
116 115 a1i ( 𝜑 → ℂfld ∈ TopSp )
117 mptexg ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ∈ V )
118 87 117 mp1i ( 𝜑 → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ∈ V )
119 funmpt Fun ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) )
120 119 a1i ( 𝜑 → Fun ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) )
121 c0ex 0 ∈ V
122 121 a1i ( 𝜑 → 0 ∈ V )
123 snfi { 0 } ∈ Fin
124 123 a1i ( 𝜑 → { 0 } ∈ Fin )
125 suppssfifsupp ( ( ( ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ∧ 0 ∈ V ) ∧ ( { 0 } ∈ Fin ∧ ( ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) supp 0 ) ⊆ { 0 } ) ) → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) finSupp 0 )
126 118 120 122 124 89 125 syl32anc ( 𝜑 → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) finSupp 0 )
127 37 38 114 116 44 74 126 tsmsid ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ) ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ) )
128 112 127 eqeltrrd ( 𝜑 → ( 𝐹𝐵 ) ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ) )
129 36 subidd ( 𝜑 → ( 𝐵𝐵 ) = 0 )
130 129 oveq1d ( 𝜑 → ( ( 𝐵𝐵 ) ↑ 𝑘 ) = ( 0 ↑ 𝑘 ) )
131 130 oveq2d ( 𝜑 → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝐵𝐵 ) ↑ 𝑘 ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) )
132 131 mpteq2dv ( 𝜑 → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝐵𝐵 ) ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) )
133 132 oveq2d ( 𝜑 → ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝐵𝐵 ) ↑ 𝑘 ) ) ) ) = ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 0 ↑ 𝑘 ) ) ) ) )
134 128 133 eleqtrrd ( 𝜑 → ( 𝐹𝐵 ) ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝐵𝐵 ) ↑ 𝑘 ) ) ) ) )
135 1 2 3 4 5 6 eltayl ( 𝜑 → ( 𝐵 𝑇 ( 𝐹𝐵 ) ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐹𝐵 ) ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝐵𝐵 ) ↑ 𝑘 ) ) ) ) ) ) )
136 36 134 135 mpbir2and ( 𝜑𝐵 𝑇 ( 𝐹𝐵 ) )
137 1 2 3 4 5 6 taylf ( 𝜑𝑇 : dom 𝑇 ⟶ ℂ )
138 ffun ( 𝑇 : dom 𝑇 ⟶ ℂ → Fun 𝑇 )
139 funbrfv2b ( Fun 𝑇 → ( 𝐵 𝑇 ( 𝐹𝐵 ) ↔ ( 𝐵 ∈ dom 𝑇 ∧ ( 𝑇𝐵 ) = ( 𝐹𝐵 ) ) ) )
140 137 138 139 3syl ( 𝜑 → ( 𝐵 𝑇 ( 𝐹𝐵 ) ↔ ( 𝐵 ∈ dom 𝑇 ∧ ( 𝑇𝐵 ) = ( 𝐹𝐵 ) ) ) )
141 136 140 mpbid ( 𝜑 → ( 𝐵 ∈ dom 𝑇 ∧ ( 𝑇𝐵 ) = ( 𝐹𝐵 ) ) )