# Metamath Proof Explorer

## Theorem stoweidlem17

Description: This lemma proves that the function g (as defined in BrosowskiDeutsh p. 91, at the end of page 91) belongs to the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem17.1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem17.2 ${⊢}{\phi }\to {N}\in ℕ$
stoweidlem17.3 ${⊢}{\phi }\to {X}:\left(0\dots {N}\right)⟶{A}$
stoweidlem17.4 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
stoweidlem17.5 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
stoweidlem17.6 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
stoweidlem17.7 ${⊢}{\phi }\to {E}\in ℝ$
stoweidlem17.8 ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
Assertion stoweidlem17 ${⊢}{\phi }\to \left({t}\in {T}⟼\sum _{{i}=0}^{{N}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}$

### Proof

Step Hyp Ref Expression
1 stoweidlem17.1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
2 stoweidlem17.2 ${⊢}{\phi }\to {N}\in ℕ$
3 stoweidlem17.3 ${⊢}{\phi }\to {X}:\left(0\dots {N}\right)⟶{A}$
4 stoweidlem17.4 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
5 stoweidlem17.5 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
6 stoweidlem17.6 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
7 stoweidlem17.7 ${⊢}{\phi }\to {E}\in ℝ$
8 stoweidlem17.8 ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
9 2 nnnn0d ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
10 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
11 9 10 eleqtrdi ${⊢}{\phi }\to {N}\in {ℤ}_{\ge 0}$
12 eluzfz2 ${⊢}{N}\in {ℤ}_{\ge 0}\to {N}\in \left(0\dots {N}\right)$
13 11 12 syl ${⊢}{\phi }\to {N}\in \left(0\dots {N}\right)$
14 13 ancli ${⊢}{\phi }\to \left({\phi }\wedge {N}\in \left(0\dots {N}\right)\right)$
15 eleq1 ${⊢}{n}=0\to \left({n}\in \left(0\dots {N}\right)↔0\in \left(0\dots {N}\right)\right)$
16 15 anbi2d ${⊢}{n}=0\to \left(\left({\phi }\wedge {n}\in \left(0\dots {N}\right)\right)↔\left({\phi }\wedge 0\in \left(0\dots {N}\right)\right)\right)$
17 oveq2 ${⊢}{n}=0\to \left(0\dots {n}\right)=\left(0\dots 0\right)$
18 17 sumeq1d ${⊢}{n}=0\to \sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)=\sum _{{i}=0}^{0}{E}{X}\left({i}\right)\left({t}\right)$
19 18 mpteq2dv ${⊢}{n}=0\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{0}{E}{X}\left({i}\right)\left({t}\right)\right)$
20 19 eleq1d ${⊢}{n}=0\to \left(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\sum _{{i}=0}^{0}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)$
21 16 20 imbi12d ${⊢}{n}=0\to \left(\left(\left({\phi }\wedge {n}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)↔\left(\left({\phi }\wedge 0\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{0}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)$
22 eleq1 ${⊢}{n}={m}\to \left({n}\in \left(0\dots {N}\right)↔{m}\in \left(0\dots {N}\right)\right)$
23 22 anbi2d ${⊢}{n}={m}\to \left(\left({\phi }\wedge {n}\in \left(0\dots {N}\right)\right)↔\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\right)$
24 oveq2 ${⊢}{n}={m}\to \left(0\dots {n}\right)=\left(0\dots {m}\right)$
25 24 sumeq1d ${⊢}{n}={m}\to \sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)=\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)$
26 25 mpteq2dv ${⊢}{n}={m}\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)$
27 26 eleq1d ${⊢}{n}={m}\to \left(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)$
28 23 27 imbi12d ${⊢}{n}={m}\to \left(\left(\left({\phi }\wedge {n}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)↔\left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)$
29 eleq1 ${⊢}{n}={m}+1\to \left({n}\in \left(0\dots {N}\right)↔{m}+1\in \left(0\dots {N}\right)\right)$
30 29 anbi2d ${⊢}{n}={m}+1\to \left(\left({\phi }\wedge {n}\in \left(0\dots {N}\right)\right)↔\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)$
31 oveq2 ${⊢}{n}={m}+1\to \left(0\dots {n}\right)=\left(0\dots {m}+1\right)$
32 31 sumeq1d ${⊢}{n}={m}+1\to \sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)=\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)$
33 32 mpteq2dv ${⊢}{n}={m}+1\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)\right)$
34 33 eleq1d ${⊢}{n}={m}+1\to \left(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)$
35 30 34 imbi12d ${⊢}{n}={m}+1\to \left(\left(\left({\phi }\wedge {n}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)↔\left(\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)$
36 eleq1 ${⊢}{n}={N}\to \left({n}\in \left(0\dots {N}\right)↔{N}\in \left(0\dots {N}\right)\right)$
37 36 anbi2d ${⊢}{n}={N}\to \left(\left({\phi }\wedge {n}\in \left(0\dots {N}\right)\right)↔\left({\phi }\wedge {N}\in \left(0\dots {N}\right)\right)\right)$
38 oveq2 ${⊢}{n}={N}\to \left(0\dots {n}\right)=\left(0\dots {N}\right)$
39 38 sumeq1d ${⊢}{n}={N}\to \sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)=\sum _{{i}=0}^{{N}}{E}{X}\left({i}\right)\left({t}\right)$
40 39 mpteq2dv ${⊢}{n}={N}\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{N}}{E}{X}\left({i}\right)\left({t}\right)\right)$
41 40 eleq1d ${⊢}{n}={N}\to \left(\left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\sum _{{i}=0}^{{N}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)$
42 37 41 imbi12d ${⊢}{n}={N}\to \left(\left(\left({\phi }\wedge {n}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{n}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)↔\left(\left({\phi }\wedge {N}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{N}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)$
43 0z ${⊢}0\in ℤ$
44 fzsn ${⊢}0\in ℤ\to \left(0\dots 0\right)=\left\{0\right\}$
45 43 44 ax-mp ${⊢}\left(0\dots 0\right)=\left\{0\right\}$
46 45 sumeq1i ${⊢}\sum _{{i}=0}^{0}{E}{X}\left({i}\right)\left({t}\right)=\sum _{{i}\in \left\{0\right\}}{E}{X}\left({i}\right)\left({t}\right)$
47 46 mpteq2i ${⊢}\left({t}\in {T}⟼\sum _{{i}=0}^{0}{E}{X}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼\sum _{{i}\in \left\{0\right\}}{E}{X}\left({i}\right)\left({t}\right)\right)$
48 7 adantr ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {E}\in ℝ$
49 48 recnd ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {E}\in ℂ$
50 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
51 nngt0 ${⊢}{N}\in ℕ\to 0<{N}$
52 0re ${⊢}0\in ℝ$
53 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
54 ltle ${⊢}\left(0\in ℝ\wedge {N}\in ℝ\right)\to \left(0<{N}\to 0\le {N}\right)$
55 52 53 54 sylancr ${⊢}{N}\in ℕ\to \left(0<{N}\to 0\le {N}\right)$
56 51 55 mpd ${⊢}{N}\in ℕ\to 0\le {N}$
57 50 56 jca ${⊢}{N}\in ℕ\to \left({N}\in ℤ\wedge 0\le {N}\right)$
58 2 57 syl ${⊢}{\phi }\to \left({N}\in ℤ\wedge 0\le {N}\right)$
59 43 eluz1i ${⊢}{N}\in {ℤ}_{\ge 0}↔\left({N}\in ℤ\wedge 0\le {N}\right)$
60 58 59 sylibr ${⊢}{\phi }\to {N}\in {ℤ}_{\ge 0}$
61 eluzfz1 ${⊢}{N}\in {ℤ}_{\ge 0}\to 0\in \left(0\dots {N}\right)$
62 60 61 syl ${⊢}{\phi }\to 0\in \left(0\dots {N}\right)$
63 3 62 ffvelrnd ${⊢}{\phi }\to {X}\left(0\right)\in {A}$
64 feq1 ${⊢}{f}={X}\left(0\right)\to \left({f}:{T}⟶ℝ↔{X}\left(0\right):{T}⟶ℝ\right)$
65 64 imbi2d ${⊢}{f}={X}\left(0\right)\to \left(\left({\phi }\to {f}:{T}⟶ℝ\right)↔\left({\phi }\to {X}\left(0\right):{T}⟶ℝ\right)\right)$
66 8 expcom ${⊢}{f}\in {A}\to \left({\phi }\to {f}:{T}⟶ℝ\right)$
67 65 66 vtoclga ${⊢}{X}\left(0\right)\in {A}\to \left({\phi }\to {X}\left(0\right):{T}⟶ℝ\right)$
68 63 67 mpcom ${⊢}{\phi }\to {X}\left(0\right):{T}⟶ℝ$
69 68 ffvelrnda ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {X}\left(0\right)\left({t}\right)\in ℝ$
70 69 recnd ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {X}\left(0\right)\left({t}\right)\in ℂ$
71 49 70 mulcld ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {E}{X}\left(0\right)\left({t}\right)\in ℂ$
72 fveq2 ${⊢}{i}=0\to {X}\left({i}\right)={X}\left(0\right)$
73 72 fveq1d ${⊢}{i}=0\to {X}\left({i}\right)\left({t}\right)={X}\left(0\right)\left({t}\right)$
74 73 oveq2d ${⊢}{i}=0\to {E}{X}\left({i}\right)\left({t}\right)={E}{X}\left(0\right)\left({t}\right)$
75 74 sumsn ${⊢}\left(0\in ℤ\wedge {E}{X}\left(0\right)\left({t}\right)\in ℂ\right)\to \sum _{{i}\in \left\{0\right\}}{E}{X}\left({i}\right)\left({t}\right)={E}{X}\left(0\right)\left({t}\right)$
76 43 71 75 sylancr ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \sum _{{i}\in \left\{0\right\}}{E}{X}\left({i}\right)\left({t}\right)={E}{X}\left(0\right)\left({t}\right)$
77 1 76 mpteq2da ${⊢}{\phi }\to \left({t}\in {T}⟼\sum _{{i}\in \left\{0\right\}}{E}{X}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼{E}{X}\left(0\right)\left({t}\right)\right)$
78 47 77 syl5eq ${⊢}{\phi }\to \left({t}\in {T}⟼\sum _{{i}=0}^{0}{E}{X}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼{E}{X}\left(0\right)\left({t}\right)\right)$
79 1 5 6 8 7 63 stoweidlem2 ${⊢}{\phi }\to \left({t}\in {T}⟼{E}{X}\left(0\right)\left({t}\right)\right)\in {A}$
80 78 79 eqeltrd ${⊢}{\phi }\to \left({t}\in {T}⟼\sum _{{i}=0}^{0}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}$
81 80 adantr ${⊢}\left({\phi }\wedge 0\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{0}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}$
82 eqidd ${⊢}{r}={t}\to {E}={E}$
83 82 cbvmptv ${⊢}\left({r}\in {T}⟼{E}\right)=\left({t}\in {T}⟼{E}\right)$
84 83 eqcomi ${⊢}\left({t}\in {T}⟼{E}\right)=\left({r}\in {T}⟼{E}\right)$
85 simpr ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {t}\in {T}$
86 84 82 85 48 fvmptd3 ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \left({t}\in {T}⟼{E}\right)\left({t}\right)={E}$
87 86 oveq1d ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)={E}{X}\left({m}+1\right)\left({t}\right)$
88 1 87 mpteq2da ${⊢}{\phi }\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)\right)=\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)$
89 88 adantr ${⊢}\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)\right)=\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)$
90 3 ffvelrnda ${⊢}\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to {X}\left({m}+1\right)\in {A}$
91 simpl ${⊢}\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to {\phi }$
92 id ${⊢}{x}={E}\to {x}={E}$
93 92 mpteq2dv ${⊢}{x}={E}\to \left({t}\in {T}⟼{x}\right)=\left({t}\in {T}⟼{E}\right)$
94 93 eleq1d ${⊢}{x}={E}\to \left(\left({t}\in {T}⟼{x}\right)\in {A}↔\left({t}\in {T}⟼{E}\right)\in {A}\right)$
95 94 imbi2d ${⊢}{x}={E}\to \left(\left({\phi }\to \left({t}\in {T}⟼{x}\right)\in {A}\right)↔\left({\phi }\to \left({t}\in {T}⟼{E}\right)\in {A}\right)\right)$
96 6 expcom ${⊢}{x}\in ℝ\to \left({\phi }\to \left({t}\in {T}⟼{x}\right)\in {A}\right)$
97 95 96 vtoclga ${⊢}{E}\in ℝ\to \left({\phi }\to \left({t}\in {T}⟼{E}\right)\in {A}\right)$
98 7 97 mpcom ${⊢}{\phi }\to \left({t}\in {T}⟼{E}\right)\in {A}$
99 98 adantr ${⊢}\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼{E}\right)\in {A}$
100 fveq1 ${⊢}{g}={X}\left({m}+1\right)\to {g}\left({t}\right)={X}\left({m}+1\right)\left({t}\right)$
101 100 oveq2d ${⊢}{g}={X}\left({m}+1\right)\to \left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)=\left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)$
102 101 mpteq2dv ${⊢}{g}={X}\left({m}+1\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)=\left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)\right)$
103 102 eleq1d ${⊢}{g}={X}\left({m}+1\right)\to \left(\left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)\right)\in {A}\right)$
104 103 imbi2d ${⊢}{g}={X}\left({m}+1\right)\to \left(\left(\left({\phi }\wedge \left({t}\in {T}⟼{E}\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)\in {A}\right)↔\left(\left({\phi }\wedge \left({t}\in {T}⟼{E}\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)\right)\in {A}\right)\right)$
105 83 eleq1i ${⊢}\left({r}\in {T}⟼{E}\right)\in {A}↔\left({t}\in {T}⟼{E}\right)\in {A}$
106 fveq1 ${⊢}{f}=\left({r}\in {T}⟼{E}\right)\to {f}\left({t}\right)=\left({r}\in {T}⟼{E}\right)\left({t}\right)$
107 83 fveq1i ${⊢}\left({r}\in {T}⟼{E}\right)\left({t}\right)=\left({t}\in {T}⟼{E}\right)\left({t}\right)$
108 106 107 syl6eq ${⊢}{f}=\left({r}\in {T}⟼{E}\right)\to {f}\left({t}\right)=\left({t}\in {T}⟼{E}\right)\left({t}\right)$
109 108 oveq1d ${⊢}{f}=\left({r}\in {T}⟼{E}\right)\to {f}\left({t}\right){g}\left({t}\right)=\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)$
110 109 mpteq2dv ${⊢}{f}=\left({r}\in {T}⟼{E}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)=\left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)$
111 110 eleq1d ${⊢}{f}=\left({r}\in {T}⟼{E}\right)\to \left(\left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)\in {A}\right)$
112 111 imbi2d ${⊢}{f}=\left({r}\in {T}⟼{E}\right)\to \left(\left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}\right)↔\left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)\in {A}\right)\right)$
113 5 3com12 ${⊢}\left({f}\in {A}\wedge {\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
114 113 3expib ${⊢}{f}\in {A}\to \left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}\right)$
115 112 114 vtoclga ${⊢}\left({r}\in {T}⟼{E}\right)\in {A}\to \left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)\in {A}\right)$
116 105 115 sylbir ${⊢}\left({t}\in {T}⟼{E}\right)\in {A}\to \left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)\in {A}\right)$
117 116 3impib ${⊢}\left(\left({t}\in {T}⟼{E}\right)\in {A}\wedge {\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)\in {A}$
118 117 3com13 ${⊢}\left({g}\in {A}\wedge {\phi }\wedge \left({t}\in {T}⟼{E}\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)\in {A}$
119 118 3expib ${⊢}{g}\in {A}\to \left(\left({\phi }\wedge \left({t}\in {T}⟼{E}\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){g}\left({t}\right)\right)\in {A}\right)$
120 104 119 vtoclga ${⊢}{X}\left({m}+1\right)\in {A}\to \left(\left({\phi }\wedge \left({t}\in {T}⟼{E}\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)\right)\in {A}\right)$
121 120 3impib ${⊢}\left({X}\left({m}+1\right)\in {A}\wedge {\phi }\wedge \left({t}\in {T}⟼{E}\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)\right)\in {A}$
122 90 91 99 121 syl3anc ${⊢}\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼{E}\right)\left({t}\right){X}\left({m}+1\right)\left({t}\right)\right)\in {A}$
123 89 122 eqeltrrd ${⊢}\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\in {A}$
124 123 ad2antll ${⊢}\left(\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\wedge \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\right)\to \left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\in {A}$
125 simprrl ${⊢}\left(\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\wedge \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\right)\to {\phi }$
126 simpl ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {m}\in {ℕ}_{0}$
127 simprl ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {\phi }$
128 2 ad2antrl ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {N}\in ℕ$
129 128 nnnn0d ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {N}\in {ℕ}_{0}$
130 nn0re ${⊢}{m}\in {ℕ}_{0}\to {m}\in ℝ$
131 130 adantr ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {m}\in ℝ$
132 peano2nn0 ${⊢}{m}\in {ℕ}_{0}\to {m}+1\in {ℕ}_{0}$
133 132 nn0red ${⊢}{m}\in {ℕ}_{0}\to {m}+1\in ℝ$
134 133 adantr ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {m}+1\in ℝ$
135 2 nnred ${⊢}{\phi }\to {N}\in ℝ$
136 135 ad2antrl ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {N}\in ℝ$
137 lep1 ${⊢}{m}\in ℝ\to {m}\le {m}+1$
138 126 130 137 3syl ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {m}\le {m}+1$
139 elfzle2 ${⊢}{m}+1\in \left(0\dots {N}\right)\to {m}+1\le {N}$
140 139 ad2antll ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {m}+1\le {N}$
141 131 134 136 138 140 letrd ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {m}\le {N}$
142 elfz2nn0 ${⊢}{m}\in \left(0\dots {N}\right)↔\left({m}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {m}\le {N}\right)$
143 126 129 141 142 syl3anbrc ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to {m}\in \left(0\dots {N}\right)$
144 126 127 143 jca32 ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\right)$
145 144 adantl ${⊢}\left(\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\wedge \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\right)\to \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\right)$
146 pm3.31 ${⊢}\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\to \left(\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)$
147 146 adantr ${⊢}\left(\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\wedge \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\right)\to \left(\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)$
148 145 147 mpd ${⊢}\left(\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\wedge \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}$
149 fveq2 ${⊢}{r}={t}\to {X}\left({m}+1\right)\left({r}\right)={X}\left({m}+1\right)\left({t}\right)$
150 149 oveq2d ${⊢}{r}={t}\to {E}{X}\left({m}+1\right)\left({r}\right)={E}{X}\left({m}+1\right)\left({t}\right)$
151 150 cbvmptv ${⊢}\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)=\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)$
152 151 eleq1i ${⊢}\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\in {A}↔\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\in {A}$
153 fveq1 ${⊢}{g}=\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\to {g}\left({t}\right)=\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\left({t}\right)$
154 151 fveq1i ${⊢}\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\left({t}\right)=\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)$
155 153 154 syl6eq ${⊢}{g}=\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\to {g}\left({t}\right)=\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)$
156 155 oveq2d ${⊢}{g}=\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)$
157 156 mpteq2dv ${⊢}{g}=\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)=\left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)$
158 157 eleq1d ${⊢}{g}=\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\to \left(\left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)\in {A}\right)$
159 158 imbi2d ${⊢}{g}=\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\to \left(\left(\left({\phi }\wedge \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)\in {A}\right)↔\left(\left({\phi }\wedge \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)\in {A}\right)\right)$
160 fveq2 ${⊢}{r}={t}\to {X}\left({i}\right)\left({r}\right)={X}\left({i}\right)\left({t}\right)$
161 160 oveq2d ${⊢}{r}={t}\to {E}{X}\left({i}\right)\left({r}\right)={E}{X}\left({i}\right)\left({t}\right)$
162 161 sumeq2sdv ${⊢}{r}={t}\to \sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)=\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)$
163 162 cbvmptv ${⊢}\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)$
164 163 eleq1i ${⊢}\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\in {A}↔\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}$
165 fveq1 ${⊢}{f}=\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\to {f}\left({t}\right)=\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\left({t}\right)$
166 163 fveq1i ${⊢}\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\left({t}\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)$
167 165 166 syl6eq ${⊢}{f}=\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\to {f}\left({t}\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)$
168 167 oveq1d ${⊢}{f}=\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\to {f}\left({t}\right)+{g}\left({t}\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)$
169 168 mpteq2dv ${⊢}{f}=\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)=\left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)$
170 169 eleq1d ${⊢}{f}=\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\to \left(\left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)\in {A}\right)$
171 170 imbi2d ${⊢}{f}=\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\to \left(\left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}\right)↔\left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)\in {A}\right)\right)$
172 4 3com12 ${⊢}\left({f}\in {A}\wedge {\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
173 172 3expib ${⊢}{f}\in {A}\to \left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}\right)$
174 171 173 vtoclga ${⊢}\left({r}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({r}\right)\right)\in {A}\to \left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)\in {A}\right)$
175 164 174 sylbir ${⊢}\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\to \left(\left({\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)\in {A}\right)$
176 175 3impib ${⊢}\left(\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\wedge {\phi }\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
177 176 3com13 ${⊢}\left({g}\in {A}\wedge {\phi }\wedge \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
178 177 3expib ${⊢}{g}\in {A}\to \left(\left({\phi }\wedge \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{g}\left({t}\right)\right)\in {A}\right)$
179 159 178 vtoclga ${⊢}\left({r}\in {T}⟼{E}{X}\left({m}+1\right)\left({r}\right)\right)\in {A}\to \left(\left({\phi }\wedge \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)\in {A}\right)$
180 152 179 sylbir ${⊢}\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\in {A}\to \left(\left({\phi }\wedge \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)\in {A}\right)$
181 180 3impib ${⊢}\left(\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\in {A}\wedge {\phi }\wedge \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)\in {A}$
182 124 125 148 181 syl3anc ${⊢}\left(\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\wedge \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\right)\to \left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)\in {A}$
183 3anass ${⊢}\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)↔\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)$
184 183 biimpri ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\to \left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)$
185 184 adantl ${⊢}\left(\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\wedge \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\right)\to \left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)$
186 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{m}\in {ℕ}_{0}$
187 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{m}+1\in \left(0\dots {N}\right)$
188 186 1 187 nf3an ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)$
189 simpr ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to {t}\in {T}$
190 fzfid ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \left(0\dots {m}\right)\in \mathrm{Fin}$
191 7 3ad2ant2 ${⊢}\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to {E}\in ℝ$
192 191 adantr ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to {E}\in ℝ$
193 192 adantr ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}\right)\right)\to {E}\in ℝ$
194 fzelp1 ${⊢}{i}\in \left(0\dots {m}\right)\to {i}\in \left(0\dots {m}+1\right)$
195 194 anim2i ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}\right)\right)\to \left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)$
196 an32 ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)↔\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\wedge {t}\in {T}\right)$
197 195 196 sylib ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}\right)\right)\to \left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\wedge {t}\in {T}\right)$
198 3 3ad2ant2 ${⊢}\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to {X}:\left(0\dots {N}\right)⟶{A}$
199 198 adantr ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\to {X}:\left(0\dots {N}\right)⟶{A}$
200 elfzuz3 ${⊢}{m}+1\in \left(0\dots {N}\right)\to {N}\in {ℤ}_{\ge \left({m}+1\right)}$
201 fzss2 ${⊢}{N}\in {ℤ}_{\ge \left({m}+1\right)}\to \left(0\dots {m}+1\right)\subseteq \left(0\dots {N}\right)$
202 200 201 syl ${⊢}{m}+1\in \left(0\dots {N}\right)\to \left(0\dots {m}+1\right)\subseteq \left(0\dots {N}\right)$
203 202 sselda ${⊢}\left({m}+1\in \left(0\dots {N}\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\to {i}\in \left(0\dots {N}\right)$
204 203 3ad2antl3 ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\to {i}\in \left(0\dots {N}\right)$
205 199 204 ffvelrnd ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\to {X}\left({i}\right)\in {A}$
206 simpl2 ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\to {\phi }$
207 feq1 ${⊢}{f}={X}\left({i}\right)\to \left({f}:{T}⟶ℝ↔{X}\left({i}\right):{T}⟶ℝ\right)$
208 207 imbi2d ${⊢}{f}={X}\left({i}\right)\to \left(\left({\phi }\to {f}:{T}⟶ℝ\right)↔\left({\phi }\to {X}\left({i}\right):{T}⟶ℝ\right)\right)$
209 208 66 vtoclga ${⊢}{X}\left({i}\right)\in {A}\to \left({\phi }\to {X}\left({i}\right):{T}⟶ℝ\right)$
210 205 206 209 sylc ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\to {X}\left({i}\right):{T}⟶ℝ$
211 210 ffvelrnda ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\wedge {t}\in {T}\right)\to {X}\left({i}\right)\left({t}\right)\in ℝ$
212 197 211 syl ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}\right)\right)\to {X}\left({i}\right)\left({t}\right)\in ℝ$
213 193 212 remulcld ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}\right)\right)\to {E}{X}\left({i}\right)\left({t}\right)\in ℝ$
214 190 213 fsumrecl ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\in ℝ$
215 eqid ${⊢}\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)$
216 215 fvmpt2 ${⊢}\left({t}\in {T}\wedge \sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\in ℝ\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)=\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)$
217 189 214 216 syl2anc ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)=\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)$
218 217 oveq1d ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{E}{X}\left({m}+1\right)\left({t}\right)=\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)+{E}{X}\left({m}+1\right)\left({t}\right)$
219 3simpc ${⊢}\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)$
220 219 adantr ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)$
221 feq1 ${⊢}{f}={X}\left({m}+1\right)\to \left({f}:{T}⟶ℝ↔{X}\left({m}+1\right):{T}⟶ℝ\right)$
222 221 imbi2d ${⊢}{f}={X}\left({m}+1\right)\to \left(\left({\phi }\to {f}:{T}⟶ℝ\right)↔\left({\phi }\to {X}\left({m}+1\right):{T}⟶ℝ\right)\right)$
223 222 66 vtoclga ${⊢}{X}\left({m}+1\right)\in {A}\to \left({\phi }\to {X}\left({m}+1\right):{T}⟶ℝ\right)$
224 90 91 223 sylc ${⊢}\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to {X}\left({m}+1\right):{T}⟶ℝ$
225 220 224 syl ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to {X}\left({m}+1\right):{T}⟶ℝ$
226 225 189 ffvelrnd ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to {X}\left({m}+1\right)\left({t}\right)\in ℝ$
227 192 226 remulcld ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to {E}{X}\left({m}+1\right)\left({t}\right)\in ℝ$
228 eqid ${⊢}\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)=\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)$
229 228 fvmpt2 ${⊢}\left({t}\in {T}\wedge {E}{X}\left({m}+1\right)\left({t}\right)\in ℝ\right)\to \left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)={E}{X}\left({m}+1\right)\left({t}\right)$
230 189 227 229 syl2anc ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)={E}{X}\left({m}+1\right)\left({t}\right)$
231 230 oveq2d ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+{E}{X}\left({m}+1\right)\left({t}\right)$
232 elfzuz ${⊢}{m}+1\in \left(0\dots {N}\right)\to {m}+1\in {ℤ}_{\ge 0}$
233 232 3ad2ant3 ${⊢}\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to {m}+1\in {ℤ}_{\ge 0}$
234 233 adantr ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to {m}+1\in {ℤ}_{\ge 0}$
235 192 adantr ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\to {E}\in ℝ$
236 211 an32s ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\to {X}\left({i}\right)\left({t}\right)\in ℝ$
237 remulcl ${⊢}\left({E}\in ℝ\wedge {X}\left({i}\right)\left({t}\right)\in ℝ\right)\to {E}{X}\left({i}\right)\left({t}\right)\in ℝ$
238 237 recnd ${⊢}\left({E}\in ℝ\wedge {X}\left({i}\right)\left({t}\right)\in ℝ\right)\to {E}{X}\left({i}\right)\left({t}\right)\in ℂ$
239 235 236 238 syl2anc ${⊢}\left(\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\wedge {i}\in \left(0\dots {m}+1\right)\right)\to {E}{X}\left({i}\right)\left({t}\right)\in ℂ$
240 fveq2 ${⊢}{i}={m}+1\to {X}\left({i}\right)={X}\left({m}+1\right)$
241 240 fveq1d ${⊢}{i}={m}+1\to {X}\left({i}\right)\left({t}\right)={X}\left({m}+1\right)\left({t}\right)$
242 241 oveq2d ${⊢}{i}={m}+1\to {E}{X}\left({i}\right)\left({t}\right)={E}{X}\left({m}+1\right)\left({t}\right)$
243 234 239 242 fsumm1 ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)=\sum _{{i}=0}^{{m}+1-1}{E}{X}\left({i}\right)\left({t}\right)+{E}{X}\left({m}+1\right)\left({t}\right)$
244 nn0cn ${⊢}{m}\in {ℕ}_{0}\to {m}\in ℂ$
245 244 3ad2ant1 ${⊢}\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to {m}\in ℂ$
246 245 adantr ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to {m}\in ℂ$
247 1cnd ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to 1\in ℂ$
248 246 247 pncand ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to {m}+1-1={m}$
249 248 oveq2d ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \left(0\dots {m}+1-1\right)=\left(0\dots {m}\right)$
250 249 sumeq1d ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \sum _{{i}=0}^{{m}+1-1}{E}{X}\left({i}\right)\left({t}\right)=\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)$
251 250 oveq1d ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \sum _{{i}=0}^{{m}+1-1}{E}{X}\left({i}\right)\left({t}\right)+{E}{X}\left({m}+1\right)\left({t}\right)=\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)+{E}{X}\left({m}+1\right)\left({t}\right)$
252 243 251 eqtrd ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)=\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)+{E}{X}\left({m}+1\right)\left({t}\right)$
253 218 231 252 3eqtr4rd ${⊢}\left(\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\wedge {t}\in {T}\right)\to \sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)=\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)$
254 188 253 mpteq2da ${⊢}\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)\right)=\left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)$
255 254 eleq1d ${⊢}\left({m}\in {ℕ}_{0}\wedge {\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left(\left({t}\in {T}⟼\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)\in {A}\right)$
256 185 255 syl ${⊢}\left(\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\wedge \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\right)\to \left(\left({t}\in {T}⟼\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}↔\left({t}\in {T}⟼\left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\left({t}\right)+\left({t}\in {T}⟼{E}{X}\left({m}+1\right)\left({t}\right)\right)\left({t}\right)\right)\in {A}\right)$
257 182 256 mpbird ${⊢}\left(\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\wedge \left({m}\in {ℕ}_{0}\wedge \left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}$
258 257 exp32 ${⊢}\left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)\to \left({m}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)$
259 258 pm2.86i ${⊢}{m}\in {ℕ}_{0}\to \left(\left(\left({\phi }\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\to \left(\left({\phi }\wedge {m}+1\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{m}+1}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)\right)$
260 21 28 35 42 81 259 nn0ind ${⊢}{N}\in {ℕ}_{0}\to \left(\left({\phi }\wedge {N}\in \left(0\dots {N}\right)\right)\to \left({t}\in {T}⟼\sum _{{i}=0}^{{N}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}\right)$
261 9 14 260 sylc ${⊢}{\phi }\to \left({t}\in {T}⟼\sum _{{i}=0}^{{N}}{E}{X}\left({i}\right)\left({t}\right)\right)\in {A}$