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 φ$
	stoweidlem17.2	$⊢ φ \to N \in ℕ$
	stoweidlem17.3	$⊢ φ \to X : (0 \dots N) ⟶ A$
	stoweidlem17.4	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem17.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem17.6	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem17.7	$⊢ φ \to E \in ℝ$
	stoweidlem17.8	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
Assertion	stoweidlem17	$⊢ φ \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) \in A$

Proof

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

Metamath Proof Explorer

Theorem stoweidlem17

Proof