dvnmul

Description: Function-builder for the N -th derivative, product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dvnmul.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvnmul.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	dvnmul.a	$⊢ (φ \land x \in X) \to A \in ℂ$
	dvnmul.cc	$⊢ (φ \land x \in X) \to B \in ℂ$
	dvnmul.n	$⊢ φ \to N \in ℕ_{0}$
	dvnmulf	$⊢ F = (x \in X ⟼ A)$
	dvnmul.f	$⊢ G = (x \in X ⟼ B)$
	dvnmul.dvnf	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) : X ⟶ ℂ$
	dvnmul.dvng	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} G) (k) : X ⟶ ℂ$
	dvnmul.c	$⊢ C = (k \in (0 \dots N) ⟼ (S D^{n} F) (k))$
	dvnmul.d	$⊢ D = (k \in (0 \dots N) ⟼ (S D^{n} G) (k))$
Assertion	dvnmul	$⊢ φ \to (S D^{n} (x \in X ⟼ A B)) (N) = (x \in X ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x))$

Proof

Step	Hyp	Ref	Expression
1		dvnmul.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvnmul.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		dvnmul.a	$⊢ (φ \land x \in X) \to A \in ℂ$
4		dvnmul.cc	$⊢ (φ \land x \in X) \to B \in ℂ$
5		dvnmul.n	$⊢ φ \to N \in ℕ_{0}$
6		dvnmulf	$⊢ F = (x \in X ⟼ A)$
7		dvnmul.f	$⊢ G = (x \in X ⟼ B)$
8		dvnmul.dvnf	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) : X ⟶ ℂ$
9		dvnmul.dvng	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} G) (k) : X ⟶ ℂ$
10		dvnmul.c	$⊢ C = (k \in (0 \dots N) ⟼ (S D^{n} F) (k))$
11		dvnmul.d	$⊢ D = (k \in (0 \dots N) ⟼ (S D^{n} G) (k))$
12		id	$⊢ φ \to φ$
13		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
14	5 13	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
15		eluzfz2	$⊢ N \in ℤ_{\geq 0} \to N \in (0 \dots N)$
16	14 15	syl	$⊢ φ \to N \in (0 \dots N)$
17		eleq1	$⊢ n = N \to (n \in (0 \dots N) \leftrightarrow N \in (0 \dots N))$
18		fveq2	$⊢ n = N \to (S D^{n} (x \in X ⟼ A B)) (n) = (S D^{n} (x \in X ⟼ A B)) (N)$
19		oveq2	$⊢ n = N \to (0 \dots n) = (0 \dots N)$
20	19	sumeq1d	$⊢ n = N \to \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x) = \sum_{k = 0}^{N} (\binom{n}{k}) C (k) (x) D (n - k) (x)$
21		oveq1	$⊢ n = N \to (\binom{n}{k}) = (\binom{N}{k})$
22		fvoveq1	$⊢ n = N \to D (n - k) = D (N - k)$
23	22	fveq1d	$⊢ n = N \to D (n - k) (x) = D (N - k) (x)$
24	23	oveq2d	$⊢ n = N \to C (k) (x) D (n - k) (x) = C (k) (x) D (N - k) (x)$
25	21 24	oveq12d	$⊢ n = N \to (\binom{n}{k}) C (k) (x) D (n - k) (x) = (\binom{N}{k}) C (k) (x) D (N - k) (x)$
26	25	sumeq2sdv	$⊢ n = N \to \sum_{k = 0}^{N} (\binom{n}{k}) C (k) (x) D (n - k) (x) = \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x)$
27	20 26	eqtrd	$⊢ n = N \to \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x) = \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x)$
28	27	mpteq2dv	$⊢ n = N \to (x \in X ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x)) = (x \in X ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x))$
29	18 28	eqeq12d	$⊢ n = N \to ((S D^{n} (x \in X ⟼ A B)) (n) = (x \in X ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x)) \leftrightarrow (S D^{n} (x \in X ⟼ A B)) (N) = (x \in X ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x)))$
30	29	imbi2d	$⊢ n = N \to ((φ \to (S D^{n} (x \in X ⟼ A B)) (n) = (x \in X ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x))) \leftrightarrow (φ \to (S D^{n} (x \in X ⟼ A B)) (N) = (x \in X ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x))))$
31	17 30	imbi12d	$⊢ n = N \to ((n \in (0 \dots N) \to (φ \to (S D^{n} (x \in X ⟼ A B)) (n) = (x \in X ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x)))) \leftrightarrow (N \in (0 \dots N) \to (φ \to (S D^{n} (x \in X ⟼ A B)) (N) = (x \in X ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x)))))$
32		fveq2	$⊢ m = 0 \to (S D^{n} (x \in X ⟼ A B)) (m) = (S D^{n} (x \in X ⟼ A B)) (0)$
33		simpl	$⊢ (m = 0 \land x \in X) \to m = 0$
34	33	oveq2d	$⊢ (m = 0 \land x \in X) \to (0 \dots m) = (0 \dots 0)$
35		simpll	$⊢ ((m = 0 \land x \in X) \land k \in (0 \dots 0)) \to m = 0$
36	35	oveq1d	$⊢ ((m = 0 \land x \in X) \land k \in (0 \dots 0)) \to (\binom{m}{k}) = (\binom{0}{k})$
37	35	fvoveq1d	$⊢ ((m = 0 \land x \in X) \land k \in (0 \dots 0)) \to D (m - k) = D (0 - k)$
38	37	fveq1d	$⊢ ((m = 0 \land x \in X) \land k \in (0 \dots 0)) \to D (m - k) (x) = D (0 - k) (x)$
39	38	oveq2d	$⊢ ((m = 0 \land x \in X) \land k \in (0 \dots 0)) \to C (k) (x) D (m - k) (x) = C (k) (x) D (0 - k) (x)$
40	36 39	oveq12d	$⊢ ((m = 0 \land x \in X) \land k \in (0 \dots 0)) \to (\binom{m}{k}) C (k) (x) D (m - k) (x) = (\binom{0}{k}) C (k) (x) D (0 - k) (x)$
41	34 40	sumeq12rdv	$⊢ (m = 0 \land x \in X) \to \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x) = \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x)$
42	41	mpteq2dva	$⊢ m = 0 \to (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x)) = (x \in X ⟼ \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x))$
43	32 42	eqeq12d	$⊢ m = 0 \to ((S D^{n} (x \in X ⟼ A B)) (m) = (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x)) \leftrightarrow (S D^{n} (x \in X ⟼ A B)) (0) = (x \in X ⟼ \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x)))$
44	43	imbi2d	$⊢ m = 0 \to ((φ \to (S D^{n} (x \in X ⟼ A B)) (m) = (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x))) \leftrightarrow (φ \to (S D^{n} (x \in X ⟼ A B)) (0) = (x \in X ⟼ \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x))))$
45		fveq2	$⊢ m = i \to (S D^{n} (x \in X ⟼ A B)) (m) = (S D^{n} (x \in X ⟼ A B)) (i)$
46		simpl	$⊢ (m = i \land x \in X) \to m = i$
47	46	oveq2d	$⊢ (m = i \land x \in X) \to (0 \dots m) = (0 \dots i)$
48		simpll	$⊢ ((m = i \land x \in X) \land k \in (0 \dots i)) \to m = i$
49	48	oveq1d	$⊢ ((m = i \land x \in X) \land k \in (0 \dots i)) \to (\binom{m}{k}) = (\binom{i}{k})$
50	48	fvoveq1d	$⊢ ((m = i \land x \in X) \land k \in (0 \dots i)) \to D (m - k) = D (i - k)$
51	50	fveq1d	$⊢ ((m = i \land x \in X) \land k \in (0 \dots i)) \to D (m - k) (x) = D (i - k) (x)$
52	51	oveq2d	$⊢ ((m = i \land x \in X) \land k \in (0 \dots i)) \to C (k) (x) D (m - k) (x) = C (k) (x) D (i - k) (x)$
53	49 52	oveq12d	$⊢ ((m = i \land x \in X) \land k \in (0 \dots i)) \to (\binom{m}{k}) C (k) (x) D (m - k) (x) = (\binom{i}{k}) C (k) (x) D (i - k) (x)$
54	47 53	sumeq12rdv	$⊢ (m = i \land x \in X) \to \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x) = \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x)$
55	54	mpteq2dva	$⊢ m = i \to (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x)) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))$
56	45 55	eqeq12d	$⊢ m = i \to ((S D^{n} (x \in X ⟼ A B)) (m) = (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x)) \leftrightarrow (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x)))$
57	56	imbi2d	$⊢ m = i \to ((φ \to (S D^{n} (x \in X ⟼ A B)) (m) = (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x))) \leftrightarrow (φ \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))))$
58		fveq2	$⊢ m = i + 1 \to (S D^{n} (x \in X ⟼ A B)) (m) = (S D^{n} (x \in X ⟼ A B)) (i + 1)$
59		simpl	$⊢ (m = i + 1 \land x \in X) \to m = i + 1$
60	59	oveq2d	$⊢ (m = i + 1 \land x \in X) \to (0 \dots m) = (0 \dots i + 1)$
61		simpll	$⊢ ((m = i + 1 \land x \in X) \land k \in (0 \dots i + 1)) \to m = i + 1$
62	61	oveq1d	$⊢ ((m = i + 1 \land x \in X) \land k \in (0 \dots i + 1)) \to (\binom{m}{k}) = (\binom{i + 1}{k})$
63	61	fvoveq1d	$⊢ ((m = i + 1 \land x \in X) \land k \in (0 \dots i + 1)) \to D (m - k) = D (i + 1 - k)$
64	63	fveq1d	$⊢ ((m = i + 1 \land x \in X) \land k \in (0 \dots i + 1)) \to D (m - k) (x) = D (i + 1 - k) (x)$
65	64	oveq2d	$⊢ ((m = i + 1 \land x \in X) \land k \in (0 \dots i + 1)) \to C (k) (x) D (m - k) (x) = C (k) (x) D (i + 1 - k) (x)$
66	62 65	oveq12d	$⊢ ((m = i + 1 \land x \in X) \land k \in (0 \dots i + 1)) \to (\binom{m}{k}) C (k) (x) D (m - k) (x) = (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
67	60 66	sumeq12rdv	$⊢ (m = i + 1 \land x \in X) \to \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x) = \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
68	67	mpteq2dva	$⊢ m = i + 1 \to (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x)) = (x \in X ⟼ \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x))$
69	58 68	eqeq12d	$⊢ m = i + 1 \to ((S D^{n} (x \in X ⟼ A B)) (m) = (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x)) \leftrightarrow (S D^{n} (x \in X ⟼ A B)) (i + 1) = (x \in X ⟼ \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)))$
70	69	imbi2d	$⊢ m = i + 1 \to ((φ \to (S D^{n} (x \in X ⟼ A B)) (m) = (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x))) \leftrightarrow (φ \to (S D^{n} (x \in X ⟼ A B)) (i + 1) = (x \in X ⟼ \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x))))$
71		fveq2	$⊢ m = n \to (S D^{n} (x \in X ⟼ A B)) (m) = (S D^{n} (x \in X ⟼ A B)) (n)$
72		simpl	$⊢ (m = n \land x \in X) \to m = n$
73	72	oveq2d	$⊢ (m = n \land x \in X) \to (0 \dots m) = (0 \dots n)$
74		simpll	$⊢ ((m = n \land x \in X) \land k \in (0 \dots n)) \to m = n$
75	74	oveq1d	$⊢ ((m = n \land x \in X) \land k \in (0 \dots n)) \to (\binom{m}{k}) = (\binom{n}{k})$
76	74	fvoveq1d	$⊢ ((m = n \land x \in X) \land k \in (0 \dots n)) \to D (m - k) = D (n - k)$
77	76	fveq1d	$⊢ ((m = n \land x \in X) \land k \in (0 \dots n)) \to D (m - k) (x) = D (n - k) (x)$
78	77	oveq2d	$⊢ ((m = n \land x \in X) \land k \in (0 \dots n)) \to C (k) (x) D (m - k) (x) = C (k) (x) D (n - k) (x)$
79	75 78	oveq12d	$⊢ ((m = n \land x \in X) \land k \in (0 \dots n)) \to (\binom{m}{k}) C (k) (x) D (m - k) (x) = (\binom{n}{k}) C (k) (x) D (n - k) (x)$
80	73 79	sumeq12rdv	$⊢ (m = n \land x \in X) \to \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x) = \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x)$
81	80	mpteq2dva	$⊢ m = n \to (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x)) = (x \in X ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x))$
82	71 81	eqeq12d	$⊢ m = n \to ((S D^{n} (x \in X ⟼ A B)) (m) = (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x)) \leftrightarrow (S D^{n} (x \in X ⟼ A B)) (n) = (x \in X ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x)))$
83	82	imbi2d	$⊢ m = n \to ((φ \to (S D^{n} (x \in X ⟼ A B)) (m) = (x \in X ⟼ \sum_{k = 0}^{m} (\binom{m}{k}) C (k) (x) D (m - k) (x))) \leftrightarrow (φ \to (S D^{n} (x \in X ⟼ A B)) (n) = (x \in X ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x))))$
84		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
85	1 84	syl	$⊢ φ \to S \subseteq ℂ$
86	3 4	mulcld	$⊢ (φ \land x \in X) \to A B \in ℂ$
87		restsspw	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \subseteq 𝒫 S$
88	87 2	sselid	$⊢ φ \to X \in 𝒫 S$
89		elpwi	$⊢ X \in 𝒫 S \to X \subseteq S$
90	88 89	syl	$⊢ φ \to X \subseteq S$
91		cnex	$⊢ ℂ \in V$
92	91	a1i	$⊢ φ \to ℂ \in V$
93	86 90 92 1	mptelpm	$⊢ φ \to (x \in X ⟼ A B) \in (ℂ ↑_{𝑝𝑚} S)$
94		dvn0	$⊢ (S \subseteq ℂ \land (x \in X ⟼ A B) \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} (x \in X ⟼ A B)) (0) = (x \in X ⟼ A B)$
95	85 93 94	syl2anc	$⊢ φ \to (S D^{n} (x \in X ⟼ A B)) (0) = (x \in X ⟼ A B)$
96		0z	$⊢ 0 \in ℤ$
97		fzsn	$⊢ 0 \in ℤ \to (0 \dots 0) = \{0\}$
98	96 97	ax-mp	$⊢ (0 \dots 0) = \{0\}$
99	98	sumeq1i	$⊢ \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x) = \sum_{k \in \{0\}} (\binom{0}{k}) C (k) (x) D (0 - k) (x)$
100	99	a1i	$⊢ (φ \land x \in X) \to \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x) = \sum_{k \in \{0\}} (\binom{0}{k}) C (k) (x) D (0 - k) (x)$
101		nfcvd	$⊢ (φ \land x \in X) \to \underline{Ⅎ} k A B$
102		nfv	$⊢ Ⅎ k (φ \land x \in X)$
103		oveq2	$⊢ k = 0 \to (\binom{0}{k}) = (\binom{0}{0})$
104		0nn0	$⊢ 0 \in ℕ_{0}$
105		bcn0	$⊢ 0 \in ℕ_{0} \to (\binom{0}{0}) = 1$
106	104 105	ax-mp	$⊢ (\binom{0}{0}) = 1$
107	106	a1i	$⊢ k = 0 \to (\binom{0}{0}) = 1$
108	103 107	eqtrd	$⊢ k = 0 \to (\binom{0}{k}) = 1$
109	108	adantl	$⊢ ((φ \land x \in X) \land k = 0) \to (\binom{0}{k}) = 1$
110		fveq2	$⊢ k = 0 \to C (k) = C (0)$
111	110	adantl	$⊢ (φ \land k = 0) \to C (k) = C (0)$
112		fveq2	$⊢ k = n \to (S D^{n} F) (k) = (S D^{n} F) (n)$
113	112	cbvmptv	$⊢ (k \in (0 \dots N) ⟼ (S D^{n} F) (k)) = (n \in (0 \dots N) ⟼ (S D^{n} F) (n))$
114	10 113	eqtri	$⊢ C = (n \in (0 \dots N) ⟼ (S D^{n} F) (n))$
115		fveq2	$⊢ n = 0 \to (S D^{n} F) (n) = (S D^{n} F) (0)$
116		eluzfz1	$⊢ N \in ℤ_{\geq 0} \to 0 \in (0 \dots N)$
117	14 116	syl	$⊢ φ \to 0 \in (0 \dots N)$
118		fvexd	$⊢ φ \to (S D^{n} F) (0) \in V$
119	114 115 117 118	fvmptd3	$⊢ φ \to C (0) = (S D^{n} F) (0)$
120	119	adantr	$⊢ (φ \land k = 0) \to C (0) = (S D^{n} F) (0)$
121	111 120	eqtrd	$⊢ (φ \land k = 0) \to C (k) = (S D^{n} F) (0)$
122	3 90 92 1	mptelpm	$⊢ φ \to (x \in X ⟼ A) \in (ℂ ↑_{𝑝𝑚} S)$
123	6 122	eqeltrid	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
124		dvn0	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0) = F$
125	85 123 124	syl2anc	$⊢ φ \to (S D^{n} F) (0) = F$
126	125	adantr	$⊢ (φ \land k = 0) \to (S D^{n} F) (0) = F$
127	121 126	eqtrd	$⊢ (φ \land k = 0) \to C (k) = F$
128	127	fveq1d	$⊢ (φ \land k = 0) \to C (k) (x) = F (x)$
129	128	adantlr	$⊢ ((φ \land x \in X) \land k = 0) \to C (k) (x) = F (x)$
130		simpr	$⊢ (φ \land x \in X) \to x \in X$
131	6	fvmpt2	$⊢ (x \in X \land A \in ℂ) \to F (x) = A$
132	130 3 131	syl2anc	$⊢ (φ \land x \in X) \to F (x) = A$
133	132	adantr	$⊢ ((φ \land x \in X) \land k = 0) \to F (x) = A$
134	129 133	eqtrd	$⊢ ((φ \land x \in X) \land k = 0) \to C (k) (x) = A$
135		oveq2	$⊢ k = 0 \to 0 - k = 0 - 0$
136		0m0e0	$⊢ 0 - 0 = 0$
137	136	a1i	$⊢ k = 0 \to 0 - 0 = 0$
138	135 137	eqtrd	$⊢ k = 0 \to 0 - k = 0$
139	138	fveq2d	$⊢ k = 0 \to D (0 - k) = D (0)$
140	139	fveq1d	$⊢ k = 0 \to D (0 - k) (x) = D (0) (x)$
141	140	adantl	$⊢ (φ \land k = 0) \to D (0 - k) (x) = D (0) (x)$
142	141	adantlr	$⊢ ((φ \land x \in X) \land k = 0) \to D (0 - k) (x) = D (0) (x)$
143		fveq2	$⊢ k = n \to (S D^{n} G) (k) = (S D^{n} G) (n)$
144	143	cbvmptv	$⊢ (k \in (0 \dots N) ⟼ (S D^{n} G) (k)) = (n \in (0 \dots N) ⟼ (S D^{n} G) (n))$
145	11 144	eqtri	$⊢ D = (n \in (0 \dots N) ⟼ (S D^{n} G) (n))$
146	145	fveq1i	$⊢ D (0) = (n \in (0 \dots N) ⟼ (S D^{n} G) (n)) (0)$
147	146	a1i	$⊢ φ \to D (0) = (n \in (0 \dots N) ⟼ (S D^{n} G) (n)) (0)$
148		eqidd	$⊢ φ \to (n \in (0 \dots N) ⟼ (S D^{n} G) (n)) = (n \in (0 \dots N) ⟼ (S D^{n} G) (n))$
149		fveq2	$⊢ n = 0 \to (S D^{n} G) (n) = (S D^{n} G) (0)$
150	149	adantl	$⊢ (φ \land n = 0) \to (S D^{n} G) (n) = (S D^{n} G) (0)$
151	4 90 92 1	mptelpm	$⊢ φ \to (x \in X ⟼ B) \in (ℂ ↑_{𝑝𝑚} S)$
152	7 151	eqeltrid	$⊢ φ \to G \in (ℂ ↑_{𝑝𝑚} S)$
153		dvn0	$⊢ (S \subseteq ℂ \land G \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} G) (0) = G$
154	85 152 153	syl2anc	$⊢ φ \to (S D^{n} G) (0) = G$
155	154	adantr	$⊢ (φ \land n = 0) \to (S D^{n} G) (0) = G$
156	150 155	eqtrd	$⊢ (φ \land n = 0) \to (S D^{n} G) (n) = G$
157	7	a1i	$⊢ φ \to G = (x \in X ⟼ B)$
158		mptexg	$⊢ X \in 𝒫 S \to (x \in X ⟼ B) \in V$
159	88 158	syl	$⊢ φ \to (x \in X ⟼ B) \in V$
160	157 159	eqeltrd	$⊢ φ \to G \in V$
161	148 156 117 160	fvmptd	$⊢ φ \to (n \in (0 \dots N) ⟼ (S D^{n} G) (n)) (0) = G$
162	147 161	eqtrd	$⊢ φ \to D (0) = G$
163	162	fveq1d	$⊢ φ \to D (0) (x) = G (x)$
164	163	ad2antrr	$⊢ ((φ \land x \in X) \land k = 0) \to D (0) (x) = G (x)$
165	157 4	fvmpt2d	$⊢ (φ \land x \in X) \to G (x) = B$
166	165	adantr	$⊢ ((φ \land x \in X) \land k = 0) \to G (x) = B$
167	142 164 166	3eqtrd	$⊢ ((φ \land x \in X) \land k = 0) \to D (0 - k) (x) = B$
168	134 167	oveq12d	$⊢ ((φ \land x \in X) \land k = 0) \to C (k) (x) D (0 - k) (x) = A B$
169	109 168	oveq12d	$⊢ ((φ \land x \in X) \land k = 0) \to (\binom{0}{k}) C (k) (x) D (0 - k) (x) = 1 A B$
170	86	mullidd	$⊢ (φ \land x \in X) \to 1 A B = A B$
171	170	adantr	$⊢ ((φ \land x \in X) \land k = 0) \to 1 A B = A B$
172	169 171	eqtrd	$⊢ ((φ \land x \in X) \land k = 0) \to (\binom{0}{k}) C (k) (x) D (0 - k) (x) = A B$
173		0re	$⊢ 0 \in ℝ$
174	173	a1i	$⊢ (φ \land x \in X) \to 0 \in ℝ$
175	101 102 172 174 86	sumsnd	$⊢ (φ \land x \in X) \to \sum_{k \in \{0\}} (\binom{0}{k}) C (k) (x) D (0 - k) (x) = A B$
176	100 175	eqtr2d	$⊢ (φ \land x \in X) \to A B = \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x)$
177	176	mpteq2dva	$⊢ φ \to (x \in X ⟼ A B) = (x \in X ⟼ \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x))$
178	95 177	eqtrd	$⊢ φ \to (S D^{n} (x \in X ⟼ A B)) (0) = (x \in X ⟼ \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x))$
179	178	a1i	$⊢ N \in ℤ_{\geq 0} \to (φ \to (S D^{n} (x \in X ⟼ A B)) (0) = (x \in X ⟼ \sum_{k = 0}^{0} (\binom{0}{k}) C (k) (x) D (0 - k) (x)))$
180		simp3	$⊢ (i \in (0 ..^N) \land (φ \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \land φ) \to φ$
181		simp1	$⊢ (i \in (0 ..^N) \land (φ \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \land φ) \to i \in (0 ..^N)$
182		simp2	$⊢ (i \in (0 ..^N) \land (φ \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \land φ) \to (φ \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x)))$
183		pm3.35	$⊢ (φ \land (φ \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x)))) \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))$
184	180 182 183	syl2anc	$⊢ (i \in (0 ..^N) \land (φ \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \land φ) \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))$
185	85	adantr	$⊢ (φ \land i \in (0 ..^N)) \to S \subseteq ℂ$
186	93	adantr	$⊢ (φ \land i \in (0 ..^N)) \to (x \in X ⟼ A B) \in (ℂ ↑_{𝑝𝑚} S)$
187		elfzonn0	$⊢ i \in (0 ..^N) \to i \in ℕ_{0}$
188	187	adantl	$⊢ (φ \land i \in (0 ..^N)) \to i \in ℕ_{0}$
189		dvnp1	$⊢ (S \subseteq ℂ \land (x \in X ⟼ A B) \in (ℂ ↑_{𝑝𝑚} S) \land i \in ℕ_{0}) \to (S D^{n} (x \in X ⟼ A B)) (i + 1) = S D (S D^{n} (x \in X ⟼ A B)) (i)$
190	185 186 188 189	syl3anc	$⊢ (φ \land i \in (0 ..^N)) \to (S D^{n} (x \in X ⟼ A B)) (i + 1) = S D (S D^{n} (x \in X ⟼ A B)) (i)$
191	190	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \to (S D^{n} (x \in X ⟼ A B)) (i + 1) = S D (S D^{n} (x \in X ⟼ A B)) (i)$
192		simpr	$⊢ ((φ \land i \in (0 ..^N)) \land (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))$
193	192	oveq2d	$⊢ ((φ \land i \in (0 ..^N)) \land (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \to S D (S D^{n} (x \in X ⟼ A B)) (i) = \frac{d (x \in X⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))}{d_{S} x}$
194		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
195		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
196	1	adantr	$⊢ (φ \land i \in (0 ..^N)) \to S \in \{ℝ, ℂ\}$
197	2	adantr	$⊢ (φ \land i \in (0 ..^N)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
198		fzfid	$⊢ (φ \land i \in (0 ..^N)) \to (0 \dots i) \in Fin$
199	187	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i \in ℕ_{0}$
200		elfzelz	$⊢ k \in (0 \dots i) \to k \in ℤ$
201	200	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \in ℤ$
202	199 201	bccld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (\binom{i}{k}) \in ℕ_{0}$
203	202	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (\binom{i}{k}) \in ℂ$
204	203	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (\binom{i}{k}) \in ℂ$
205	204	3adant3	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to (\binom{i}{k}) \in ℂ$
206		simpll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to φ$
207		0zd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \in ℤ$
208		elfzoel2	$⊢ i \in (0 ..^N) \to N \in ℤ$
209	208	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N \in ℤ$
210		elfzle1	$⊢ k \in (0 \dots i) \to 0 \leq k$
211	210	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \leq k$
212	201	zred	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \in ℝ$
213	208	zred	$⊢ i \in (0 ..^N) \to N \in ℝ$
214	213	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N \in ℝ$
215	187	nn0red	$⊢ i \in (0 ..^N) \to i \in ℝ$
216	215	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i \in ℝ$
217		elfzle2	$⊢ k \in (0 \dots i) \to k \leq i$
218	217	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \leq i$
219		elfzolt2	$⊢ i \in (0 ..^N) \to i < N$
220	219	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i < N$
221	212 216 214 218 220	lelttrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k < N$
222	212 214 221	ltled	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \leq N$
223	207 209 201 211 222	elfzd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \in (0 \dots N)$
224	223	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to k \in (0 \dots N)$
225	10	a1i	$⊢ φ \to C = (k \in (0 \dots N) ⟼ (S D^{n} F) (k))$
226		fvexd	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) \in V$
227	225 226	fvmpt2d	$⊢ (φ \land k \in (0 \dots N)) \to C (k) = (S D^{n} F) (k)$
228	227	feq1d	$⊢ (φ \land k \in (0 \dots N)) \to (C (k) : X ⟶ ℂ \leftrightarrow (S D^{n} F) (k) : X ⟶ ℂ)$
229	8 228	mpbird	$⊢ (φ \land k \in (0 \dots N)) \to C (k) : X ⟶ ℂ$
230	206 224 229	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k) : X ⟶ ℂ$
231	230	3adant3	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to C (k) : X ⟶ ℂ$
232		simp3	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to x \in X$
233	231 232	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to C (k) (x) \in ℂ$
234	187	nn0zd	$⊢ i \in (0 ..^N) \to i \in ℤ$
235	234	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i \in ℤ$
236	235 201	zsubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k \in ℤ$
237		elfzel2	$⊢ k \in (0 \dots i) \to i \in ℤ$
238	237	zred	$⊢ k \in (0 \dots i) \to i \in ℝ$
239	200	zred	$⊢ k \in (0 \dots i) \to k \in ℝ$
240	238 239	subge0d	$⊢ k \in (0 \dots i) \to (0 \leq i - k \leftrightarrow k \leq i)$
241	217 240	mpbird	$⊢ k \in (0 \dots i) \to 0 \leq i - k$
242	241	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \leq i - k$
243	216 212	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k \in ℝ$
244	214 212	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - k \in ℝ$
245	173	a1i	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \in ℝ$
246	214 245	jca	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (N \in ℝ \land 0 \in ℝ)$
247		resubcl	$⊢ (N \in ℝ \land 0 \in ℝ) \to N - 0 \in ℝ$
248	246 247	syl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - 0 \in ℝ$
249	216 214 212 220	ltsub1dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k < N - k$
250	245 212 214 211	lesub2dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - k \leq N - 0$
251	243 244 248 249 250	ltletrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k < N - 0$
252	213	recnd	$⊢ i \in (0 ..^N) \to N \in ℂ$
253	252	subid1d	$⊢ i \in (0 ..^N) \to N - 0 = N$
254	253	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - 0 = N$
255	251 254	breqtrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k < N$
256	243 214 255	ltled	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k \leq N$
257	207 209 236 242 256	elfzd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k \in (0 \dots N)$
258	257	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to i - k \in (0 \dots N)$
259		ovex	$⊢ i - k \in V$
260		eleq1	$⊢ j = i - k \to (j \in (0 \dots N) \leftrightarrow i - k \in (0 \dots N))$
261	260	anbi2d	$⊢ j = i - k \to ((φ \land j \in (0 \dots N)) \leftrightarrow (φ \land i - k \in (0 \dots N)))$
262		fveq2	$⊢ j = i - k \to (S D^{n} G) (j) = (S D^{n} G) (i - k)$
263	262	feq1d	$⊢ j = i - k \to ((S D^{n} G) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (i - k) : X ⟶ ℂ)$
264	261 263	imbi12d	$⊢ j = i - k \to (((φ \land j \in (0 \dots N)) \to (S D^{n} G) (j) : X ⟶ ℂ) \leftrightarrow ((φ \land i - k \in (0 \dots N)) \to (S D^{n} G) (i - k) : X ⟶ ℂ))$
265		nfv	$⊢ Ⅎ k ((φ \land j \in (0 \dots N)) \to (S D^{n} G) (j) : X ⟶ ℂ)$
266		eleq1	$⊢ k = j \to (k \in (0 \dots N) \leftrightarrow j \in (0 \dots N))$
267	266	anbi2d	$⊢ k = j \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land j \in (0 \dots N)))$
268		fveq2	$⊢ k = j \to (S D^{n} G) (k) = (S D^{n} G) (j)$
269	268	feq1d	$⊢ k = j \to ((S D^{n} G) (k) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (j) : X ⟶ ℂ)$
270	267 269	imbi12d	$⊢ k = j \to (((φ \land k \in (0 \dots N)) \to (S D^{n} G) (k) : X ⟶ ℂ) \leftrightarrow ((φ \land j \in (0 \dots N)) \to (S D^{n} G) (j) : X ⟶ ℂ))$
271	265 270 9	chvarfv	$⊢ (φ \land j \in (0 \dots N)) \to (S D^{n} G) (j) : X ⟶ ℂ$
272	259 264 271	vtocl	$⊢ (φ \land i - k \in (0 \dots N)) \to (S D^{n} G) (i - k) : X ⟶ ℂ$
273	206 258 272	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k) : X ⟶ ℂ$
274		fveq2	$⊢ n = i - k \to (S D^{n} G) (n) = (S D^{n} G) (i - k)$
275		fvexd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k) \in V$
276	145 274 257 275	fvmptd3	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to D (i - k) = (S D^{n} G) (i - k)$
277	276	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i - k) = (S D^{n} G) (i - k)$
278	277	feq1d	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (D (i - k) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (i - k) : X ⟶ ℂ)$
279	273 278	mpbird	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i - k) : X ⟶ ℂ$
280	279	3adant3	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to D (i - k) : X ⟶ ℂ$
281	280 232	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to D (i - k) (x) \in ℂ$
282	233 281	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to C (k) (x) D (i - k) (x) \in ℂ$
283	205 282	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to (\binom{i}{k}) C (k) (x) D (i - k) (x) \in ℂ$
284	205	3expa	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to (\binom{i}{k}) \in ℂ$
285	235	peano2zd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 \in ℤ$
286	285 201	zsubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \in ℤ$
287		peano2re	$⊢ i \in ℝ \to i + 1 \in ℝ$
288	238 287	syl	$⊢ k \in (0 \dots i) \to i + 1 \in ℝ$
289		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
290	239 289	syl	$⊢ k \in (0 \dots i) \to k + 1 \in ℝ$
291	239	ltp1d	$⊢ k \in (0 \dots i) \to k < k + 1$
292		1red	$⊢ k \in (0 \dots i) \to 1 \in ℝ$
293	239 238 292 217	leadd1dd	$⊢ k \in (0 \dots i) \to k + 1 \leq i + 1$
294	239 290 288 291 293	ltletrd	$⊢ k \in (0 \dots i) \to k < i + 1$
295	239 288 294	ltled	$⊢ k \in (0 \dots i) \to k \leq i + 1$
296	295	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \leq i + 1$
297	216 287	syl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 \in ℝ$
298	297 212	subge0d	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (0 \leq i + 1 - k \leftrightarrow k \leq i + 1)$
299	296 298	mpbird	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \leq i + 1 - k$
300	297 212	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \in ℝ$
301		elfzop1le2	$⊢ i \in (0 ..^N) \to i + 1 \leq N$
302	301	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 \leq N$
303	297 214 212 302	lesub1dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \leq N - k$
304	250 254	breqtrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - k \leq N$
305	300 244 214 303 304	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \leq N$
306	207 209 286 299 305	elfzd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \in (0 \dots N)$
307	306	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to i + 1 - k \in (0 \dots N)$
308		ovex	$⊢ i + 1 - k \in V$
309		eleq1	$⊢ j = i + 1 - k \to (j \in (0 \dots N) \leftrightarrow i + 1 - k \in (0 \dots N))$
310	309	anbi2d	$⊢ j = i + 1 - k \to ((φ \land j \in (0 \dots N)) \leftrightarrow (φ \land i + 1 - k \in (0 \dots N)))$
311		fveq2	$⊢ j = i + 1 - k \to (S D^{n} G) (j) = (S D^{n} G) (i + 1 - k)$
312	311	feq1d	$⊢ j = i + 1 - k \to ((S D^{n} G) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (i + 1 - k) : X ⟶ ℂ)$
313	310 312	imbi12d	$⊢ j = i + 1 - k \to (((φ \land j \in (0 \dots N)) \to (S D^{n} G) (j) : X ⟶ ℂ) \leftrightarrow ((φ \land i + 1 - k \in (0 \dots N)) \to (S D^{n} G) (i + 1 - k) : X ⟶ ℂ))$
314	308 313 271	vtocl	$⊢ (φ \land i + 1 - k \in (0 \dots N)) \to (S D^{n} G) (i + 1 - k) : X ⟶ ℂ$
315	206 307 314	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i + 1 - k) : X ⟶ ℂ$
316	145	a1i	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D = (n \in (0 \dots N) ⟼ (S D^{n} G) (n))$
317		simpr	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land n = i + 1 - k) \to n = i + 1 - k$
318	317	fveq2d	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land n = i + 1 - k) \to (S D^{n} G) (n) = (S D^{n} G) (i + 1 - k)$
319		fvexd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i + 1 - k) \in V$
320	316 318 307 319	fvmptd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i + 1 - k) = (S D^{n} G) (i + 1 - k)$
321	320	feq1d	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (D (i + 1 - k) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (i + 1 - k) : X ⟶ ℂ)$
322	315 321	mpbird	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i + 1 - k) : X ⟶ ℂ$
323	322	ffvelcdmda	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to D (i + 1 - k) (x) \in ℂ$
324	233	3expa	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k) (x) \in ℂ$
325	323 324	mulcomd	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to D (i + 1 - k) (x) C (k) (x) = C (k) (x) D (i + 1 - k) (x)$
326	325	oveq2d	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k + 1) (x) D (i - k) (x) + D (i + 1 - k) (x) C (k) (x) = C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)$
327	201	peano2zd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \in ℤ$
328	173	a1i	$⊢ k \in (0 \dots i) \to 0 \in ℝ$
329	328 239 290 210 291	lelttrd	$⊢ k \in (0 \dots i) \to 0 < k + 1$
330	328 290 329	ltled	$⊢ k \in (0 \dots i) \to 0 \leq k + 1$
331	330	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \leq k + 1$
332	212 289	syl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \in ℝ$
333	293	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \leq i + 1$
334	332 297 214 333 302	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \leq N$
335	207 209 327 331 334	elfzd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \in (0 \dots N)$
336	335	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to k + 1 \in (0 \dots N)$
337		ovex	$⊢ k + 1 \in V$
338		eleq1	$⊢ j = k + 1 \to (j \in (0 \dots N) \leftrightarrow k + 1 \in (0 \dots N))$
339	338	anbi2d	$⊢ j = k + 1 \to ((φ \land j \in (0 \dots N)) \leftrightarrow (φ \land k + 1 \in (0 \dots N)))$
340		fveq2	$⊢ j = k + 1 \to C (j) = C (k + 1)$
341	340	feq1d	$⊢ j = k + 1 \to (C (j) : X ⟶ ℂ \leftrightarrow C (k + 1) : X ⟶ ℂ)$
342	339 341	imbi12d	$⊢ j = k + 1 \to (((φ \land j \in (0 \dots N)) \to C (j) : X ⟶ ℂ) \leftrightarrow ((φ \land k + 1 \in (0 \dots N)) \to C (k + 1) : X ⟶ ℂ))$
343		nfv	$⊢ Ⅎ k (φ \land j \in (0 \dots N))$
344		nfmpt1	$⊢ \underline{Ⅎ} k (k \in (0 \dots N) ⟼ (S D^{n} F) (k))$
345	10 344	nfcxfr	$⊢ \underline{Ⅎ} k C$
346		nfcv	$⊢ \underline{Ⅎ} k j$
347	345 346	nffv	$⊢ \underline{Ⅎ} k C (j)$
348		nfcv	$⊢ \underline{Ⅎ} k X$
349		nfcv	$⊢ \underline{Ⅎ} k ℂ$
350	347 348 349	nff	$⊢ Ⅎ k C (j) : X ⟶ ℂ$
351	343 350	nfim	$⊢ Ⅎ k ((φ \land j \in (0 \dots N)) \to C (j) : X ⟶ ℂ)$
352		fveq2	$⊢ k = j \to C (k) = C (j)$
353	352	feq1d	$⊢ k = j \to (C (k) : X ⟶ ℂ \leftrightarrow C (j) : X ⟶ ℂ)$
354	267 353	imbi12d	$⊢ k = j \to (((φ \land k \in (0 \dots N)) \to C (k) : X ⟶ ℂ) \leftrightarrow ((φ \land j \in (0 \dots N)) \to C (j) : X ⟶ ℂ))$
355	351 354 229	chvarfv	$⊢ (φ \land j \in (0 \dots N)) \to C (j) : X ⟶ ℂ$
356	337 342 355	vtocl	$⊢ (φ \land k + 1 \in (0 \dots N)) \to C (k + 1) : X ⟶ ℂ$
357	206 336 356	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k + 1) : X ⟶ ℂ$
358	357	ffvelcdmda	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k + 1) (x) \in ℂ$
359	281	3expa	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to D (i - k) (x) \in ℂ$
360	358 359	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k + 1) (x) D (i - k) (x) \in ℂ$
361	323 324	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to D (i + 1 - k) (x) C (k) (x) \in ℂ$
362	360 361	addcld	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k + 1) (x) D (i - k) (x) + D (i + 1 - k) (x) C (k) (x) \in ℂ$
363	326 362	eqeltrrd	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x) \in ℂ$
364	284 363	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)) \in ℂ$
365	364	3impa	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)) \in ℂ$
366	206 1	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to S \in \{ℝ, ℂ\}$
367	173	a1i	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to 0 \in ℝ$
368	206 2	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
369	366 368 204	dvmptconst	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to \frac{d (x \in X⟼ (\binom{i}{k}))}{d_{S} x} = (x \in X ⟼ 0)$
370	282	3expa	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k) (x) D (i - k) (x) \in ℂ$
371	206 224 227	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k) = (S D^{n} F) (k)$
372	371	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} F) (k) = C (k)$
373	230	feqmptd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k) = (x \in X ⟼ C (k) (x))$
374	372 373	eqtr2d	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (x \in X ⟼ C (k) (x)) = (S D^{n} F) (k)$
375	374	oveq2d	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to \frac{d (x \in X⟼ C (k) (x))}{d_{S} x} = S D (S D^{n} F) (k)$
376	366 84	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to S \subseteq ℂ$
377	206 123	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
378		elfznn0	$⊢ k \in (0 \dots i) \to k \in ℕ_{0}$
379	378	adantl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to k \in ℕ_{0}$
380		dvnp1	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to (S D^{n} F) (k + 1) = S D (S D^{n} F) (k)$
381	376 377 379 380	syl3anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} F) (k + 1) = S D (S D^{n} F) (k)$
382	381	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to S D (S D^{n} F) (k) = (S D^{n} F) (k + 1)$
383		fveq2	$⊢ n = k + 1 \to (S D^{n} F) (n) = (S D^{n} F) (k + 1)$
384		fvexd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} F) (k + 1) \in V$
385	114 383 336 384	fvmptd3	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k + 1) = (S D^{n} F) (k + 1)$
386	385	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} F) (k + 1) = C (k + 1)$
387	357	feqmptd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k + 1) = (x \in X ⟼ C (k + 1) (x))$
388	386 387	eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} F) (k + 1) = (x \in X ⟼ C (k + 1) (x))$
389	375 382 388	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to \frac{d (x \in X⟼ C (k) (x))}{d_{S} x} = (x \in X ⟼ C (k + 1) (x))$
390	277	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k) = D (i - k)$
391	279	feqmptd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i - k) = (x \in X ⟼ D (i - k) (x))$
392	390 391	eqtr2d	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (x \in X ⟼ D (i - k) (x)) = (S D^{n} G) (i - k)$
393	392	oveq2d	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to \frac{d (x \in X⟼ D (i - k) (x))}{d_{S} x} = S D (S D^{n} G) (i - k)$
394	206 152	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to G \in (ℂ ↑_{𝑝𝑚} S)$
395		fznn0sub	$⊢ k \in (0 \dots i) \to i - k \in ℕ_{0}$
396	395	adantl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to i - k \in ℕ_{0}$
397		dvnp1	$⊢ (S \subseteq ℂ \land G \in (ℂ ↑_{𝑝𝑚} S) \land i - k \in ℕ_{0}) \to (S D^{n} G) (i - k + 1) = S D (S D^{n} G) (i - k)$
398	376 394 396 397	syl3anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k + 1) = S D (S D^{n} G) (i - k)$
399	398	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to S D (S D^{n} G) (i - k) = (S D^{n} G) (i - k + 1)$
400	216	recnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i \in ℂ$
401		1cnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 1 \in ℂ$
402	212	recnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \in ℂ$
403	400 401 402	addsubd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k = i - k + 1$
404	403	eqcomd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k + 1 = i + 1 - k$
405	404	fveq2d	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k + 1) = (S D^{n} G) (i + 1 - k)$
406	405	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k + 1) = (S D^{n} G) (i + 1 - k)$
407	320	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i + 1 - k) = D (i + 1 - k)$
408	322	feqmptd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i + 1 - k) = (x \in X ⟼ D (i + 1 - k) (x))$
409	406 407 408	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k + 1) = (x \in X ⟼ D (i + 1 - k) (x))$
410	393 399 409	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to \frac{d (x \in X⟼ D (i - k) (x))}{d_{S} x} = (x \in X ⟼ D (i + 1 - k) (x))$
411	366 324 358 389 359 323 410	dvmptmul	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to \frac{d (x \in X⟼ C (k) (x) D (i - k) (x))}{d_{S} x} = (x \in X ⟼ C (k + 1) (x) D (i - k) (x) + D (i + 1 - k) (x) C (k) (x))$
412	366 284 367 369 370 362 411	dvmptmul	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to \frac{d (x \in X⟼ (\binom{i}{k}) C (k) (x) D (i - k) (x))}{d_{S} x} = (x \in X ⟼ 0 \cdot C (k) (x) D (i - k) (x) + (C (k + 1) (x) D (i - k) (x) + D (i + 1 - k) (x) C (k) (x)) (\binom{i}{k}))$
413	370	mul02d	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to 0 \cdot C (k) (x) D (i - k) (x) = 0$
414	326	oveq1d	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to (C (k + 1) (x) D (i - k) (x) + D (i + 1 - k) (x) C (k) (x)) (\binom{i}{k}) = (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)) (\binom{i}{k})$
415	363 284	mulcomd	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)) (\binom{i}{k}) = (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x))$
416	414 415	eqtrd	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to (C (k + 1) (x) D (i - k) (x) + D (i + 1 - k) (x) C (k) (x)) (\binom{i}{k}) = (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x))$
417	413 416	oveq12d	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to 0 \cdot C (k) (x) D (i - k) (x) + (C (k + 1) (x) D (i - k) (x) + D (i + 1 - k) (x) C (k) (x)) (\binom{i}{k}) = 0 + (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x))$
418	364	addlidd	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to 0 + (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)) = (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x))$
419	417 418	eqtrd	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to 0 \cdot C (k) (x) D (i - k) (x) + (C (k + 1) (x) D (i - k) (x) + D (i + 1 - k) (x) C (k) (x)) (\binom{i}{k}) = (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x))$
420	419	mpteq2dva	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (x \in X ⟼ 0 \cdot C (k) (x) D (i - k) (x) + (C (k + 1) (x) D (i - k) (x) + D (i + 1 - k) (x) C (k) (x)) (\binom{i}{k})) = (x \in X ⟼ (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)))$
421	412 420	eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to \frac{d (x \in X⟼ (\binom{i}{k}) C (k) (x) D (i - k) (x))}{d_{S} x} = (x \in X ⟼ (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)))$
422	194 195 196 197 198 283 365 421	dvmptfsum	$⊢ (φ \land i \in (0 ..^N)) \to \frac{d (x \in X⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))}{d_{S} x} = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)))$
423	204	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i}{k}) \in ℂ$
424	360	an32s	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to C (k + 1) (x) D (i - k) (x) \in ℂ$
425		anass	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \leftrightarrow ((φ \land i \in (0 ..^N)) \land (k \in (0 \dots i) \land x \in X))$
426		ancom	$⊢ (k \in (0 \dots i) \land x \in X) \leftrightarrow (x \in X \land k \in (0 \dots i))$
427	426	anbi2i	$⊢ ((φ \land i \in (0 ..^N)) \land (k \in (0 \dots i) \land x \in X)) \leftrightarrow ((φ \land i \in (0 ..^N)) \land (x \in X \land k \in (0 \dots i)))$
428		anass	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \leftrightarrow ((φ \land i \in (0 ..^N)) \land (x \in X \land k \in (0 \dots i)))$
429	428	bicomi	$⊢ ((φ \land i \in (0 ..^N)) \land (x \in X \land k \in (0 \dots i))) \leftrightarrow (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i))$
430	427 429	bitri	$⊢ ((φ \land i \in (0 ..^N)) \land (k \in (0 \dots i) \land x \in X)) \leftrightarrow (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i))$
431	425 430	bitri	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \leftrightarrow (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i))$
432	431	imbi1i	$⊢ ((((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k) (x) \in ℂ) \leftrightarrow ((((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to C (k) (x) \in ℂ)$
433	324 432	mpbi	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to C (k) (x) \in ℂ$
434	431	imbi1i	$⊢ ((((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to D (i + 1 - k) (x) \in ℂ) \leftrightarrow ((((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to D (i + 1 - k) (x) \in ℂ)$
435	323 434	mpbi	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to D (i + 1 - k) (x) \in ℂ$
436	433 435	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to C (k) (x) D (i + 1 - k) (x) \in ℂ$
437	423 424 436	adddid	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)) = (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) + (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
438	437	sumeq2dv	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)) = \sum_{k = 0}^{i} ((\binom{i}{k}) C (k + 1) (x) D (i - k) (x) + (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x))$
439	198	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (0 \dots i) \in Fin$
440	423 424	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) \in ℂ$
441	423 436	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) \in ℂ$
442	439 440 441	fsumadd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} ((\binom{i}{k}) C (k + 1) (x) D (i - k) (x) + (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)) = \sum_{k = 0}^{i} (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) + \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
443		oveq2	$⊢ k = h \to (\binom{i}{k}) = (\binom{i}{h})$
444		fvoveq1	$⊢ k = h \to C (k + 1) = C (h + 1)$
445	444	fveq1d	$⊢ k = h \to C (k + 1) (x) = C (h + 1) (x)$
446		oveq2	$⊢ k = h \to i - k = i - h$
447	446	fveq2d	$⊢ k = h \to D (i - k) = D (i - h)$
448	447	fveq1d	$⊢ k = h \to D (i - k) (x) = D (i - h) (x)$
449	445 448	oveq12d	$⊢ k = h \to C (k + 1) (x) D (i - k) (x) = C (h + 1) (x) D (i - h) (x)$
450	443 449	oveq12d	$⊢ k = h \to (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) = (\binom{i}{h}) C (h + 1) (x) D (i - h) (x)$
451		nfcv	$⊢ \underline{Ⅎ} h (\binom{i}{k}) C (k + 1) (x) D (i - k) (x)$
452		nfcv	$⊢ \underline{Ⅎ} k (\binom{i}{h})$
453		nfcv	$⊢ \underline{Ⅎ} k \times$
454		nfcv	$⊢ \underline{Ⅎ} k (h + 1)$
455	345 454	nffv	$⊢ \underline{Ⅎ} k C (h + 1)$
456		nfcv	$⊢ \underline{Ⅎ} k x$
457	455 456	nffv	$⊢ \underline{Ⅎ} k C (h + 1) (x)$
458		nfmpt1	$⊢ \underline{Ⅎ} k (k \in (0 \dots N) ⟼ (S D^{n} G) (k))$
459	11 458	nfcxfr	$⊢ \underline{Ⅎ} k D$
460		nfcv	$⊢ \underline{Ⅎ} k (i - h)$
461	459 460	nffv	$⊢ \underline{Ⅎ} k D (i - h)$
462	461 456	nffv	$⊢ \underline{Ⅎ} k D (i - h) (x)$
463	457 453 462	nfov	$⊢ \underline{Ⅎ} k C (h + 1) (x) D (i - h) (x)$
464	452 453 463	nfov	$⊢ \underline{Ⅎ} k (\binom{i}{h}) C (h + 1) (x) D (i - h) (x)$
465	450 451 464	cbvsum	$⊢ \sum_{k = 0}^{i} (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) = \sum_{h = 0}^{i} (\binom{i}{h}) C (h + 1) (x) D (i - h) (x)$
466	465	a1i	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) = \sum_{h = 0}^{i} (\binom{i}{h}) C (h + 1) (x) D (i - h) (x)$
467		1zzd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 1 \in ℤ$
468	96	a1i	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 0 \in ℤ$
469	234	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to i \in ℤ$
470		nfv	$⊢ Ⅎ k ((φ \land i \in (0 ..^N)) \land x \in X)$
471		nfcv	$⊢ \underline{Ⅎ} k h$
472		nfcv	$⊢ \underline{Ⅎ} k (0 \dots i)$
473	471 472	nfel	$⊢ Ⅎ k h \in (0 \dots i)$
474	470 473	nfan	$⊢ Ⅎ k (((φ \land i \in (0 ..^N)) \land x \in X) \land h \in (0 \dots i))$
475	464 349	nfel	$⊢ Ⅎ k (\binom{i}{h}) C (h + 1) (x) D (i - h) (x) \in ℂ$
476	474 475	nfim	$⊢ Ⅎ k ((((φ \land i \in (0 ..^N)) \land x \in X) \land h \in (0 \dots i)) \to (\binom{i}{h}) C (h + 1) (x) D (i - h) (x) \in ℂ)$
477		eleq1	$⊢ k = h \to (k \in (0 \dots i) \leftrightarrow h \in (0 \dots i))$
478	477	anbi2d	$⊢ k = h \to ((((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \leftrightarrow (((φ \land i \in (0 ..^N)) \land x \in X) \land h \in (0 \dots i)))$
479	450	eleq1d	$⊢ k = h \to ((\binom{i}{k}) C (k + 1) (x) D (i - k) (x) \in ℂ \leftrightarrow (\binom{i}{h}) C (h + 1) (x) D (i - h) (x) \in ℂ)$
480	478 479	imbi12d	$⊢ k = h \to (((((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) \in ℂ) \leftrightarrow ((((φ \land i \in (0 ..^N)) \land x \in X) \land h \in (0 \dots i)) \to (\binom{i}{h}) C (h + 1) (x) D (i - h) (x) \in ℂ))$
481	476 480 440	chvarfv	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land h \in (0 \dots i)) \to (\binom{i}{h}) C (h + 1) (x) D (i - h) (x) \in ℂ$
482		oveq2	$⊢ h = j - 1 \to (\binom{i}{h}) = (\binom{i}{j - 1})$
483		fvoveq1	$⊢ h = j - 1 \to C (h + 1) = C (j - 1 + 1)$
484	483	fveq1d	$⊢ h = j - 1 \to C (h + 1) (x) = C (j - 1 + 1) (x)$
485		oveq2	$⊢ h = j - 1 \to i - h = i - (j - 1)$
486	485	fveq2d	$⊢ h = j - 1 \to D (i - h) = D (i - (j - 1))$
487	486	fveq1d	$⊢ h = j - 1 \to D (i - h) (x) = D (i - (j - 1)) (x)$
488	484 487	oveq12d	$⊢ h = j - 1 \to C (h + 1) (x) D (i - h) (x) = C (j - 1 + 1) (x) D (i - (j - 1)) (x)$
489	482 488	oveq12d	$⊢ h = j - 1 \to (\binom{i}{h}) C (h + 1) (x) D (i - h) (x) = (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x)$
490	467 468 469 481 489	fsumshft	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{h = 0}^{i} (\binom{i}{h}) C (h + 1) (x) D (i - h) (x) = \sum_{j = 0 + 1}^{i + 1} (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x)$
491	466 490	eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) = \sum_{j = 0 + 1}^{i + 1} (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x)$
492		0p1e1	$⊢ 0 + 1 = 1$
493	492	oveq1i	$⊢ (0 + 1 \dots i + 1) = (1 \dots i + 1)$
494	493	sumeq1i	$⊢ \sum_{j = 0 + 1}^{i + 1} (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x) = \sum_{j = 1}^{i + 1} (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x)$
495	494	a1i	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{j = 0 + 1}^{i + 1} (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x) = \sum_{j = 1}^{i + 1} (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x)$
496		elfzelz	$⊢ j \in (1 \dots i + 1) \to j \in ℤ$
497	496	zcnd	$⊢ j \in (1 \dots i + 1) \to j \in ℂ$
498		1cnd	$⊢ j \in (1 \dots i + 1) \to 1 \in ℂ$
499	497 498	npcand	$⊢ j \in (1 \dots i + 1) \to j - 1 + 1 = j$
500	499	fveq2d	$⊢ j \in (1 \dots i + 1) \to C (j - 1 + 1) = C (j)$
501	500	fveq1d	$⊢ j \in (1 \dots i + 1) \to C (j - 1 + 1) (x) = C (j) (x)$
502	501	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to C (j - 1 + 1) (x) = C (j) (x)$
503	215	recnd	$⊢ i \in (0 ..^N) \to i \in ℂ$
504	503	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℂ$
505	497	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℂ$
506	498	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 1 \in ℂ$
507	504 505 506	subsub3d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i - (j - 1) = i + 1 - j$
508	507	fveq2d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to D (i - (j - 1)) = D (i + 1 - j)$
509	508	fveq1d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to D (i - (j - 1)) (x) = D (i + 1 - j) (x)$
510	502 509	oveq12d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to C (j - 1 + 1) (x) D (i - (j - 1)) (x) = C (j) (x) D (i + 1 - j) (x)$
511	510	oveq2d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x) = (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
512	511	sumeq2dv	$⊢ i \in (0 ..^N) \to \sum_{j = 1}^{i + 1} (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x) = \sum_{j = 1}^{i + 1} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
513	512	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{j = 1}^{i + 1} (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x) = \sum_{j = 1}^{i + 1} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
514		nfv	$⊢ Ⅎ j ((φ \land i \in (0 ..^N)) \land x \in X)$
515		nfcv	$⊢ \underline{Ⅎ} j (\binom{i}{i + 1 - 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
516		fzfid	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (1 \dots i + 1) \in Fin$
517	187	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℕ_{0}$
518	496	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℤ$
519		1zzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 1 \in ℤ$
520	518 519	zsubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j - 1 \in ℤ$
521	517 520	bccld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℕ_{0}$
522	521	nn0cnd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℂ$
523	522	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℂ$
524	523	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℂ$
525	12	ad2antrr	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to φ$
526		0zd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 0 \in ℤ$
527	208	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to N \in ℤ$
528	173	a1i	$⊢ j \in (1 \dots i + 1) \to 0 \in ℝ$
529	496	zred	$⊢ j \in (1 \dots i + 1) \to j \in ℝ$
530		1red	$⊢ j \in (1 \dots i + 1) \to 1 \in ℝ$
531		0lt1	$⊢ 0 < 1$
532	531	a1i	$⊢ j \in (1 \dots i + 1) \to 0 < 1$
533		elfzle1	$⊢ j \in (1 \dots i + 1) \to 1 \leq j$
534	528 530 529 532 533	ltletrd	$⊢ j \in (1 \dots i + 1) \to 0 < j$
535	528 529 534	ltled	$⊢ j \in (1 \dots i + 1) \to 0 \leq j$
536	535	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 0 \leq j$
537	529	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℝ$
538	215	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℝ$
539		1red	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 1 \in ℝ$
540	538 539	readdcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 \in ℝ$
541	213	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to N \in ℝ$
542		elfzle2	$⊢ j \in (1 \dots i + 1) \to j \leq i + 1$
543	542	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \leq i + 1$
544	301	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 \leq N$
545	537 540 541 543 544	letrd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \leq N$
546	526 527 518 536 545	elfzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in (0 \dots N)$
547	546	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to j \in (0 \dots N)$
548	525 547 355	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to C (j) : X ⟶ ℂ$
549	548	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to C (j) : X ⟶ ℂ$
550		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to x \in X$
551	549 550	ffvelcdmd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to C (j) (x) \in ℂ$
552	234	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℤ$
553	552	peano2zd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 \in ℤ$
554	553 518	zsubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \in ℤ$
555	540 537	subge0d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (0 \leq i + 1 - j \leftrightarrow j \leq i + 1)$
556	543 555	mpbird	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 0 \leq i + 1 - j$
557	540 537	resubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \in ℝ$
558	557	leidd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \leq i + 1 - j$
559	529 534	elrpd	$⊢ j \in (1 \dots i + 1) \to j \in ℝ^{+}$
560	559	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℝ^{+}$
561	540 560	ltsubrpd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j < i + 1$
562	557 540 541 561 544	ltletrd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j < N$
563	557 557 541 558 562	lelttrd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j < N$
564	557 541 563	ltled	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \leq N$
565	526 527 554 556 564	elfzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \in (0 \dots N)$
566	565	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to i + 1 - j \in (0 \dots N)$
567		nfv	$⊢ Ⅎ k (φ \land i + 1 - j \in (0 \dots N))$
568		nfcv	$⊢ \underline{Ⅎ} k (i + 1 - j)$
569	459 568	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - j)$
570	569 348 349	nff	$⊢ Ⅎ k D (i + 1 - j) : X ⟶ ℂ$
571	567 570	nfim	$⊢ Ⅎ k ((φ \land i + 1 - j \in (0 \dots N)) \to D (i + 1 - j) : X ⟶ ℂ)$
572		ovex	$⊢ i + 1 - j \in V$
573		eleq1	$⊢ k = i + 1 - j \to (k \in (0 \dots N) \leftrightarrow i + 1 - j \in (0 \dots N))$
574	573	anbi2d	$⊢ k = i + 1 - j \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land i + 1 - j \in (0 \dots N)))$
575		fveq2	$⊢ k = i + 1 - j \to D (k) = D (i + 1 - j)$
576	575	feq1d	$⊢ k = i + 1 - j \to (D (k) : X ⟶ ℂ \leftrightarrow D (i + 1 - j) : X ⟶ ℂ)$
577	574 576	imbi12d	$⊢ k = i + 1 - j \to (((φ \land k \in (0 \dots N)) \to D (k) : X ⟶ ℂ) \leftrightarrow ((φ \land i + 1 - j \in (0 \dots N)) \to D (i + 1 - j) : X ⟶ ℂ))$
578	11	a1i	$⊢ φ \to D = (k \in (0 \dots N) ⟼ (S D^{n} G) (k))$
579		fvexd	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} G) (k) \in V$
580	578 579	fvmpt2d	$⊢ (φ \land k \in (0 \dots N)) \to D (k) = (S D^{n} G) (k)$
581	580	feq1d	$⊢ (φ \land k \in (0 \dots N)) \to (D (k) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (k) : X ⟶ ℂ)$
582	9 581	mpbird	$⊢ (φ \land k \in (0 \dots N)) \to D (k) : X ⟶ ℂ$
583	571 572 577 582	vtoclf	$⊢ (φ \land i + 1 - j \in (0 \dots N)) \to D (i + 1 - j) : X ⟶ ℂ$
584	525 566 583	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to D (i + 1 - j) : X ⟶ ℂ$
585	584	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to D (i + 1 - j) : X ⟶ ℂ$
586	585 550	ffvelcdmd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to D (i + 1 - j) (x) \in ℂ$
587	551 586	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to C (j) (x) D (i + 1 - j) (x) \in ℂ$
588	524 587	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) \in ℂ$
589		1zzd	$⊢ i \in (0 ..^N) \to 1 \in ℤ$
590	234	peano2zd	$⊢ i \in (0 ..^N) \to i + 1 \in ℤ$
591	492	eqcomi	$⊢ 1 = 0 + 1$
592	591	a1i	$⊢ i \in (0 ..^N) \to 1 = 0 + 1$
593	173	a1i	$⊢ i \in (0 ..^N) \to 0 \in ℝ$
594		1red	$⊢ i \in (0 ..^N) \to 1 \in ℝ$
595	187	nn0ge0d	$⊢ i \in (0 ..^N) \to 0 \leq i$
596	593 215 594 595	leadd1dd	$⊢ i \in (0 ..^N) \to 0 + 1 \leq i + 1$
597	592 596	eqbrtrd	$⊢ i \in (0 ..^N) \to 1 \leq i + 1$
598	589 590 597	3jca	$⊢ i \in (0 ..^N) \to (1 \in ℤ \land i + 1 \in ℤ \land 1 \leq i + 1)$
599		eluz2	$⊢ i + 1 \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land i + 1 \in ℤ \land 1 \leq i + 1)$
600	598 599	sylibr	$⊢ i \in (0 ..^N) \to i + 1 \in ℤ_{\geq 1}$
601		eluzfz2	$⊢ i + 1 \in ℤ_{\geq 1} \to i + 1 \in (1 \dots i + 1)$
602	600 601	syl	$⊢ i \in (0 ..^N) \to i + 1 \in (1 \dots i + 1)$
603	602	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to i + 1 \in (1 \dots i + 1)$
604		oveq1	$⊢ j = i + 1 \to j - 1 = i + 1 - 1$
605	604	oveq2d	$⊢ j = i + 1 \to (\binom{i}{j - 1}) = (\binom{i}{i + 1 - 1})$
606		fveq2	$⊢ j = i + 1 \to C (j) = C (i + 1)$
607	606	fveq1d	$⊢ j = i + 1 \to C (j) (x) = C (i + 1) (x)$
608		oveq2	$⊢ j = i + 1 \to i + 1 - j = i + 1 - (i + 1)$
609	608	fveq2d	$⊢ j = i + 1 \to D (i + 1 - j) = D (i + 1 - (i + 1))$
610	609	fveq1d	$⊢ j = i + 1 \to D (i + 1 - j) (x) = D (i + 1 - (i + 1)) (x)$
611	607 610	oveq12d	$⊢ j = i + 1 \to C (j) (x) D (i + 1 - j) (x) = C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
612	605 611	oveq12d	$⊢ j = i + 1 \to (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) = (\binom{i}{i + 1 - 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
613	514 515 516 588 603 612	fsumsplit1	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{j = 1}^{i + 1} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) = (\binom{i}{i + 1 - 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x) + \sum_{j \in (1 \dots i + 1) ∖ \{i + 1\}} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
614		1cnd	$⊢ i \in (0 ..^N) \to 1 \in ℂ$
615	503 614	pncand	$⊢ i \in (0 ..^N) \to i + 1 - 1 = i$
616	615	oveq2d	$⊢ i \in (0 ..^N) \to (\binom{i}{i + 1 - 1}) = (\binom{i}{i})$
617		bcnn	$⊢ i \in ℕ_{0} \to (\binom{i}{i}) = 1$
618	187 617	syl	$⊢ i \in (0 ..^N) \to (\binom{i}{i}) = 1$
619	616 618	eqtrd	$⊢ i \in (0 ..^N) \to (\binom{i}{i + 1 - 1}) = 1$
620	503 614	addcld	$⊢ i \in (0 ..^N) \to i + 1 \in ℂ$
621	620	subidd	$⊢ i \in (0 ..^N) \to i + 1 - (i + 1) = 0$
622	621	fveq2d	$⊢ i \in (0 ..^N) \to D (i + 1 - (i + 1)) = D (0)$
623	622	fveq1d	$⊢ i \in (0 ..^N) \to D (i + 1 - (i + 1)) (x) = D (0) (x)$
624	623	oveq2d	$⊢ i \in (0 ..^N) \to C (i + 1) (x) D (i + 1 - (i + 1)) (x) = C (i + 1) (x) D (0) (x)$
625	619 624	oveq12d	$⊢ i \in (0 ..^N) \to (\binom{i}{i + 1 - 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x) = 1 C (i + 1) (x) D (0) (x)$
626	625	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i}{i + 1 - 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x) = 1 C (i + 1) (x) D (0) (x)$
627		simpl	$⊢ (φ \land i \in (0 ..^N)) \to φ$
628		fzofzp1	$⊢ i \in (0 ..^N) \to i + 1 \in (0 \dots N)$
629	628	adantl	$⊢ (φ \land i \in (0 ..^N)) \to i + 1 \in (0 \dots N)$
630		nfv	$⊢ Ⅎ k (φ \land i + 1 \in (0 \dots N))$
631		nfcv	$⊢ \underline{Ⅎ} k (i + 1)$
632	345 631	nffv	$⊢ \underline{Ⅎ} k C (i + 1)$
633	632 348 349	nff	$⊢ Ⅎ k C (i + 1) : X ⟶ ℂ$
634	630 633	nfim	$⊢ Ⅎ k ((φ \land i + 1 \in (0 \dots N)) \to C (i + 1) : X ⟶ ℂ)$
635		ovex	$⊢ i + 1 \in V$
636		eleq1	$⊢ k = i + 1 \to (k \in (0 \dots N) \leftrightarrow i + 1 \in (0 \dots N))$
637	636	anbi2d	$⊢ k = i + 1 \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land i + 1 \in (0 \dots N)))$
638		fveq2	$⊢ k = i + 1 \to C (k) = C (i + 1)$
639	638	feq1d	$⊢ k = i + 1 \to (C (k) : X ⟶ ℂ \leftrightarrow C (i + 1) : X ⟶ ℂ)$
640	637 639	imbi12d	$⊢ k = i + 1 \to (((φ \land k \in (0 \dots N)) \to C (k) : X ⟶ ℂ) \leftrightarrow ((φ \land i + 1 \in (0 \dots N)) \to C (i + 1) : X ⟶ ℂ))$
641	634 635 640 229	vtoclf	$⊢ (φ \land i + 1 \in (0 \dots N)) \to C (i + 1) : X ⟶ ℂ$
642	627 629 641	syl2anc	$⊢ (φ \land i \in (0 ..^N)) \to C (i + 1) : X ⟶ ℂ$
643	642	ffvelcdmda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) \in ℂ$
644		nfv	$⊢ Ⅎ k (φ \land 0 \in (0 \dots N))$
645		nfcv	$⊢ \underline{Ⅎ} k 0$
646	459 645	nffv	$⊢ \underline{Ⅎ} k D (0)$
647	646 348 349	nff	$⊢ Ⅎ k D (0) : X ⟶ ℂ$
648	644 647	nfim	$⊢ Ⅎ k ((φ \land 0 \in (0 \dots N)) \to D (0) : X ⟶ ℂ)$
649		c0ex	$⊢ 0 \in V$
650		eleq1	$⊢ k = 0 \to (k \in (0 \dots N) \leftrightarrow 0 \in (0 \dots N))$
651	650	anbi2d	$⊢ k = 0 \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land 0 \in (0 \dots N)))$
652		fveq2	$⊢ k = 0 \to D (k) = D (0)$
653	652	feq1d	$⊢ k = 0 \to (D (k) : X ⟶ ℂ \leftrightarrow D (0) : X ⟶ ℂ)$
654	651 653	imbi12d	$⊢ k = 0 \to (((φ \land k \in (0 \dots N)) \to D (k) : X ⟶ ℂ) \leftrightarrow ((φ \land 0 \in (0 \dots N)) \to D (0) : X ⟶ ℂ))$
655	648 649 654 582	vtoclf	$⊢ (φ \land 0 \in (0 \dots N)) \to D (0) : X ⟶ ℂ$
656	12 117 655	syl2anc	$⊢ φ \to D (0) : X ⟶ ℂ$
657	656	adantr	$⊢ (φ \land i \in (0 ..^N)) \to D (0) : X ⟶ ℂ$
658	657	ffvelcdmda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (0) (x) \in ℂ$
659	643 658	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) \in ℂ$
660	659	mullidd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 1 C (i + 1) (x) D (0) (x) = C (i + 1) (x) D (0) (x)$
661	626 660	eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i}{i + 1 - 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x) = C (i + 1) (x) D (0) (x)$
662		1m1e0	$⊢ 1 - 1 = 0$
663	662	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
664	13	eqcomi	$⊢ ℤ_{\geq 0} = ℕ_{0}$
665	663 664	eqtr2i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
666	665	a1i	$⊢ i \in (0 ..^N) \to ℕ_{0} = ℤ_{\geq (1 - 1)}$
667	187 666	eleqtrd	$⊢ i \in (0 ..^N) \to i \in ℤ_{\geq (1 - 1)}$
668		fzdifsuc2	$⊢ i \in ℤ_{\geq (1 - 1)} \to (1 \dots i) = (1 \dots i + 1) ∖ \{i + 1\}$
669	667 668	syl	$⊢ i \in (0 ..^N) \to (1 \dots i) = (1 \dots i + 1) ∖ \{i + 1\}$
670	669	eqcomd	$⊢ i \in (0 ..^N) \to (1 \dots i + 1) ∖ \{i + 1\} = (1 \dots i)$
671	670	sumeq1d	$⊢ i \in (0 ..^N) \to \sum_{j \in (1 \dots i + 1) ∖ \{i + 1\}} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) = \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
672	671	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{j \in (1 \dots i + 1) ∖ \{i + 1\}} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) = \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
673	661 672	oveq12d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i}{i + 1 - 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x) + \sum_{j \in (1 \dots i + 1) ∖ \{i + 1\}} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) = C (i + 1) (x) D (0) (x) + \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
674	513 613 673	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{j = 1}^{i + 1} (\binom{i}{j - 1}) C (j - 1 + 1) (x) D (i - (j - 1)) (x) = C (i + 1) (x) D (0) (x) + \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
675	491 495 674	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) = C (i + 1) (x) D (0) (x) + \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
676		nfcv	$⊢ \underline{Ⅎ} k (\binom{i}{0})$
677	345 645	nffv	$⊢ \underline{Ⅎ} k C (0)$
678	677 456	nffv	$⊢ \underline{Ⅎ} k C (0) (x)$
679		nfcv	$⊢ \underline{Ⅎ} k (i + 1 - 0)$
680	459 679	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - 0)$
681	680 456	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - 0) (x)$
682	678 453 681	nfov	$⊢ \underline{Ⅎ} k C (0) (x) D (i + 1 - 0) (x)$
683	676 453 682	nfov	$⊢ \underline{Ⅎ} k (\binom{i}{0}) C (0) (x) D (i + 1 - 0) (x)$
684	664	a1i	$⊢ i \in (0 ..^N) \to ℤ_{\geq 0} = ℕ_{0}$
685	187 684	eleqtrrd	$⊢ i \in (0 ..^N) \to i \in ℤ_{\geq 0}$
686		eluzfz1	$⊢ i \in ℤ_{\geq 0} \to 0 \in (0 \dots i)$
687	685 686	syl	$⊢ i \in (0 ..^N) \to 0 \in (0 \dots i)$
688	687	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 0 \in (0 \dots i)$
689		oveq2	$⊢ k = 0 \to (\binom{i}{k}) = (\binom{i}{0})$
690	110	fveq1d	$⊢ k = 0 \to C (k) (x) = C (0) (x)$
691		oveq2	$⊢ k = 0 \to i + 1 - k = i + 1 - 0$
692	691	fveq2d	$⊢ k = 0 \to D (i + 1 - k) = D (i + 1 - 0)$
693	692	fveq1d	$⊢ k = 0 \to D (i + 1 - k) (x) = D (i + 1 - 0) (x)$
694	690 693	oveq12d	$⊢ k = 0 \to C (k) (x) D (i + 1 - k) (x) = C (0) (x) D (i + 1 - 0) (x)$
695	689 694	oveq12d	$⊢ k = 0 \to (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i}{0}) C (0) (x) D (i + 1 - 0) (x)$
696	470 683 439 441 688 695	fsumsplit1	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i}{0}) C (0) (x) D (i + 1 - 0) (x) + \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
697	620	subid1d	$⊢ i \in (0 ..^N) \to i + 1 - 0 = i + 1$
698	697	fveq2d	$⊢ i \in (0 ..^N) \to D (i + 1 - 0) = D (i + 1)$
699	698	fveq1d	$⊢ i \in (0 ..^N) \to D (i + 1 - 0) (x) = D (i + 1) (x)$
700	699	oveq2d	$⊢ i \in (0 ..^N) \to C (0) (x) D (i + 1 - 0) (x) = C (0) (x) D (i + 1) (x)$
701	700	oveq2d	$⊢ i \in (0 ..^N) \to (\binom{i}{0}) C (0) (x) D (i + 1 - 0) (x) = (\binom{i}{0}) C (0) (x) D (i + 1) (x)$
702	701	oveq1d	$⊢ i \in (0 ..^N) \to (\binom{i}{0}) C (0) (x) D (i + 1 - 0) (x) + \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i}{0}) C (0) (x) D (i + 1) (x) + \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
703	702	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i}{0}) C (0) (x) D (i + 1 - 0) (x) + \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i}{0}) C (0) (x) D (i + 1) (x) + \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
704		bcn0	$⊢ i \in ℕ_{0} \to (\binom{i}{0}) = 1$
705	187 704	syl	$⊢ i \in (0 ..^N) \to (\binom{i}{0}) = 1$
706	705	oveq1d	$⊢ i \in (0 ..^N) \to (\binom{i}{0}) C (0) (x) D (i + 1) (x) = 1 C (0) (x) D (i + 1) (x)$
707	706	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i}{0}) C (0) (x) D (i + 1) (x) = 1 C (0) (x) D (i + 1) (x)$
708	677 348 349	nff	$⊢ Ⅎ k C (0) : X ⟶ ℂ$
709	644 708	nfim	$⊢ Ⅎ k ((φ \land 0 \in (0 \dots N)) \to C (0) : X ⟶ ℂ)$
710	110	feq1d	$⊢ k = 0 \to (C (k) : X ⟶ ℂ \leftrightarrow C (0) : X ⟶ ℂ)$
711	651 710	imbi12d	$⊢ k = 0 \to (((φ \land k \in (0 \dots N)) \to C (k) : X ⟶ ℂ) \leftrightarrow ((φ \land 0 \in (0 \dots N)) \to C (0) : X ⟶ ℂ))$
712	709 649 711 229	vtoclf	$⊢ (φ \land 0 \in (0 \dots N)) \to C (0) : X ⟶ ℂ$
713	12 117 712	syl2anc	$⊢ φ \to C (0) : X ⟶ ℂ$
714	713	adantr	$⊢ (φ \land i \in (0 ..^N)) \to C (0) : X ⟶ ℂ$
715	714	ffvelcdmda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (0) (x) \in ℂ$
716	459 631	nffv	$⊢ \underline{Ⅎ} k D (i + 1)$
717	716 348 349	nff	$⊢ Ⅎ k D (i + 1) : X ⟶ ℂ$
718	630 717	nfim	$⊢ Ⅎ k ((φ \land i + 1 \in (0 \dots N)) \to D (i + 1) : X ⟶ ℂ)$
719		fveq2	$⊢ k = i + 1 \to D (k) = D (i + 1)$
720	719	feq1d	$⊢ k = i + 1 \to (D (k) : X ⟶ ℂ \leftrightarrow D (i + 1) : X ⟶ ℂ)$
721	637 720	imbi12d	$⊢ k = i + 1 \to (((φ \land k \in (0 \dots N)) \to D (k) : X ⟶ ℂ) \leftrightarrow ((φ \land i + 1 \in (0 \dots N)) \to D (i + 1) : X ⟶ ℂ))$
722	718 635 721 582	vtoclf	$⊢ (φ \land i + 1 \in (0 \dots N)) \to D (i + 1) : X ⟶ ℂ$
723	627 629 722	syl2anc	$⊢ (φ \land i \in (0 ..^N)) \to D (i + 1) : X ⟶ ℂ$
724	723	ffvelcdmda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (i + 1) (x) \in ℂ$
725	715 724	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (0) (x) D (i + 1) (x) \in ℂ$
726	725	mullidd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 1 C (0) (x) D (i + 1) (x) = C (0) (x) D (i + 1) (x)$
727	707 726	eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i}{0}) C (0) (x) D (i + 1) (x) = C (0) (x) D (i + 1) (x)$
728		nfv	$⊢ Ⅎ j i \in (0 ..^N)$
729		1zzd	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to 1 \in ℤ$
730	234	adantr	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to i \in ℤ$
731		eldifi	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in (0 \dots i)$
732		elfzelz	$⊢ j \in (0 \dots i) \to j \in ℤ$
733	731 732	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in ℤ$
734	733	adantl	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to j \in ℤ$
735		elfznn0	$⊢ j \in (0 \dots i) \to j \in ℕ_{0}$
736	731 735	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in ℕ_{0}$
737		eldifsni	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \neq 0$
738	736 737	jca	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to (j \in ℕ_{0} \land j \neq 0)$
739		elnnne0	$⊢ j \in ℕ \leftrightarrow (j \in ℕ_{0} \land j \neq 0)$
740	738 739	sylibr	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in ℕ$
741		nnge1	$⊢ j \in ℕ \to 1 \leq j$
742	740 741	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to 1 \leq j$
743	742	adantl	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to 1 \leq j$
744		elfzle2	$⊢ j \in (0 \dots i) \to j \leq i$
745	731 744	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \leq i$
746	745	adantl	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to j \leq i$
747	729 730 734 743 746	elfzd	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to j \in (1 \dots i)$
748	747	ex	$⊢ i \in (0 ..^N) \to (j \in ((0 \dots i) ∖ \{0\}) \to j \in (1 \dots i))$
749		0zd	$⊢ j \in (1 \dots i) \to 0 \in ℤ$
750		elfzel2	$⊢ j \in (1 \dots i) \to i \in ℤ$
751		elfzelz	$⊢ j \in (1 \dots i) \to j \in ℤ$
752	173	a1i	$⊢ j \in (1 \dots i) \to 0 \in ℝ$
753	751	zred	$⊢ j \in (1 \dots i) \to j \in ℝ$
754		1red	$⊢ j \in (1 \dots i) \to 1 \in ℝ$
755	531	a1i	$⊢ j \in (1 \dots i) \to 0 < 1$
756		elfzle1	$⊢ j \in (1 \dots i) \to 1 \leq j$
757	752 754 753 755 756	ltletrd	$⊢ j \in (1 \dots i) \to 0 < j$
758	752 753 757	ltled	$⊢ j \in (1 \dots i) \to 0 \leq j$
759		elfzle2	$⊢ j \in (1 \dots i) \to j \leq i$
760	749 750 751 758 759	elfzd	$⊢ j \in (1 \dots i) \to j \in (0 \dots i)$
761	752 757	gtned	$⊢ j \in (1 \dots i) \to j \neq 0$
762		nelsn	$⊢ j \neq 0 \to \neg j \in \{0\}$
763	761 762	syl	$⊢ j \in (1 \dots i) \to \neg j \in \{0\}$
764	760 763	eldifd	$⊢ j \in (1 \dots i) \to j \in ((0 \dots i) ∖ \{0\})$
765	764	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to j \in ((0 \dots i) ∖ \{0\})$
766	765	ex	$⊢ i \in (0 ..^N) \to (j \in (1 \dots i) \to j \in ((0 \dots i) ∖ \{0\}))$
767	748 766	impbid	$⊢ i \in (0 ..^N) \to (j \in ((0 \dots i) ∖ \{0\}) \leftrightarrow j \in (1 \dots i))$
768	728 767	alrimi	$⊢ i \in (0 ..^N) \to \forall j (j \in ((0 \dots i) ∖ \{0\}) \leftrightarrow j \in (1 \dots i))$
769		dfcleq	$⊢ (0 \dots i) ∖ \{0\} = (1 \dots i) \leftrightarrow \forall j (j \in ((0 \dots i) ∖ \{0\}) \leftrightarrow j \in (1 \dots i))$
770	768 769	sylibr	$⊢ i \in (0 ..^N) \to (0 \dots i) ∖ \{0\} = (1 \dots i)$
771	770	sumeq1d	$⊢ i \in (0 ..^N) \to \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
772	771	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
773	727 772	oveq12d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i}{0}) C (0) (x) D (i + 1) (x) + \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
774	696 703 773	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
775	675 774	oveq12d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) + \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = C (i + 1) (x) D (0) (x) + \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) + C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
776		fzfid	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (1 \dots i) \in Fin$
777	187	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to i \in ℕ_{0}$
778	765 733	syl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to j \in ℤ$
779		1zzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to 1 \in ℤ$
780	778 779	zsubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to j - 1 \in ℤ$
781	777 780	bccld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℕ_{0}$
782	781	nn0cnd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℂ$
783	782	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℂ$
784	783	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℂ$
785		simpl	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to ((φ \land i \in (0 ..^N)) \land x \in X)$
786		fzelp1	$⊢ j \in (1 \dots i) \to j \in (1 \dots i + 1)$
787	786	adantl	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to j \in (1 \dots i + 1)$
788	785 787 551	syl2anc	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to C (j) (x) \in ℂ$
789	787 586	syldan	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to D (i + 1 - j) (x) \in ℂ$
790	788 789	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to C (j) (x) D (i + 1 - j) (x) \in ℂ$
791	784 790	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) \in ℂ$
792	776 791	fsumcl	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) \in ℂ$
793	187	adantr	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to i \in ℕ_{0}$
794		elfzelz	$⊢ k \in (1 \dots i) \to k \in ℤ$
795	794	adantl	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to k \in ℤ$
796	793 795	bccld	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℕ_{0}$
797	796	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℂ$
798	797	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℂ$
799	798	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℂ$
800		simpll	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (φ \land i \in (0 ..^N))$
801		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to x \in X$
802	760	ssriv	$⊢ (1 \dots i) \subseteq (0 \dots i)$
803		id	$⊢ k \in (1 \dots i) \to k \in (1 \dots i)$
804	802 803	sselid	$⊢ k \in (1 \dots i) \to k \in (0 \dots i)$
805	804	adantl	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to k \in (0 \dots i)$
806	800 801 805 433	syl21anc	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to C (k) (x) \in ℂ$
807	805 435	syldan	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to D (i + 1 - k) (x) \in ℂ$
808	806 807	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to C (k) (x) D (i + 1 - k) (x) \in ℂ$
809	799 808	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) \in ℂ$
810	776 809	fsumcl	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) \in ℂ$
811	659 792 725 810	add4d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) + \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) + C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = C (i + 1) (x) D (0) (x) + C (0) (x) D (i + 1) (x) + \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
812		oveq1	$⊢ j = k \to j - 1 = k - 1$
813	812	oveq2d	$⊢ j = k \to (\binom{i}{j - 1}) = (\binom{i}{k - 1})$
814		fveq2	$⊢ j = k \to C (j) = C (k)$
815	814	fveq1d	$⊢ j = k \to C (j) (x) = C (k) (x)$
816		oveq2	$⊢ j = k \to i + 1 - j = i + 1 - k$
817	816	fveq2d	$⊢ j = k \to D (i + 1 - j) = D (i + 1 - k)$
818	817	fveq1d	$⊢ j = k \to D (i + 1 - j) (x) = D (i + 1 - k) (x)$
819	815 818	oveq12d	$⊢ j = k \to C (j) (x) D (i + 1 - j) (x) = C (k) (x) D (i + 1 - k) (x)$
820	813 819	oveq12d	$⊢ j = k \to (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) = (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x)$
821		nfcv	$⊢ \underline{Ⅎ} k (\binom{i}{j - 1})$
822	347 456	nffv	$⊢ \underline{Ⅎ} k C (j) (x)$
823	569 456	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - j) (x)$
824	822 453 823	nfov	$⊢ \underline{Ⅎ} k C (j) (x) D (i + 1 - j) (x)$
825	821 453 824	nfov	$⊢ \underline{Ⅎ} k (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
826		nfcv	$⊢ \underline{Ⅎ} j (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x)$
827	820 825 826	cbvsum	$⊢ \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) = \sum_{k = 1}^{i} (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x)$
828	827	a1i	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) = \sum_{k = 1}^{i} (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x)$
829	828	oveq1d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 1}^{i} (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
830		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
831	795 830	syl	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to k - 1 \in ℤ$
832	793 831	bccld	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℕ_{0}$
833	832	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℂ$
834	833	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℂ$
835	834	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℂ$
836	835 808	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x) \in ℂ$
837	776 836 809	fsumadd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 1}^{i} ((\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x) + (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)) = \sum_{k = 1}^{i} (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
838	837	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 1}^{i} (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 1}^{i} ((\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x) + (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x))$
839	833 797	addcomd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) + (\binom{i}{k}) = (\binom{i}{k}) + (\binom{i}{k - 1})$
840		bcpasc	$⊢ (i \in ℕ_{0} \land k \in ℤ) \to (\binom{i}{k}) + (\binom{i}{k - 1}) = (\binom{i + 1}{k})$
841	793 795 840	syl2anc	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k}) + (\binom{i}{k - 1}) = (\binom{i + 1}{k})$
842	839 841	eqtr2d	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) = (\binom{i}{k - 1}) + (\binom{i}{k})$
843	842	oveq1d	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = ((\binom{i}{k - 1}) + (\binom{i}{k})) C (k) (x) D (i + 1 - k) (x)$
844	843	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = ((\binom{i}{k - 1}) + (\binom{i}{k})) C (k) (x) D (i + 1 - k) (x)$
845	844	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = ((\binom{i}{k - 1}) + (\binom{i}{k})) C (k) (x) D (i + 1 - k) (x)$
846	835 799 808	adddird	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to ((\binom{i}{k - 1}) + (\binom{i}{k})) C (k) (x) D (i + 1 - k) (x) = (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x) + (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)$
847	845 846	eqtr2d	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x) + (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
848	847	sumeq2dv	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 1}^{i} ((\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x) + (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x)) = \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
849	829 838 848	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
850	849	oveq2d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) + C (0) (x) D (i + 1) (x) + \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = C (i + 1) (x) D (0) (x) + C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
851		peano2nn0	$⊢ i \in ℕ_{0} \to i + 1 \in ℕ_{0}$
852	793 851	syl	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to i + 1 \in ℕ_{0}$
853	852 795	bccld	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℕ_{0}$
854	853	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
855	854	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
856	855	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
857	856 808	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) \in ℂ$
858	776 857	fsumcl	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) \in ℂ$
859	659 725 858	addassd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) + C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = C (i + 1) (x) D (0) (x) + C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
860	187 851	syl	$⊢ i \in (0 ..^N) \to i + 1 \in ℕ_{0}$
861		bcn0	$⊢ i + 1 \in ℕ_{0} \to (\binom{i + 1}{0}) = 1$
862	860 861	syl	$⊢ i \in (0 ..^N) \to (\binom{i + 1}{0}) = 1$
863	862 700	oveq12d	$⊢ i \in (0 ..^N) \to (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x) = 1 C (0) (x) D (i + 1) (x)$
864	863	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x) = 1 C (0) (x) D (i + 1) (x)$
865	864 726	eqtr2d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (0) (x) D (i + 1) (x) = (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x)$
866	770	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (0 \dots i) ∖ \{0\} = (1 \dots i)$
867	866	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (1 \dots i) = (0 \dots i) ∖ \{0\}$
868	867	sumeq1d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
869	865 868	oveq12d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x) + \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
870		nfcv	$⊢ \underline{Ⅎ} k (\binom{i + 1}{0})$
871	870 453 682	nfov	$⊢ \underline{Ⅎ} k (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x)$
872	199 851	syl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 \in ℕ_{0}$
873	872 201	bccld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℕ_{0}$
874	873	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
875	874	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
876	875	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
877	876 436	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) \in ℂ$
878		oveq2	$⊢ k = 0 \to (\binom{i + 1}{k}) = (\binom{i + 1}{0})$
879	878 694	oveq12d	$⊢ k = 0 \to (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x)$
880	470 871 439 877 688 879	fsumsplit1	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x) + \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
881	880	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x) + \sum_{k \in (0 \dots i) ∖ \{0\}} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 0}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
882	869 881	eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 0}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
883	882	oveq2d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) + C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = C (i + 1) (x) D (0) (x) + \sum_{k = 0}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
884		bcnn	$⊢ i + 1 \in ℕ_{0} \to (\binom{i + 1}{i + 1}) = 1$
885	860 884	syl	$⊢ i \in (0 ..^N) \to (\binom{i + 1}{i + 1}) = 1$
886	885	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i + 1}{i + 1}) = 1$
887	886	oveq1d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i + 1}{i + 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x) = 1 C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
888	622	adantl	$⊢ (φ \land i \in (0 ..^N)) \to D (i + 1 - (i + 1)) = D (0)$
889	888	feq1d	$⊢ (φ \land i \in (0 ..^N)) \to (D (i + 1 - (i + 1)) : X ⟶ ℂ \leftrightarrow D (0) : X ⟶ ℂ)$
890	657 889	mpbird	$⊢ (φ \land i \in (0 ..^N)) \to D (i + 1 - (i + 1)) : X ⟶ ℂ$
891	890	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (i + 1 - (i + 1)) : X ⟶ ℂ$
892		simpr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to x \in X$
893	891 892	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (i + 1 - (i + 1)) (x) \in ℂ$
894	643 893	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (i + 1 - (i + 1)) (x) \in ℂ$
895	894	mullidd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 1 C (i + 1) (x) D (i + 1 - (i + 1)) (x) = C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
896	624	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (i + 1 - (i + 1)) (x) = C (i + 1) (x) D (0) (x)$
897	887 895 896	3eqtrrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) = (\binom{i + 1}{i + 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
898		fzdifsuc	$⊢ i \in ℤ_{\geq 0} \to (0 \dots i) = (0 \dots i + 1) ∖ \{i + 1\}$
899	685 898	syl	$⊢ i \in (0 ..^N) \to (0 \dots i) = (0 \dots i + 1) ∖ \{i + 1\}$
900	899	sumeq1d	$⊢ i \in (0 ..^N) \to \sum_{k = 0}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k \in (0 \dots i + 1) ∖ \{i + 1\}} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
901	900	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k \in (0 \dots i + 1) ∖ \{i + 1\}} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
902	897 901	oveq12d	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) + \sum_{k = 0}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i + 1}{i + 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x) + \sum_{k \in (0 \dots i + 1) ∖ \{i + 1\}} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
903		nfcv	$⊢ \underline{Ⅎ} k (\binom{i + 1}{i + 1})$
904	632 456	nffv	$⊢ \underline{Ⅎ} k C (i + 1) (x)$
905		nfcv	$⊢ \underline{Ⅎ} k (i + 1 - (i + 1))$
906	459 905	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - (i + 1))$
907	906 456	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - (i + 1)) (x)$
908	904 453 907	nfov	$⊢ \underline{Ⅎ} k C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
909	903 453 908	nfov	$⊢ \underline{Ⅎ} k (\binom{i + 1}{i + 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
910		fzfid	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (0 \dots i + 1) \in Fin$
911	860	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \in ℕ_{0}$
912		elfzelz	$⊢ k \in (0 \dots i + 1) \to k \in ℤ$
913	912	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \in ℤ$
914	911 913	bccld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℕ_{0}$
915	914	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℂ$
916	915	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℂ$
917	916	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℂ$
918	627	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to φ$
919	96	a1i	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \in ℤ$
920	208	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N \in ℤ$
921		elfzle1	$⊢ k \in (0 \dots i + 1) \to 0 \leq k$
922	921	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \leq k$
923	913	zred	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \in ℝ$
924	911	nn0red	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \in ℝ$
925	213	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N \in ℝ$
926		elfzle2	$⊢ k \in (0 \dots i + 1) \to k \leq i + 1$
927	926	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \leq i + 1$
928	301	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \leq N$
929	923 924 925 927 928	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \leq N$
930	919 920 913 922 929	elfzd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \in (0 \dots N)$
931	930	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to k \in (0 \dots N)$
932	918 931 229	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to C (k) : X ⟶ ℂ$
933	932	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to C (k) : X ⟶ ℂ$
934		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to x \in X$
935	933 934	ffvelcdmd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to C (k) (x) \in ℂ$
936	918	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to φ$
937	590	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \in ℤ$
938	937 913	zsubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \in ℤ$
939	924 923	subge0d	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (0 \leq i + 1 - k \leftrightarrow k \leq i + 1)$
940	927 939	mpbird	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \leq i + 1 - k$
941	924 923	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \in ℝ$
942	925 923	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - k \in ℝ$
943	925 173 247	sylancl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - 0 \in ℝ$
944	924 925 923 928	lesub1dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \leq N - k$
945	173	a1i	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \in ℝ$
946	945 923 925 922	lesub2dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - k \leq N - 0$
947	941 942 943 944 946	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \leq N - 0$
948	253	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - 0 = N$
949	947 948	breqtrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \leq N$
950	919 920 938 940 949	elfzd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \in (0 \dots N)$
951	950	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to i + 1 - k \in (0 \dots N)$
952	951	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to i + 1 - k \in (0 \dots N)$
953		fveq2	$⊢ j = i + 1 - k \to D (j) = D (i + 1 - k)$
954	953	feq1d	$⊢ j = i + 1 - k \to (D (j) : X ⟶ ℂ \leftrightarrow D (i + 1 - k) : X ⟶ ℂ)$
955	310 954	imbi12d	$⊢ j = i + 1 - k \to (((φ \land j \in (0 \dots N)) \to D (j) : X ⟶ ℂ) \leftrightarrow ((φ \land i + 1 - k \in (0 \dots N)) \to D (i + 1 - k) : X ⟶ ℂ))$
956	459 346	nffv	$⊢ \underline{Ⅎ} k D (j)$
957	956 348 349	nff	$⊢ Ⅎ k D (j) : X ⟶ ℂ$
958	343 957	nfim	$⊢ Ⅎ k ((φ \land j \in (0 \dots N)) \to D (j) : X ⟶ ℂ)$
959		fveq2	$⊢ k = j \to D (k) = D (j)$
960	959	feq1d	$⊢ k = j \to (D (k) : X ⟶ ℂ \leftrightarrow D (j) : X ⟶ ℂ)$
961	267 960	imbi12d	$⊢ k = j \to (((φ \land k \in (0 \dots N)) \to D (k) : X ⟶ ℂ) \leftrightarrow ((φ \land j \in (0 \dots N)) \to D (j) : X ⟶ ℂ))$
962	958 961 582	chvarfv	$⊢ (φ \land j \in (0 \dots N)) \to D (j) : X ⟶ ℂ$
963	308 955 962	vtocl	$⊢ (φ \land i + 1 - k \in (0 \dots N)) \to D (i + 1 - k) : X ⟶ ℂ$
964	936 952 963	syl2anc	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to D (i + 1 - k) : X ⟶ ℂ$
965	964 934	ffvelcdmd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to D (i + 1 - k) (x) \in ℂ$
966	935 965	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to C (k) (x) D (i + 1 - k) (x) \in ℂ$
967	917 966	mulcld	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) \in ℂ$
968	860 684	eleqtrrd	$⊢ i \in (0 ..^N) \to i + 1 \in ℤ_{\geq 0}$
969		eluzfz2	$⊢ i + 1 \in ℤ_{\geq 0} \to i + 1 \in (0 \dots i + 1)$
970	968 969	syl	$⊢ i \in (0 ..^N) \to i + 1 \in (0 \dots i + 1)$
971	970	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to i + 1 \in (0 \dots i + 1)$
972		oveq2	$⊢ k = i + 1 \to (\binom{i + 1}{k}) = (\binom{i + 1}{i + 1})$
973	638	fveq1d	$⊢ k = i + 1 \to C (k) (x) = C (i + 1) (x)$
974		oveq2	$⊢ k = i + 1 \to i + 1 - k = i + 1 - (i + 1)$
975	974	fveq2d	$⊢ k = i + 1 \to D (i + 1 - k) = D (i + 1 - (i + 1))$
976	975	fveq1d	$⊢ k = i + 1 \to D (i + 1 - k) (x) = D (i + 1 - (i + 1)) (x)$
977	973 976	oveq12d	$⊢ k = i + 1 \to C (k) (x) D (i + 1 - k) (x) = C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
978	972 977	oveq12d	$⊢ k = i + 1 \to (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i + 1}{i + 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
979	470 909 910 967 971 978	fsumsplit1	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = (\binom{i + 1}{i + 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x) + \sum_{k \in (0 \dots i + 1) ∖ \{i + 1\}} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
980	979	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i + 1}{i + 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x) + \sum_{k \in (0 \dots i + 1) ∖ \{i + 1\}} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
981	883 902 980	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) + C (0) (x) D (i + 1) (x) + \sum_{k = 1}^{i} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
982	850 859 981	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) + C (0) (x) D (i + 1) (x) + \sum_{j = 1}^{i} (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x) + \sum_{k = 1}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
983	775 811 982	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i}{k}) C (k + 1) (x) D (i - k) (x) + \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i + 1 - k) (x) = \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
984	438 442 983	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to \sum_{k = 0}^{i} (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x)) = \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x)$
985	984	mpteq2dva	$⊢ (φ \land i \in (0 ..^N)) \to (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) (C (k + 1) (x) D (i - k) (x) + C (k) (x) D (i + 1 - k) (x))) = (x \in X ⟼ \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x))$
986	422 985	eqtrd	$⊢ (φ \land i \in (0 ..^N)) \to \frac{d (x \in X⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))}{d_{S} x} = (x \in X ⟼ \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x))$
987	986	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \to \frac{d (x \in X⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))}{d_{S} x} = (x \in X ⟼ \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x))$
988	191 193 987	3eqtrd	$⊢ ((φ \land i \in (0 ..^N)) \land (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \to (S D^{n} (x \in X ⟼ A B)) (i + 1) = (x \in X ⟼ \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x))$
989	180 181 184 988	syl21anc	$⊢ (i \in (0 ..^N) \land (φ \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \land φ) \to (S D^{n} (x \in X ⟼ A B)) (i + 1) = (x \in X ⟼ \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x))$
990	989	3exp	$⊢ i \in (0 ..^N) \to ((φ \to (S D^{n} (x \in X ⟼ A B)) (i) = (x \in X ⟼ \sum_{k = 0}^{i} (\binom{i}{k}) C (k) (x) D (i - k) (x))) \to (φ \to (S D^{n} (x \in X ⟼ A B)) (i + 1) = (x \in X ⟼ \sum_{k = 0}^{i + 1} (\binom{i + 1}{k}) C (k) (x) D (i + 1 - k) (x))))$
991	44 57 70 83 179 990	fzind2	$⊢ n \in (0 \dots N) \to (φ \to (S D^{n} (x \in X ⟼ A B)) (n) = (x \in X ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) C (k) (x) D (n - k) (x)))$
992	31 991	vtoclg	$⊢ N \in ℕ_{0} \to (N \in (0 \dots N) \to (φ \to (S D^{n} (x \in X ⟼ A B)) (N) = (x \in X ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x))))$
993	5 16 992	sylc	$⊢ φ \to (φ \to (S D^{n} (x \in X ⟼ A B)) (N) = (x \in X ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x)))$
994	12 993	mpd	$⊢ φ \to (S D^{n} (x \in X ⟼ A B)) (N) = (x \in X ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) C (k) (x) D (N - k) (x))$

Metamath Proof Explorer

Theorem dvnmul

Proof