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	ffvelcdmd	$⊢ φ \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	ffvelcdmda	$⊢ (φ \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	ffvelcdmda	$⊢ (φ \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	bilanri	$⊢ ((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))$
185		nfv	$⊢ Ⅎ t m \in ℕ_{0}$
186		nfv	$⊢ Ⅎ t m + 1 \in (0 \dots N)$
187	185 1 186	nf3an	$⊢ Ⅎ t (m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N))$
188		simpr	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to t \in T$
189		fzfid	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to (0 \dots m) \in Fin$
190	7	3ad2ant2	$⊢ (m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \to E \in ℝ$
191	190	adantr	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to E \in ℝ$
192	191	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 ℝ$
193		fzelp1	$⊢ i \in (0 \dots m) \to i \in (0 \dots m + 1)$
194	193	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))$
195		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)$
196	194 195	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)$
197	3	3ad2ant2	$⊢ (m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \to X : (0 \dots N) ⟶ A$
198	197	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$
199		elfzuz3	$⊢ m + 1 \in (0 \dots N) \to N \in ℤ_{\geq (m + 1)}$
200		fzss2	$⊢ N \in ℤ_{\geq (m + 1)} \to (0 \dots m + 1) \subseteq (0 \dots N)$
201	199 200	syl	$⊢ m + 1 \in (0 \dots N) \to (0 \dots m + 1) \subseteq (0 \dots N)$
202	201	sselda	$⊢ (m + 1 \in (0 \dots N) \land i \in (0 \dots m + 1)) \to i \in (0 \dots N)$
203	202	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)$
204	198 203	ffvelcdmd	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land i \in (0 \dots m + 1)) \to X (i) \in A$
205		simpl2	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land i \in (0 \dots m + 1)) \to φ$
206		feq1	$⊢ f = X (i) \to (f : T ⟶ ℝ \leftrightarrow X (i) : T ⟶ ℝ)$
207	206	imbi2d	$⊢ f = X (i) \to ((φ \to f : T ⟶ ℝ) \leftrightarrow (φ \to X (i) : T ⟶ ℝ))$
208	207 66	vtoclga	$⊢ X (i) \in A \to (φ \to X (i) : T ⟶ ℝ)$
209	204 205 208	sylc	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land i \in (0 \dots m + 1)) \to X (i) : T ⟶ ℝ$
210	209	ffvelcdmda	$⊢ (((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 ℝ$
211	196 210	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 ℝ$
212	192 211	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 ℝ$
213	189 212	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 ℝ$
214		eqid	$⊢ (t \in T ⟼ \sum_{i = 0}^{m} E X (i) (t)) = (t \in T ⟼ \sum_{i = 0}^{m} E X (i) (t))$
215	214	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)$
216	188 213 215	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)$
217	216	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)$
218		3simpc	$⊢ (m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \to (φ \land m + 1 \in (0 \dots N))$
219	218	adantr	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to (φ \land m + 1 \in (0 \dots N))$
220		feq1	$⊢ f = X (m + 1) \to (f : T ⟶ ℝ \leftrightarrow X (m + 1) : T ⟶ ℝ)$
221	220	imbi2d	$⊢ f = X (m + 1) \to ((φ \to f : T ⟶ ℝ) \leftrightarrow (φ \to X (m + 1) : T ⟶ ℝ))$
222	221 66	vtoclga	$⊢ X (m + 1) \in A \to (φ \to X (m + 1) : T ⟶ ℝ)$
223	90 91 222	sylc	$⊢ (φ \land m + 1 \in (0 \dots N)) \to X (m + 1) : T ⟶ ℝ$
224	219 223	syl	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to X (m + 1) : T ⟶ ℝ$
225	224 188	ffvelcdmd	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to X (m + 1) (t) \in ℝ$
226	191 225	remulcld	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to E X (m + 1) (t) \in ℝ$
227		eqid	$⊢ (t \in T ⟼ E X (m + 1) (t)) = (t \in T ⟼ E X (m + 1) (t))$
228	227	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)$
229	188 226 228	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)$
230	229	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)$
231		elfzuz	$⊢ m + 1 \in (0 \dots N) \to m + 1 \in ℤ_{\geq 0}$
232	231	3ad2ant3	$⊢ (m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \to m + 1 \in ℤ_{\geq 0}$
233	232	adantr	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to m + 1 \in ℤ_{\geq 0}$
234	191	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 ℝ$
235	210	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 ℝ$
236		remulcl	$⊢ (E \in ℝ \land X (i) (t) \in ℝ) \to E X (i) (t) \in ℝ$
237	236	recnd	$⊢ (E \in ℝ \land X (i) (t) \in ℝ) \to E X (i) (t) \in ℂ$
238	234 235 237	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 ℂ$
239		fveq2	$⊢ i = m + 1 \to X (i) = X (m + 1)$
240	239	fveq1d	$⊢ i = m + 1 \to X (i) (t) = X (m + 1) (t)$
241	240	oveq2d	$⊢ i = m + 1 \to E X (i) (t) = E X (m + 1) (t)$
242	233 238 241	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)$
243		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
244	243	3ad2ant1	$⊢ (m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \to m \in ℂ$
245	244	adantr	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to m \in ℂ$
246		1cnd	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to 1 \in ℂ$
247	245 246	pncand	$⊢ ((m \in ℕ_{0} \land φ \land m + 1 \in (0 \dots N)) \land t \in T) \to m + 1 - 1 = m$
248	247	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)$
249	248	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)$
250	249	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)$
251	242 250	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)$
252	217 230 251	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)$
253	187 252	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))$
254	253	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)$
255	184 254	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)$
256	182 255	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$
257	256	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))$
258	257	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))$
259	21 28 35 42 81 258	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)$
260	9 14 259	sylc	$⊢ φ \to (t \in T ⟼ \sum_{i = 0}^{N} E X (i) (t)) \in A$

Metamath Proof Explorer

Theorem stoweidlem17

Proof