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 φ S
taylfval.f φ F : A
taylfval.a φ A S
taylfval.n φ N 0 N = +∞
taylfval.b φ k 0 N B dom S D n F k
taylfval.t T = N S Tayl F B
Assertion tayl0 φ B dom T T B = F B

Proof

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