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	mulid2d	$⊢ (φ \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	ffvelrnd	$⊢ ((φ \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	ffvelrnd	$⊢ ((φ \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	ffvelrnda	$⊢ (((φ \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	ffvelrnda	$⊢ (((φ \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	addid2d	$⊢ (((φ \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 (0 \dots i)$
452		nfcv	$⊢ \underline{Ⅎ} k (0 \dots i)$
453		nfcv	$⊢ \underline{Ⅎ} h (\binom{i}{k}) C (k + 1) (x) D (i - k) (x)$
454		nfcv	$⊢ \underline{Ⅎ} k (\binom{i}{h})$
455		nfcv	$⊢ \underline{Ⅎ} k \times$
456		nfcv	$⊢ \underline{Ⅎ} k (h + 1)$
457	345 456	nffv	$⊢ \underline{Ⅎ} k C (h + 1)$
458		nfcv	$⊢ \underline{Ⅎ} k x$
459	457 458	nffv	$⊢ \underline{Ⅎ} k C (h + 1) (x)$
460		nfmpt1	$⊢ \underline{Ⅎ} k (k \in (0 \dots N) ⟼ (S D^{n} G) (k))$
461	11 460	nfcxfr	$⊢ \underline{Ⅎ} k D$
462		nfcv	$⊢ \underline{Ⅎ} k (i - h)$
463	461 462	nffv	$⊢ \underline{Ⅎ} k D (i - h)$
464	463 458	nffv	$⊢ \underline{Ⅎ} k D (i - h) (x)$
465	459 455 464	nfov	$⊢ \underline{Ⅎ} k C (h + 1) (x) D (i - h) (x)$
466	454 455 465	nfov	$⊢ \underline{Ⅎ} k (\binom{i}{h}) C (h + 1) (x) D (i - h) (x)$
467	450 451 452 453 466	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)$
468	467	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)$
469		1zzd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 1 \in ℤ$
470	96	a1i	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 0 \in ℤ$
471	234	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to i \in ℤ$
472		nfv	$⊢ Ⅎ k ((φ \land i \in (0 ..^N)) \land x \in X)$
473		nfcv	$⊢ \underline{Ⅎ} k h$
474	473 452	nfel	$⊢ Ⅎ k h \in (0 \dots i)$
475	472 474	nfan	$⊢ Ⅎ k (((φ \land i \in (0 ..^N)) \land x \in X) \land h \in (0 \dots i))$
476	466 349	nfel	$⊢ Ⅎ k (\binom{i}{h}) C (h + 1) (x) D (i - h) (x) \in ℂ$
477	475 476	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 ℂ)$
478		eleq1	$⊢ k = h \to (k \in (0 \dots i) \leftrightarrow h \in (0 \dots i))$
479	478	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)))$
480	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 ℂ)$
481	479 480	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 ℂ))$
482	477 481 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 ℂ$
483		oveq2	$⊢ h = j - 1 \to (\binom{i}{h}) = (\binom{i}{j - 1})$
484		fvoveq1	$⊢ h = j - 1 \to C (h + 1) = C (j - 1 + 1)$
485	484	fveq1d	$⊢ h = j - 1 \to C (h + 1) (x) = C (j - 1 + 1) (x)$
486		oveq2	$⊢ h = j - 1 \to i - h = i - (j - 1)$
487	486	fveq2d	$⊢ h = j - 1 \to D (i - h) = D (i - (j - 1))$
488	487	fveq1d	$⊢ h = j - 1 \to D (i - h) (x) = D (i - (j - 1)) (x)$
489	485 488	oveq12d	$⊢ h = j - 1 \to C (h + 1) (x) D (i - h) (x) = C (j - 1 + 1) (x) D (i - (j - 1)) (x)$
490	483 489	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)$
491	469 470 471 482 490	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)$
492	468 491	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)$
493		0p1e1	$⊢ 0 + 1 = 1$
494	493	oveq1i	$⊢ (0 + 1 \dots i + 1) = (1 \dots i + 1)$
495	494	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)$
496	495	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)$
497		elfzelz	$⊢ j \in (1 \dots i + 1) \to j \in ℤ$
498	497	zcnd	$⊢ j \in (1 \dots i + 1) \to j \in ℂ$
499		1cnd	$⊢ j \in (1 \dots i + 1) \to 1 \in ℂ$
500	498 499	npcand	$⊢ j \in (1 \dots i + 1) \to j - 1 + 1 = j$
501	500	fveq2d	$⊢ j \in (1 \dots i + 1) \to C (j - 1 + 1) = C (j)$
502	501	fveq1d	$⊢ j \in (1 \dots i + 1) \to C (j - 1 + 1) (x) = C (j) (x)$
503	502	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to C (j - 1 + 1) (x) = C (j) (x)$
504	215	recnd	$⊢ i \in (0 ..^N) \to i \in ℂ$
505	504	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℂ$
506	498	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℂ$
507	499	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 1 \in ℂ$
508	505 506 507	subsub3d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i - (j - 1) = i + 1 - j$
509	508	fveq2d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to D (i - (j - 1)) = D (i + 1 - j)$
510	509	fveq1d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to D (i - (j - 1)) (x) = D (i + 1 - j) (x)$
511	503 510	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)$
512	511	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)$
513	512	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)$
514	513	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)$
515		nfv	$⊢ Ⅎ j ((φ \land i \in (0 ..^N)) \land x \in X)$
516		nfcv	$⊢ \underline{Ⅎ} j (\binom{i}{i + 1 - 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
517		fzfid	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (1 \dots i + 1) \in Fin$
518	187	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℕ_{0}$
519	497	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℤ$
520		1zzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 1 \in ℤ$
521	519 520	zsubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j - 1 \in ℤ$
522	518 521	bccld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℕ_{0}$
523	522	nn0cnd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℂ$
524	523	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℂ$
525	524	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℂ$
526	12	ad2antrr	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to φ$
527		0zd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 0 \in ℤ$
528	208	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to N \in ℤ$
529	173	a1i	$⊢ j \in (1 \dots i + 1) \to 0 \in ℝ$
530	497	zred	$⊢ j \in (1 \dots i + 1) \to j \in ℝ$
531		1red	$⊢ j \in (1 \dots i + 1) \to 1 \in ℝ$
532		0lt1	$⊢ 0 < 1$
533	532	a1i	$⊢ j \in (1 \dots i + 1) \to 0 < 1$
534		elfzle1	$⊢ j \in (1 \dots i + 1) \to 1 \leq j$
535	529 531 530 533 534	ltletrd	$⊢ j \in (1 \dots i + 1) \to 0 < j$
536	529 530 535	ltled	$⊢ j \in (1 \dots i + 1) \to 0 \leq j$
537	536	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 0 \leq j$
538	530	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℝ$
539	215	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℝ$
540		1red	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 1 \in ℝ$
541	539 540	readdcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 \in ℝ$
542	213	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to N \in ℝ$
543		elfzle2	$⊢ j \in (1 \dots i + 1) \to j \leq i + 1$
544	543	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \leq i + 1$
545	301	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 \leq N$
546	538 541 542 544 545	letrd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \leq N$
547	527 528 519 537 546	elfzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in (0 \dots N)$
548	547	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to j \in (0 \dots N)$
549	526 548 355	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to C (j) : X ⟶ ℂ$
550	549	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to C (j) : X ⟶ ℂ$
551		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to x \in X$
552	550 551	ffvelrnd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to C (j) (x) \in ℂ$
553	234	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℤ$
554	553	peano2zd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 \in ℤ$
555	554 519	zsubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \in ℤ$
556	541 538	subge0d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (0 \leq i + 1 - j \leftrightarrow j \leq i + 1)$
557	544 556	mpbird	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 0 \leq i + 1 - j$
558	541 538	resubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \in ℝ$
559	558	leidd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \leq i + 1 - j$
560	530 535	elrpd	$⊢ j \in (1 \dots i + 1) \to j \in ℝ^{+}$
561	560	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℝ^{+}$
562	541 561	ltsubrpd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j < i + 1$
563	558 541 542 562 545	ltletrd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j < N$
564	558 558 542 559 563	lelttrd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j < N$
565	558 542 564	ltled	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \leq N$
566	527 528 555 557 565	elfzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \in (0 \dots N)$
567	566	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to i + 1 - j \in (0 \dots N)$
568		nfv	$⊢ Ⅎ k (φ \land i + 1 - j \in (0 \dots N))$
569		nfcv	$⊢ \underline{Ⅎ} k (i + 1 - j)$
570	461 569	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - j)$
571	570 348 349	nff	$⊢ Ⅎ k D (i + 1 - j) : X ⟶ ℂ$
572	568 571	nfim	$⊢ Ⅎ k ((φ \land i + 1 - j \in (0 \dots N)) \to D (i + 1 - j) : X ⟶ ℂ)$
573		ovex	$⊢ i + 1 - j \in V$
574		eleq1	$⊢ k = i + 1 - j \to (k \in (0 \dots N) \leftrightarrow i + 1 - j \in (0 \dots N))$
575	574	anbi2d	$⊢ k = i + 1 - j \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land i + 1 - j \in (0 \dots N)))$
576		fveq2	$⊢ k = i + 1 - j \to D (k) = D (i + 1 - j)$
577	576	feq1d	$⊢ k = i + 1 - j \to (D (k) : X ⟶ ℂ \leftrightarrow D (i + 1 - j) : X ⟶ ℂ)$
578	575 577	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 ⟶ ℂ))$
579	11	a1i	$⊢ φ \to D = (k \in (0 \dots N) ⟼ (S D^{n} G) (k))$
580		fvexd	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} G) (k) \in V$
581	579 580	fvmpt2d	$⊢ (φ \land k \in (0 \dots N)) \to D (k) = (S D^{n} G) (k)$
582	581	feq1d	$⊢ (φ \land k \in (0 \dots N)) \to (D (k) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (k) : X ⟶ ℂ)$
583	9 582	mpbird	$⊢ (φ \land k \in (0 \dots N)) \to D (k) : X ⟶ ℂ$
584	572 573 578 583	vtoclf	$⊢ (φ \land i + 1 - j \in (0 \dots N)) \to D (i + 1 - j) : X ⟶ ℂ$
585	526 567 584	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to D (i + 1 - j) : X ⟶ ℂ$
586	585	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to D (i + 1 - j) : X ⟶ ℂ$
587	586 551	ffvelrnd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to D (i + 1 - j) (x) \in ℂ$
588	552 587	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 ℂ$
589	525 588	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 ℂ$
590		1zzd	$⊢ i \in (0 ..^N) \to 1 \in ℤ$
591	234	peano2zd	$⊢ i \in (0 ..^N) \to i + 1 \in ℤ$
592	493	eqcomi	$⊢ 1 = 0 + 1$
593	592	a1i	$⊢ i \in (0 ..^N) \to 1 = 0 + 1$
594	173	a1i	$⊢ i \in (0 ..^N) \to 0 \in ℝ$
595		1red	$⊢ i \in (0 ..^N) \to 1 \in ℝ$
596	187	nn0ge0d	$⊢ i \in (0 ..^N) \to 0 \leq i$
597	594 215 595 596	leadd1dd	$⊢ i \in (0 ..^N) \to 0 + 1 \leq i + 1$
598	593 597	eqbrtrd	$⊢ i \in (0 ..^N) \to 1 \leq i + 1$
599	590 591 598	3jca	$⊢ i \in (0 ..^N) \to (1 \in ℤ \land i + 1 \in ℤ \land 1 \leq i + 1)$
600		eluz2	$⊢ i + 1 \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land i + 1 \in ℤ \land 1 \leq i + 1)$
601	599 600	sylibr	$⊢ i \in (0 ..^N) \to i + 1 \in ℤ_{\geq 1}$
602		eluzfz2	$⊢ i + 1 \in ℤ_{\geq 1} \to i + 1 \in (1 \dots i + 1)$
603	601 602	syl	$⊢ i \in (0 ..^N) \to i + 1 \in (1 \dots i + 1)$
604	603	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to i + 1 \in (1 \dots i + 1)$
605		oveq1	$⊢ j = i + 1 \to j - 1 = i + 1 - 1$
606	605	oveq2d	$⊢ j = i + 1 \to (\binom{i}{j - 1}) = (\binom{i}{i + 1 - 1})$
607		fveq2	$⊢ j = i + 1 \to C (j) = C (i + 1)$
608	607	fveq1d	$⊢ j = i + 1 \to C (j) (x) = C (i + 1) (x)$
609		oveq2	$⊢ j = i + 1 \to i + 1 - j = i + 1 - (i + 1)$
610	609	fveq2d	$⊢ j = i + 1 \to D (i + 1 - j) = D (i + 1 - (i + 1))$
611	610	fveq1d	$⊢ j = i + 1 \to D (i + 1 - j) (x) = D (i + 1 - (i + 1)) (x)$
612	608 611	oveq12d	$⊢ j = i + 1 \to C (j) (x) D (i + 1 - j) (x) = C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
613	606 612	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)$
614	515 516 517 589 604 613	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)$
615		1cnd	$⊢ i \in (0 ..^N) \to 1 \in ℂ$
616	504 615	pncand	$⊢ i \in (0 ..^N) \to i + 1 - 1 = i$
617	616	oveq2d	$⊢ i \in (0 ..^N) \to (\binom{i}{i + 1 - 1}) = (\binom{i}{i})$
618		bcnn	$⊢ i \in ℕ_{0} \to (\binom{i}{i}) = 1$
619	187 618	syl	$⊢ i \in (0 ..^N) \to (\binom{i}{i}) = 1$
620	617 619	eqtrd	$⊢ i \in (0 ..^N) \to (\binom{i}{i + 1 - 1}) = 1$
621	504 615	addcld	$⊢ i \in (0 ..^N) \to i + 1 \in ℂ$
622	621	subidd	$⊢ i \in (0 ..^N) \to i + 1 - (i + 1) = 0$
623	622	fveq2d	$⊢ i \in (0 ..^N) \to D (i + 1 - (i + 1)) = D (0)$
624	623	fveq1d	$⊢ i \in (0 ..^N) \to D (i + 1 - (i + 1)) (x) = D (0) (x)$
625	624	oveq2d	$⊢ i \in (0 ..^N) \to C (i + 1) (x) D (i + 1 - (i + 1)) (x) = C (i + 1) (x) D (0) (x)$
626	620 625	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)$
627	626	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)$
628		simpl	$⊢ (φ \land i \in (0 ..^N)) \to φ$
629		fzofzp1	$⊢ i \in (0 ..^N) \to i + 1 \in (0 \dots N)$
630	629	adantl	$⊢ (φ \land i \in (0 ..^N)) \to i + 1 \in (0 \dots N)$
631		nfv	$⊢ Ⅎ k (φ \land i + 1 \in (0 \dots N))$
632		nfcv	$⊢ \underline{Ⅎ} k (i + 1)$
633	345 632	nffv	$⊢ \underline{Ⅎ} k C (i + 1)$
634	633 348 349	nff	$⊢ Ⅎ k C (i + 1) : X ⟶ ℂ$
635	631 634	nfim	$⊢ Ⅎ k ((φ \land i + 1 \in (0 \dots N)) \to C (i + 1) : X ⟶ ℂ)$
636		ovex	$⊢ i + 1 \in V$
637		eleq1	$⊢ k = i + 1 \to (k \in (0 \dots N) \leftrightarrow i + 1 \in (0 \dots N))$
638	637	anbi2d	$⊢ k = i + 1 \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land i + 1 \in (0 \dots N)))$
639		fveq2	$⊢ k = i + 1 \to C (k) = C (i + 1)$
640	639	feq1d	$⊢ k = i + 1 \to (C (k) : X ⟶ ℂ \leftrightarrow C (i + 1) : X ⟶ ℂ)$
641	638 640	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 ⟶ ℂ))$
642	635 636 641 229	vtoclf	$⊢ (φ \land i + 1 \in (0 \dots N)) \to C (i + 1) : X ⟶ ℂ$
643	628 630 642	syl2anc	$⊢ (φ \land i \in (0 ..^N)) \to C (i + 1) : X ⟶ ℂ$
644	643	ffvelrnda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) \in ℂ$
645		nfv	$⊢ Ⅎ k (φ \land 0 \in (0 \dots N))$
646		nfcv	$⊢ \underline{Ⅎ} k 0$
647	461 646	nffv	$⊢ \underline{Ⅎ} k D (0)$
648	647 348 349	nff	$⊢ Ⅎ k D (0) : X ⟶ ℂ$
649	645 648	nfim	$⊢ Ⅎ k ((φ \land 0 \in (0 \dots N)) \to D (0) : X ⟶ ℂ)$
650		c0ex	$⊢ 0 \in V$
651		eleq1	$⊢ k = 0 \to (k \in (0 \dots N) \leftrightarrow 0 \in (0 \dots N))$
652	651	anbi2d	$⊢ k = 0 \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land 0 \in (0 \dots N)))$
653		fveq2	$⊢ k = 0 \to D (k) = D (0)$
654	653	feq1d	$⊢ k = 0 \to (D (k) : X ⟶ ℂ \leftrightarrow D (0) : X ⟶ ℂ)$
655	652 654	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 ⟶ ℂ))$
656	649 650 655 583	vtoclf	$⊢ (φ \land 0 \in (0 \dots N)) \to D (0) : X ⟶ ℂ$
657	12 117 656	syl2anc	$⊢ φ \to D (0) : X ⟶ ℂ$
658	657	adantr	$⊢ (φ \land i \in (0 ..^N)) \to D (0) : X ⟶ ℂ$
659	658	ffvelrnda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (0) (x) \in ℂ$
660	644 659	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) \in ℂ$
661	660	mulid2d	$⊢ ((φ \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)$
662	627 661	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)$
663		1m1e0	$⊢ 1 - 1 = 0$
664	663	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
665	13	eqcomi	$⊢ ℤ_{\geq 0} = ℕ_{0}$
666	664 665	eqtr2i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
667	666	a1i	$⊢ i \in (0 ..^N) \to ℕ_{0} = ℤ_{\geq (1 - 1)}$
668	187 667	eleqtrd	$⊢ i \in (0 ..^N) \to i \in ℤ_{\geq (1 - 1)}$
669		fzdifsuc2	$⊢ i \in ℤ_{\geq (1 - 1)} \to (1 \dots i) = (1 \dots i + 1) ∖ \{i + 1\}$
670	668 669	syl	$⊢ i \in (0 ..^N) \to (1 \dots i) = (1 \dots i + 1) ∖ \{i + 1\}$
671	670	eqcomd	$⊢ i \in (0 ..^N) \to (1 \dots i + 1) ∖ \{i + 1\} = (1 \dots i)$
672	671	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)$
673	672	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)$
674	662 673	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)$
675	514 614 674	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)$
676	492 496 675	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)$
677		nfcv	$⊢ \underline{Ⅎ} k (\binom{i}{0})$
678	345 646	nffv	$⊢ \underline{Ⅎ} k C (0)$
679	678 458	nffv	$⊢ \underline{Ⅎ} k C (0) (x)$
680		nfcv	$⊢ \underline{Ⅎ} k (i + 1 - 0)$
681	461 680	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - 0)$
682	681 458	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - 0) (x)$
683	679 455 682	nfov	$⊢ \underline{Ⅎ} k C (0) (x) D (i + 1 - 0) (x)$
684	677 455 683	nfov	$⊢ \underline{Ⅎ} k (\binom{i}{0}) C (0) (x) D (i + 1 - 0) (x)$
685	665	a1i	$⊢ i \in (0 ..^N) \to ℤ_{\geq 0} = ℕ_{0}$
686	187 685	eleqtrrd	$⊢ i \in (0 ..^N) \to i \in ℤ_{\geq 0}$
687		eluzfz1	$⊢ i \in ℤ_{\geq 0} \to 0 \in (0 \dots i)$
688	686 687	syl	$⊢ i \in (0 ..^N) \to 0 \in (0 \dots i)$
689	688	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 0 \in (0 \dots i)$
690		oveq2	$⊢ k = 0 \to (\binom{i}{k}) = (\binom{i}{0})$
691	110	fveq1d	$⊢ k = 0 \to C (k) (x) = C (0) (x)$
692		oveq2	$⊢ k = 0 \to i + 1 - k = i + 1 - 0$
693	692	fveq2d	$⊢ k = 0 \to D (i + 1 - k) = D (i + 1 - 0)$
694	693	fveq1d	$⊢ k = 0 \to D (i + 1 - k) (x) = D (i + 1 - 0) (x)$
695	691 694	oveq12d	$⊢ k = 0 \to C (k) (x) D (i + 1 - k) (x) = C (0) (x) D (i + 1 - 0) (x)$
696	690 695	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)$
697	472 684 439 441 689 696	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)$
698	621	subid1d	$⊢ i \in (0 ..^N) \to i + 1 - 0 = i + 1$
699	698	fveq2d	$⊢ i \in (0 ..^N) \to D (i + 1 - 0) = D (i + 1)$
700	699	fveq1d	$⊢ i \in (0 ..^N) \to D (i + 1 - 0) (x) = D (i + 1) (x)$
701	700	oveq2d	$⊢ i \in (0 ..^N) \to C (0) (x) D (i + 1 - 0) (x) = C (0) (x) D (i + 1) (x)$
702	701	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)$
703	702	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)$
704	703	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)$
705		bcn0	$⊢ i \in ℕ_{0} \to (\binom{i}{0}) = 1$
706	187 705	syl	$⊢ i \in (0 ..^N) \to (\binom{i}{0}) = 1$
707	706	oveq1d	$⊢ i \in (0 ..^N) \to (\binom{i}{0}) C (0) (x) D (i + 1) (x) = 1 C (0) (x) D (i + 1) (x)$
708	707	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)$
709	678 348 349	nff	$⊢ Ⅎ k C (0) : X ⟶ ℂ$
710	645 709	nfim	$⊢ Ⅎ k ((φ \land 0 \in (0 \dots N)) \to C (0) : X ⟶ ℂ)$
711	110	feq1d	$⊢ k = 0 \to (C (k) : X ⟶ ℂ \leftrightarrow C (0) : X ⟶ ℂ)$
712	652 711	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 ⟶ ℂ))$
713	710 650 712 229	vtoclf	$⊢ (φ \land 0 \in (0 \dots N)) \to C (0) : X ⟶ ℂ$
714	12 117 713	syl2anc	$⊢ φ \to C (0) : X ⟶ ℂ$
715	714	adantr	$⊢ (φ \land i \in (0 ..^N)) \to C (0) : X ⟶ ℂ$
716	715	ffvelrnda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (0) (x) \in ℂ$
717	461 632	nffv	$⊢ \underline{Ⅎ} k D (i + 1)$
718	717 348 349	nff	$⊢ Ⅎ k D (i + 1) : X ⟶ ℂ$
719	631 718	nfim	$⊢ Ⅎ k ((φ \land i + 1 \in (0 \dots N)) \to D (i + 1) : X ⟶ ℂ)$
720		fveq2	$⊢ k = i + 1 \to D (k) = D (i + 1)$
721	720	feq1d	$⊢ k = i + 1 \to (D (k) : X ⟶ ℂ \leftrightarrow D (i + 1) : X ⟶ ℂ)$
722	638 721	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 ⟶ ℂ))$
723	719 636 722 583	vtoclf	$⊢ (φ \land i + 1 \in (0 \dots N)) \to D (i + 1) : X ⟶ ℂ$
724	628 630 723	syl2anc	$⊢ (φ \land i \in (0 ..^N)) \to D (i + 1) : X ⟶ ℂ$
725	724	ffvelrnda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (i + 1) (x) \in ℂ$
726	716 725	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (0) (x) D (i + 1) (x) \in ℂ$
727	726	mulid2d	$⊢ ((φ \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)$
728	708 727	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)$
729		nfv	$⊢ Ⅎ j i \in (0 ..^N)$
730		1zzd	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to 1 \in ℤ$
731	234	adantr	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to i \in ℤ$
732		eldifi	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in (0 \dots i)$
733		elfzelz	$⊢ j \in (0 \dots i) \to j \in ℤ$
734	732 733	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in ℤ$
735	734	adantl	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to j \in ℤ$
736		elfznn0	$⊢ j \in (0 \dots i) \to j \in ℕ_{0}$
737	732 736	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in ℕ_{0}$
738		eldifsni	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \neq 0$
739	737 738	jca	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to (j \in ℕ_{0} \land j \neq 0)$
740		elnnne0	$⊢ j \in ℕ \leftrightarrow (j \in ℕ_{0} \land j \neq 0)$
741	739 740	sylibr	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in ℕ$
742		nnge1	$⊢ j \in ℕ \to 1 \leq j$
743	741 742	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to 1 \leq j$
744	743	adantl	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to 1 \leq j$
745		elfzle2	$⊢ j \in (0 \dots i) \to j \leq i$
746	732 745	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \leq i$
747	746	adantl	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to j \leq i$
748	730 731 735 744 747	elfzd	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to j \in (1 \dots i)$
749	748	ex	$⊢ i \in (0 ..^N) \to (j \in ((0 \dots i) ∖ \{0\}) \to j \in (1 \dots i))$
750		0zd	$⊢ j \in (1 \dots i) \to 0 \in ℤ$
751		elfzel2	$⊢ j \in (1 \dots i) \to i \in ℤ$
752		elfzelz	$⊢ j \in (1 \dots i) \to j \in ℤ$
753	173	a1i	$⊢ j \in (1 \dots i) \to 0 \in ℝ$
754	752	zred	$⊢ j \in (1 \dots i) \to j \in ℝ$
755		1red	$⊢ j \in (1 \dots i) \to 1 \in ℝ$
756	532	a1i	$⊢ j \in (1 \dots i) \to 0 < 1$
757		elfzle1	$⊢ j \in (1 \dots i) \to 1 \leq j$
758	753 755 754 756 757	ltletrd	$⊢ j \in (1 \dots i) \to 0 < j$
759	753 754 758	ltled	$⊢ j \in (1 \dots i) \to 0 \leq j$
760		elfzle2	$⊢ j \in (1 \dots i) \to j \leq i$
761	750 751 752 759 760	elfzd	$⊢ j \in (1 \dots i) \to j \in (0 \dots i)$
762	753 758	gtned	$⊢ j \in (1 \dots i) \to j \neq 0$
763		nelsn	$⊢ j \neq 0 \to \neg j \in \{0\}$
764	762 763	syl	$⊢ j \in (1 \dots i) \to \neg j \in \{0\}$
765	761 764	eldifd	$⊢ j \in (1 \dots i) \to j \in ((0 \dots i) ∖ \{0\})$
766	765	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to j \in ((0 \dots i) ∖ \{0\})$
767	766	ex	$⊢ i \in (0 ..^N) \to (j \in (1 \dots i) \to j \in ((0 \dots i) ∖ \{0\}))$
768	749 767	impbid	$⊢ i \in (0 ..^N) \to (j \in ((0 \dots i) ∖ \{0\}) \leftrightarrow j \in (1 \dots i))$
769	729 768	alrimi	$⊢ i \in (0 ..^N) \to \forall j (j \in ((0 \dots i) ∖ \{0\}) \leftrightarrow j \in (1 \dots i))$
770		dfcleq	$⊢ (0 \dots i) ∖ \{0\} = (1 \dots i) \leftrightarrow \forall j (j \in ((0 \dots i) ∖ \{0\}) \leftrightarrow j \in (1 \dots i))$
771	769 770	sylibr	$⊢ i \in (0 ..^N) \to (0 \dots i) ∖ \{0\} = (1 \dots i)$
772	771	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)$
773	772	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)$
774	728 773	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)$
775	697 704 774	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)$
776	676 775	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)$
777		fzfid	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (1 \dots i) \in Fin$
778	187	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to i \in ℕ_{0}$
779	766 734	syl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to j \in ℤ$
780		1zzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to 1 \in ℤ$
781	779 780	zsubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to j - 1 \in ℤ$
782	778 781	bccld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℕ_{0}$
783	782	nn0cnd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℂ$
784	783	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℂ$
785	784	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℂ$
786		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)$
787		fzelp1	$⊢ j \in (1 \dots i) \to j \in (1 \dots i + 1)$
788	787	adantl	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to j \in (1 \dots i + 1)$
789	786 788 552	syl2anc	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to C (j) (x) \in ℂ$
790	788 587	syldan	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to D (i + 1 - j) (x) \in ℂ$
791	789 790	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 ℂ$
792	785 791	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 ℂ$
793	777 792	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 ℂ$
794	187	adantr	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to i \in ℕ_{0}$
795		elfzelz	$⊢ k \in (1 \dots i) \to k \in ℤ$
796	795	adantl	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to k \in ℤ$
797	794 796	bccld	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℕ_{0}$
798	797	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℂ$
799	798	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℂ$
800	799	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℂ$
801		simpll	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (φ \land i \in (0 ..^N))$
802		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to x \in X$
803	761	ssriv	$⊢ (1 \dots i) \subseteq (0 \dots i)$
804		id	$⊢ k \in (1 \dots i) \to k \in (1 \dots i)$
805	803 804	sselid	$⊢ k \in (1 \dots i) \to k \in (0 \dots i)$
806	805	adantl	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to k \in (0 \dots i)$
807	801 802 806 433	syl21anc	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to C (k) (x) \in ℂ$
808	806 435	syldan	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to D (i + 1 - k) (x) \in ℂ$
809	807 808	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 ℂ$
810	800 809	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 ℂ$
811	777 810	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 ℂ$
812	660 793 726 811	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)$
813		oveq1	$⊢ j = k \to j - 1 = k - 1$
814	813	oveq2d	$⊢ j = k \to (\binom{i}{j - 1}) = (\binom{i}{k - 1})$
815		fveq2	$⊢ j = k \to C (j) = C (k)$
816	815	fveq1d	$⊢ j = k \to C (j) (x) = C (k) (x)$
817		oveq2	$⊢ j = k \to i + 1 - j = i + 1 - k$
818	817	fveq2d	$⊢ j = k \to D (i + 1 - j) = D (i + 1 - k)$
819	818	fveq1d	$⊢ j = k \to D (i + 1 - j) (x) = D (i + 1 - k) (x)$
820	816 819	oveq12d	$⊢ j = k \to C (j) (x) D (i + 1 - j) (x) = C (k) (x) D (i + 1 - k) (x)$
821	814 820	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)$
822		nfcv	$⊢ \underline{Ⅎ} k (1 \dots i)$
823		nfcv	$⊢ \underline{Ⅎ} j (1 \dots i)$
824		nfcv	$⊢ \underline{Ⅎ} k (\binom{i}{j - 1})$
825	347 458	nffv	$⊢ \underline{Ⅎ} k C (j) (x)$
826	570 458	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - j) (x)$
827	825 455 826	nfov	$⊢ \underline{Ⅎ} k C (j) (x) D (i + 1 - j) (x)$
828	824 455 827	nfov	$⊢ \underline{Ⅎ} k (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
829		nfcv	$⊢ \underline{Ⅎ} j (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x)$
830	821 822 823 828 829	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)$
831	830	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)$
832	831	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)$
833		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
834	796 833	syl	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to k - 1 \in ℤ$
835	794 834	bccld	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℕ_{0}$
836	835	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℂ$
837	836	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℂ$
838	837	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℂ$
839	838 809	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 ℂ$
840	777 839 810	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)$
841	840	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))$
842	836 798	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})$
843		bcpasc	$⊢ (i \in ℕ_{0} \land k \in ℤ) \to (\binom{i}{k}) + (\binom{i}{k - 1}) = (\binom{i + 1}{k})$
844	794 796 843	syl2anc	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k}) + (\binom{i}{k - 1}) = (\binom{i + 1}{k})$
845	842 844	eqtr2d	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) = (\binom{i}{k - 1}) + (\binom{i}{k})$
846	845	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)$
847	846	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)$
848	847	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)$
849	838 800 809	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)$
850	848 849	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)$
851	850	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)$
852	832 841 851	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)$
853	852	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)$
854		peano2nn0	$⊢ i \in ℕ_{0} \to i + 1 \in ℕ_{0}$
855	794 854	syl	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to i + 1 \in ℕ_{0}$
856	855 796	bccld	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℕ_{0}$
857	856	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
858	857	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
859	858	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
860	859 809	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 ℂ$
861	777 860	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 ℂ$
862	660 726 861	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)$
863	187 854	syl	$⊢ i \in (0 ..^N) \to i + 1 \in ℕ_{0}$
864		bcn0	$⊢ i + 1 \in ℕ_{0} \to (\binom{i + 1}{0}) = 1$
865	863 864	syl	$⊢ i \in (0 ..^N) \to (\binom{i + 1}{0}) = 1$
866	865 701	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)$
867	866	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)$
868	867 727	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)$
869	771	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (0 \dots i) ∖ \{0\} = (1 \dots i)$
870	869	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (1 \dots i) = (0 \dots i) ∖ \{0\}$
871	870	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)$
872	868 871	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)$
873		nfcv	$⊢ \underline{Ⅎ} k (\binom{i + 1}{0})$
874	873 455 683	nfov	$⊢ \underline{Ⅎ} k (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x)$
875	199 854	syl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 \in ℕ_{0}$
876	875 201	bccld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℕ_{0}$
877	876	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
878	877	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
879	878	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
880	879 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 ℂ$
881		oveq2	$⊢ k = 0 \to (\binom{i + 1}{k}) = (\binom{i + 1}{0})$
882	881 695	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)$
883	472 874 439 880 689 882	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)$
884	883	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)$
885	872 884	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)$
886	885	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)$
887		bcnn	$⊢ i + 1 \in ℕ_{0} \to (\binom{i + 1}{i + 1}) = 1$
888	863 887	syl	$⊢ i \in (0 ..^N) \to (\binom{i + 1}{i + 1}) = 1$
889	888	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i + 1}{i + 1}) = 1$
890	889	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)$
891	623	adantl	$⊢ (φ \land i \in (0 ..^N)) \to D (i + 1 - (i + 1)) = D (0)$
892	891	feq1d	$⊢ (φ \land i \in (0 ..^N)) \to (D (i + 1 - (i + 1)) : X ⟶ ℂ \leftrightarrow D (0) : X ⟶ ℂ)$
893	658 892	mpbird	$⊢ (φ \land i \in (0 ..^N)) \to D (i + 1 - (i + 1)) : X ⟶ ℂ$
894	893	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (i + 1 - (i + 1)) : X ⟶ ℂ$
895		simpr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to x \in X$
896	894 895	ffvelrnd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (i + 1 - (i + 1)) (x) \in ℂ$
897	644 896	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (i + 1 - (i + 1)) (x) \in ℂ$
898	897	mulid2d	$⊢ ((φ \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)$
899	625	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)$
900	890 898 899	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)$
901		fzdifsuc	$⊢ i \in ℤ_{\geq 0} \to (0 \dots i) = (0 \dots i + 1) ∖ \{i + 1\}$
902	686 901	syl	$⊢ i \in (0 ..^N) \to (0 \dots i) = (0 \dots i + 1) ∖ \{i + 1\}$
903	902	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)$
904	903	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)$
905	900 904	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)$
906		nfcv	$⊢ \underline{Ⅎ} k (\binom{i + 1}{i + 1})$
907	633 458	nffv	$⊢ \underline{Ⅎ} k C (i + 1) (x)$
908		nfcv	$⊢ \underline{Ⅎ} k (i + 1 - (i + 1))$
909	461 908	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - (i + 1))$
910	909 458	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - (i + 1)) (x)$
911	907 455 910	nfov	$⊢ \underline{Ⅎ} k C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
912	906 455 911	nfov	$⊢ \underline{Ⅎ} k (\binom{i + 1}{i + 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
913		fzfid	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (0 \dots i + 1) \in Fin$
914	863	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \in ℕ_{0}$
915		elfzelz	$⊢ k \in (0 \dots i + 1) \to k \in ℤ$
916	915	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \in ℤ$
917	914 916	bccld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℕ_{0}$
918	917	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℂ$
919	918	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℂ$
920	919	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℂ$
921	628	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to φ$
922	96	a1i	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \in ℤ$
923	208	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N \in ℤ$
924		elfzle1	$⊢ k \in (0 \dots i + 1) \to 0 \leq k$
925	924	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \leq k$
926	916	zred	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \in ℝ$
927	914	nn0red	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \in ℝ$
928	213	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N \in ℝ$
929		elfzle2	$⊢ k \in (0 \dots i + 1) \to k \leq i + 1$
930	929	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \leq i + 1$
931	301	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \leq N$
932	926 927 928 930 931	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \leq N$
933	922 923 916 925 932	elfzd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \in (0 \dots N)$
934	933	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to k \in (0 \dots N)$
935	921 934 229	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to C (k) : X ⟶ ℂ$
936	935	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to C (k) : X ⟶ ℂ$
937		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to x \in X$
938	936 937	ffvelrnd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to C (k) (x) \in ℂ$
939	921	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to φ$
940	591	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \in ℤ$
941	940 916	zsubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \in ℤ$
942	927 926	subge0d	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (0 \leq i + 1 - k \leftrightarrow k \leq i + 1)$
943	930 942	mpbird	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \leq i + 1 - k$
944	927 926	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \in ℝ$
945	928 926	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - k \in ℝ$
946	928 173 247	sylancl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - 0 \in ℝ$
947	927 928 926 931	lesub1dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \leq N - k$
948	173	a1i	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \in ℝ$
949	948 926 928 925	lesub2dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - k \leq N - 0$
950	944 945 946 947 949	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \leq N - 0$
951	253	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - 0 = N$
952	950 951	breqtrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \leq N$
953	922 923 941 943 952	elfzd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \in (0 \dots N)$
954	953	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to i + 1 - k \in (0 \dots N)$
955	954	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)$
956		fveq2	$⊢ j = i + 1 - k \to D (j) = D (i + 1 - k)$
957	956	feq1d	$⊢ j = i + 1 - k \to (D (j) : X ⟶ ℂ \leftrightarrow D (i + 1 - k) : X ⟶ ℂ)$
958	310 957	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 ⟶ ℂ))$
959	461 346	nffv	$⊢ \underline{Ⅎ} k D (j)$
960	959 348 349	nff	$⊢ Ⅎ k D (j) : X ⟶ ℂ$
961	343 960	nfim	$⊢ Ⅎ k ((φ \land j \in (0 \dots N)) \to D (j) : X ⟶ ℂ)$
962		fveq2	$⊢ k = j \to D (k) = D (j)$
963	962	feq1d	$⊢ k = j \to (D (k) : X ⟶ ℂ \leftrightarrow D (j) : X ⟶ ℂ)$
964	267 963	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 ⟶ ℂ))$
965	961 964 583	chvarfv	$⊢ (φ \land j \in (0 \dots N)) \to D (j) : X ⟶ ℂ$
966	308 958 965	vtocl	$⊢ (φ \land i + 1 - k \in (0 \dots N)) \to D (i + 1 - k) : X ⟶ ℂ$
967	939 955 966	syl2anc	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to D (i + 1 - k) : X ⟶ ℂ$
968	967 937	ffvelrnd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to D (i + 1 - k) (x) \in ℂ$
969	938 968	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 ℂ$
970	920 969	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 ℂ$
971	863 685	eleqtrrd	$⊢ i \in (0 ..^N) \to i + 1 \in ℤ_{\geq 0}$
972		eluzfz2	$⊢ i + 1 \in ℤ_{\geq 0} \to i + 1 \in (0 \dots i + 1)$
973	971 972	syl	$⊢ i \in (0 ..^N) \to i + 1 \in (0 \dots i + 1)$
974	973	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to i + 1 \in (0 \dots i + 1)$
975		oveq2	$⊢ k = i + 1 \to (\binom{i + 1}{k}) = (\binom{i + 1}{i + 1})$
976	639	fveq1d	$⊢ k = i + 1 \to C (k) (x) = C (i + 1) (x)$
977		oveq2	$⊢ k = i + 1 \to i + 1 - k = i + 1 - (i + 1)$
978	977	fveq2d	$⊢ k = i + 1 \to D (i + 1 - k) = D (i + 1 - (i + 1))$
979	978	fveq1d	$⊢ k = i + 1 \to D (i + 1 - k) (x) = D (i + 1 - (i + 1)) (x)$
980	976 979	oveq12d	$⊢ k = i + 1 \to C (k) (x) D (i + 1 - k) (x) = C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
981	975 980	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)$
982	472 912 913 970 974 981	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)$
983	982	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)$
984	886 905 983	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)$
985	853 862 984	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)$
986	776 812 985	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)$
987	438 442 986	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)$
988	987	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))$
989	422 988	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))$
990	989	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))$
991	191 193 990	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))$
992	180 181 184 991	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))$
993	992	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))))$
994	44 57 70 83 179 993	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)))$
995	31 994	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))))$
996	5 16 995	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)))$
997	12 996	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