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	sseldi	$⊢ φ \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	207 209 201	3jca	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (0 \in ℤ \land N \in ℤ \land k \in ℤ)$
211		elfzle1	$⊢ k \in (0 \dots i) \to 0 \leq k$
212	211	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \leq k$
213	201	zred	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \in ℝ$
214	208	zred	$⊢ i \in (0 ..^N) \to N \in ℝ$
215	214	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N \in ℝ$
216	187	nn0red	$⊢ i \in (0 ..^N) \to i \in ℝ$
217	216	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i \in ℝ$
218		elfzle2	$⊢ k \in (0 \dots i) \to k \leq i$
219	218	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \leq i$
220		elfzolt2	$⊢ i \in (0 ..^N) \to i < N$
221	220	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i < N$
222	213 217 215 219 221	lelttrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k < N$
223	213 215 222	ltled	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \leq N$
224	210 212 223	jca32	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to ((0 \in ℤ \land N \in ℤ \land k \in ℤ) \land (0 \leq k \land k \leq N))$
225		elfz2	$⊢ k \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land k \in ℤ) \land (0 \leq k \land k \leq N))$
226	224 225	sylibr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \in (0 \dots N)$
227	226	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to k \in (0 \dots N)$
228	10	a1i	$⊢ φ \to C = (k \in (0 \dots N) ⟼ (S D^{n} F) (k))$
229		fvexd	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) \in V$
230	228 229	fvmpt2d	$⊢ (φ \land k \in (0 \dots N)) \to C (k) = (S D^{n} F) (k)$
231	230	feq1d	$⊢ (φ \land k \in (0 \dots N)) \to (C (k) : X ⟶ ℂ \leftrightarrow (S D^{n} F) (k) : X ⟶ ℂ)$
232	8 231	mpbird	$⊢ (φ \land k \in (0 \dots N)) \to C (k) : X ⟶ ℂ$
233	206 227 232	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k) : X ⟶ ℂ$
234	233	3adant3	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to C (k) : X ⟶ ℂ$
235		simp3	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to x \in X$
236	234 235	ffvelrnd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to C (k) (x) \in ℂ$
237	187	nn0zd	$⊢ i \in (0 ..^N) \to i \in ℤ$
238	237	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i \in ℤ$
239	238 201	zsubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k \in ℤ$
240	207 209 239	3jca	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (0 \in ℤ \land N \in ℤ \land i - k \in ℤ)$
241		elfzel2	$⊢ k \in (0 \dots i) \to i \in ℤ$
242	241	zred	$⊢ k \in (0 \dots i) \to i \in ℝ$
243	200	zred	$⊢ k \in (0 \dots i) \to k \in ℝ$
244	242 243	subge0d	$⊢ k \in (0 \dots i) \to (0 \leq i - k \leftrightarrow k \leq i)$
245	218 244	mpbird	$⊢ k \in (0 \dots i) \to 0 \leq i - k$
246	245	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \leq i - k$
247	217 213	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k \in ℝ$
248	215 213	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - k \in ℝ$
249	173	a1i	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \in ℝ$
250	215 249	jca	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (N \in ℝ \land 0 \in ℝ)$
251		resubcl	$⊢ (N \in ℝ \land 0 \in ℝ) \to N - 0 \in ℝ$
252	250 251	syl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - 0 \in ℝ$
253	217 215 213 221	ltsub1dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k < N - k$
254	249 213 215 212	lesub2dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - k \leq N - 0$
255	247 248 252 253 254	ltletrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k < N - 0$
256	214	recnd	$⊢ i \in (0 ..^N) \to N \in ℂ$
257	256	subid1d	$⊢ i \in (0 ..^N) \to N - 0 = N$
258	257	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - 0 = N$
259	255 258	breqtrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k < N$
260	247 215 259	ltled	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k \leq N$
261	240 246 260	jca32	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to ((0 \in ℤ \land N \in ℤ \land i - k \in ℤ) \land (0 \leq i - k \land i - k \leq N))$
262		elfz2	$⊢ i - k \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land i - k \in ℤ) \land (0 \leq i - k \land i - k \leq N))$
263	261 262	sylibr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k \in (0 \dots N)$
264	263	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to i - k \in (0 \dots N)$
265		ovex	$⊢ i - k \in V$
266		eleq1	$⊢ j = i - k \to (j \in (0 \dots N) \leftrightarrow i - k \in (0 \dots N))$
267	266	anbi2d	$⊢ j = i - k \to ((φ \land j \in (0 \dots N)) \leftrightarrow (φ \land i - k \in (0 \dots N)))$
268		fveq2	$⊢ j = i - k \to (S D^{n} G) (j) = (S D^{n} G) (i - k)$
269	268	feq1d	$⊢ j = i - k \to ((S D^{n} G) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (i - k) : X ⟶ ℂ)$
270	267 269	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 ⟶ ℂ))$
271		nfv	$⊢ Ⅎ k ((φ \land j \in (0 \dots N)) \to (S D^{n} G) (j) : X ⟶ ℂ)$
272		eleq1	$⊢ k = j \to (k \in (0 \dots N) \leftrightarrow j \in (0 \dots N))$
273	272	anbi2d	$⊢ k = j \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land j \in (0 \dots N)))$
274		fveq2	$⊢ k = j \to (S D^{n} G) (k) = (S D^{n} G) (j)$
275	274	feq1d	$⊢ k = j \to ((S D^{n} G) (k) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (j) : X ⟶ ℂ)$
276	273 275	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 ⟶ ℂ))$
277	271 276 9	chvarfv	$⊢ (φ \land j \in (0 \dots N)) \to (S D^{n} G) (j) : X ⟶ ℂ$
278	265 270 277	vtocl	$⊢ (φ \land i - k \in (0 \dots N)) \to (S D^{n} G) (i - k) : X ⟶ ℂ$
279	206 264 278	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k) : X ⟶ ℂ$
280		fveq2	$⊢ n = i - k \to (S D^{n} G) (n) = (S D^{n} G) (i - k)$
281		fvexd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k) \in V$
282	145 280 263 281	fvmptd3	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to D (i - k) = (S D^{n} G) (i - k)$
283	282	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i - k) = (S D^{n} G) (i - k)$
284	283	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 ⟶ ℂ)$
285	279 284	mpbird	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i - k) : X ⟶ ℂ$
286	285	3adant3	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to D (i - k) : X ⟶ ℂ$
287	286 235	ffvelrnd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i) \land x \in X) \to D (i - k) (x) \in ℂ$
288	236 287	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 ℂ$
289	205 288	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 ℂ$
290	205	3expa	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to (\binom{i}{k}) \in ℂ$
291	238	peano2zd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 \in ℤ$
292	291 201	zsubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \in ℤ$
293	207 209 292	3jca	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (0 \in ℤ \land N \in ℤ \land i + 1 - k \in ℤ)$
294		peano2re	$⊢ i \in ℝ \to i + 1 \in ℝ$
295	242 294	syl	$⊢ k \in (0 \dots i) \to i + 1 \in ℝ$
296		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
297	243 296	syl	$⊢ k \in (0 \dots i) \to k + 1 \in ℝ$
298	243	ltp1d	$⊢ k \in (0 \dots i) \to k < k + 1$
299		1red	$⊢ k \in (0 \dots i) \to 1 \in ℝ$
300	243 242 299 218	leadd1dd	$⊢ k \in (0 \dots i) \to k + 1 \leq i + 1$
301	243 297 295 298 300	ltletrd	$⊢ k \in (0 \dots i) \to k < i + 1$
302	243 295 301	ltled	$⊢ k \in (0 \dots i) \to k \leq i + 1$
303	302	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \leq i + 1$
304	217 294	syl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 \in ℝ$
305	304 213	subge0d	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (0 \leq i + 1 - k \leftrightarrow k \leq i + 1)$
306	303 305	mpbird	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \leq i + 1 - k$
307	304 213	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \in ℝ$
308		elfzop1le2	$⊢ i \in (0 ..^N) \to i + 1 \leq N$
309	308	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 \leq N$
310	304 215 213 309	lesub1dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \leq N - k$
311	254 258	breqtrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to N - k \leq N$
312	307 248 215 310 311	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \leq N$
313	293 306 312	jca32	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to ((0 \in ℤ \land N \in ℤ \land i + 1 - k \in ℤ) \land (0 \leq i + 1 - k \land i + 1 - k \leq N))$
314		elfz2	$⊢ i + 1 - k \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land i + 1 - k \in ℤ) \land (0 \leq i + 1 - k \land i + 1 - k \leq N))$
315	313 314	sylibr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k \in (0 \dots N)$
316	315	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to i + 1 - k \in (0 \dots N)$
317		ovex	$⊢ i + 1 - k \in V$
318		eleq1	$⊢ j = i + 1 - k \to (j \in (0 \dots N) \leftrightarrow i + 1 - k \in (0 \dots N))$
319	318	anbi2d	$⊢ j = i + 1 - k \to ((φ \land j \in (0 \dots N)) \leftrightarrow (φ \land i + 1 - k \in (0 \dots N)))$
320		fveq2	$⊢ j = i + 1 - k \to (S D^{n} G) (j) = (S D^{n} G) (i + 1 - k)$
321	320	feq1d	$⊢ j = i + 1 - k \to ((S D^{n} G) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (i + 1 - k) : X ⟶ ℂ)$
322	319 321	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 ⟶ ℂ))$
323	317 322 277	vtocl	$⊢ (φ \land i + 1 - k \in (0 \dots N)) \to (S D^{n} G) (i + 1 - k) : X ⟶ ℂ$
324	206 316 323	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i + 1 - k) : X ⟶ ℂ$
325	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))$
326		simpr	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land n = i + 1 - k) \to n = i + 1 - k$
327	326	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)$
328		fvexd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i + 1 - k) \in V$
329	325 327 316 328	fvmptd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i + 1 - k) = (S D^{n} G) (i + 1 - k)$
330	329	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 ⟶ ℂ)$
331	324 330	mpbird	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i + 1 - k) : X ⟶ ℂ$
332	331	ffvelrnda	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to D (i + 1 - k) (x) \in ℂ$
333	236	3expa	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k) (x) \in ℂ$
334	332 333	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)$
335	334	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)$
336	201	peano2zd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \in ℤ$
337	207 209 336	3jca	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (0 \in ℤ \land N \in ℤ \land k + 1 \in ℤ)$
338	173	a1i	$⊢ k \in (0 \dots i) \to 0 \in ℝ$
339	338 243 297 211 298	lelttrd	$⊢ k \in (0 \dots i) \to 0 < k + 1$
340	338 297 339	ltled	$⊢ k \in (0 \dots i) \to 0 \leq k + 1$
341	340	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 0 \leq k + 1$
342	213 296	syl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \in ℝ$
343	300	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \leq i + 1$
344	342 304 215 343 309	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \leq N$
345	337 341 344	jca32	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to ((0 \in ℤ \land N \in ℤ \land k + 1 \in ℤ) \land (0 \leq k + 1 \land k + 1 \leq N))$
346		elfz2	$⊢ k + 1 \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land k + 1 \in ℤ) \land (0 \leq k + 1 \land k + 1 \leq N))$
347	345 346	sylibr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k + 1 \in (0 \dots N)$
348	347	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to k + 1 \in (0 \dots N)$
349		ovex	$⊢ k + 1 \in V$
350		eleq1	$⊢ j = k + 1 \to (j \in (0 \dots N) \leftrightarrow k + 1 \in (0 \dots N))$
351	350	anbi2d	$⊢ j = k + 1 \to ((φ \land j \in (0 \dots N)) \leftrightarrow (φ \land k + 1 \in (0 \dots N)))$
352		fveq2	$⊢ j = k + 1 \to C (j) = C (k + 1)$
353	352	feq1d	$⊢ j = k + 1 \to (C (j) : X ⟶ ℂ \leftrightarrow C (k + 1) : X ⟶ ℂ)$
354	351 353	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 ⟶ ℂ))$
355		nfv	$⊢ Ⅎ k (φ \land j \in (0 \dots N))$
356		nfmpt1	$⊢ \underline{Ⅎ} k (k \in (0 \dots N) ⟼ (S D^{n} F) (k))$
357	10 356	nfcxfr	$⊢ \underline{Ⅎ} k C$
358		nfcv	$⊢ \underline{Ⅎ} k j$
359	357 358	nffv	$⊢ \underline{Ⅎ} k C (j)$
360		nfcv	$⊢ \underline{Ⅎ} k X$
361		nfcv	$⊢ \underline{Ⅎ} k ℂ$
362	359 360 361	nff	$⊢ Ⅎ k C (j) : X ⟶ ℂ$
363	355 362	nfim	$⊢ Ⅎ k ((φ \land j \in (0 \dots N)) \to C (j) : X ⟶ ℂ)$
364		fveq2	$⊢ k = j \to C (k) = C (j)$
365	364	feq1d	$⊢ k = j \to (C (k) : X ⟶ ℂ \leftrightarrow C (j) : X ⟶ ℂ)$
366	273 365	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 ⟶ ℂ))$
367	363 366 232	chvarfv	$⊢ (φ \land j \in (0 \dots N)) \to C (j) : X ⟶ ℂ$
368	349 354 367	vtocl	$⊢ (φ \land k + 1 \in (0 \dots N)) \to C (k + 1) : X ⟶ ℂ$
369	206 348 368	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k + 1) : X ⟶ ℂ$
370	369	ffvelrnda	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to C (k + 1) (x) \in ℂ$
371	287	3expa	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to D (i - k) (x) \in ℂ$
372	370 371	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 ℂ$
373	332 333	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 ℂ$
374	372 373	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 ℂ$
375	335 374	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 ℂ$
376	290 375	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 ℂ$
377	376	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 ℂ$
378	206 1	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to S \in \{ℝ, ℂ\}$
379	173	a1i	$⊢ (((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \land x \in X) \to 0 \in ℝ$
380	206 2	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
381	378 380 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)$
382	288	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 ℂ$
383	206 227 230	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k) = (S D^{n} F) (k)$
384	383	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} F) (k) = C (k)$
385	233	feqmptd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k) = (x \in X ⟼ C (k) (x))$
386	384 385	eqtr2d	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (x \in X ⟼ C (k) (x)) = (S D^{n} F) (k)$
387	386	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)$
388	378 84	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to S \subseteq ℂ$
389	206 123	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
390		elfznn0	$⊢ k \in (0 \dots i) \to k \in ℕ_{0}$
391	390	adantl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to k \in ℕ_{0}$
392		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)$
393	388 389 391 392	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)$
394	393	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)$
395		fveq2	$⊢ n = k + 1 \to (S D^{n} F) (n) = (S D^{n} F) (k + 1)$
396		fvexd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} F) (k + 1) \in V$
397	114 395 348 396	fvmptd3	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k + 1) = (S D^{n} F) (k + 1)$
398	397	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} F) (k + 1) = C (k + 1)$
399	369	feqmptd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to C (k + 1) = (x \in X ⟼ C (k + 1) (x))$
400	398 399	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))$
401	387 394 400	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))$
402	283	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i - k) = D (i - k)$
403	285	feqmptd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to D (i - k) = (x \in X ⟼ D (i - k) (x))$
404	402 403	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)$
405	404	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)$
406	206 152	syl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to G \in (ℂ ↑_{𝑝𝑚} S)$
407		fznn0sub	$⊢ k \in (0 \dots i) \to i - k \in ℕ_{0}$
408	407	adantl	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to i - k \in ℕ_{0}$
409		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)$
410	388 406 408 409	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)$
411	410	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)$
412	217	recnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i \in ℂ$
413		1cnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to 1 \in ℂ$
414	213	recnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to k \in ℂ$
415	412 413 414	addsubd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 - k = i - k + 1$
416	415	eqcomd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i - k + 1 = i + 1 - k$
417	416	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)$
418	417	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)$
419	329	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (S D^{n} G) (i + 1 - k) = D (i + 1 - k)$
420	331	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))$
421	418 419 420	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))$
422	405 411 421	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))$
423	378 333 370 401 371 332 422	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))$
424	378 290 379 381 382 374 423	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}))$
425	382	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$
426	335	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})$
427	375 290	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))$
428	426 427	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))$
429	425 428	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))$
430	376	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))$
431	429 430	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))$
432	431	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)))$
433	424 432	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)))$
434	194 195 196 197 198 289 377 433	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)))$
435	204	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i}{k}) \in ℂ$
436	372	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 ℂ$
437		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))$
438		ancom	$⊢ (k \in (0 \dots i) \land x \in X) \leftrightarrow (x \in X \land k \in (0 \dots i))$
439	438	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)))$
440		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)))$
441	440	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))$
442	439 441	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))$
443	437 442	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))$
444	443	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 ℂ)$
445	333 444	mpbi	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to C (k) (x) \in ℂ$
446	443	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 ℂ)$
447	332 446	mpbi	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to D (i + 1 - k) (x) \in ℂ$
448	445 447	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 ℂ$
449	435 436 448	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)$
450	449	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))$
451	198	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (0 \dots i) \in Fin$
452	435 436	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 ℂ$
453	435 448	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 ℂ$
454	451 452 453	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)$
455		oveq2	$⊢ k = h \to (\binom{i}{k}) = (\binom{i}{h})$
456		fvoveq1	$⊢ k = h \to C (k + 1) = C (h + 1)$
457	456	fveq1d	$⊢ k = h \to C (k + 1) (x) = C (h + 1) (x)$
458		oveq2	$⊢ k = h \to i - k = i - h$
459	458	fveq2d	$⊢ k = h \to D (i - k) = D (i - h)$
460	459	fveq1d	$⊢ k = h \to D (i - k) (x) = D (i - h) (x)$
461	457 460	oveq12d	$⊢ k = h \to C (k + 1) (x) D (i - k) (x) = C (h + 1) (x) D (i - h) (x)$
462	455 461	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)$
463		nfcv	$⊢ \underline{Ⅎ} h (0 \dots i)$
464		nfcv	$⊢ \underline{Ⅎ} k (0 \dots i)$
465		nfcv	$⊢ \underline{Ⅎ} h (\binom{i}{k}) C (k + 1) (x) D (i - k) (x)$
466		nfcv	$⊢ \underline{Ⅎ} k (\binom{i}{h})$
467		nfcv	$⊢ \underline{Ⅎ} k \times$
468		nfcv	$⊢ \underline{Ⅎ} k (h + 1)$
469	357 468	nffv	$⊢ \underline{Ⅎ} k C (h + 1)$
470		nfcv	$⊢ \underline{Ⅎ} k x$
471	469 470	nffv	$⊢ \underline{Ⅎ} k C (h + 1) (x)$
472		nfmpt1	$⊢ \underline{Ⅎ} k (k \in (0 \dots N) ⟼ (S D^{n} G) (k))$
473	11 472	nfcxfr	$⊢ \underline{Ⅎ} k D$
474		nfcv	$⊢ \underline{Ⅎ} k (i - h)$
475	473 474	nffv	$⊢ \underline{Ⅎ} k D (i - h)$
476	475 470	nffv	$⊢ \underline{Ⅎ} k D (i - h) (x)$
477	471 467 476	nfov	$⊢ \underline{Ⅎ} k C (h + 1) (x) D (i - h) (x)$
478	466 467 477	nfov	$⊢ \underline{Ⅎ} k (\binom{i}{h}) C (h + 1) (x) D (i - h) (x)$
479	462 463 464 465 478	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)$
480	479	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)$
481		1zzd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 1 \in ℤ$
482	96	a1i	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 0 \in ℤ$
483	237	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to i \in ℤ$
484		nfv	$⊢ Ⅎ k ((φ \land i \in (0 ..^N)) \land x \in X)$
485		nfcv	$⊢ \underline{Ⅎ} k h$
486	485 464	nfel	$⊢ Ⅎ k h \in (0 \dots i)$
487	484 486	nfan	$⊢ Ⅎ k (((φ \land i \in (0 ..^N)) \land x \in X) \land h \in (0 \dots i))$
488	478 361	nfel	$⊢ Ⅎ k (\binom{i}{h}) C (h + 1) (x) D (i - h) (x) \in ℂ$
489	487 488	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 ℂ)$
490		eleq1	$⊢ k = h \to (k \in (0 \dots i) \leftrightarrow h \in (0 \dots i))$
491	490	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)))$
492	462	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 ℂ)$
493	491 492	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 ℂ))$
494	489 493 452	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 ℂ$
495		oveq2	$⊢ h = j - 1 \to (\binom{i}{h}) = (\binom{i}{j - 1})$
496		fvoveq1	$⊢ h = j - 1 \to C (h + 1) = C (j - 1 + 1)$
497	496	fveq1d	$⊢ h = j - 1 \to C (h + 1) (x) = C (j - 1 + 1) (x)$
498		oveq2	$⊢ h = j - 1 \to i - h = i - (j - 1)$
499	498	fveq2d	$⊢ h = j - 1 \to D (i - h) = D (i - (j - 1))$
500	499	fveq1d	$⊢ h = j - 1 \to D (i - h) (x) = D (i - (j - 1)) (x)$
501	497 500	oveq12d	$⊢ h = j - 1 \to C (h + 1) (x) D (i - h) (x) = C (j - 1 + 1) (x) D (i - (j - 1)) (x)$
502	495 501	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)$
503	481 482 483 494 502	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)$
504	480 503	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)$
505		0p1e1	$⊢ 0 + 1 = 1$
506	505	oveq1i	$⊢ (0 + 1 \dots i + 1) = (1 \dots i + 1)$
507	506	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)$
508	507	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)$
509		elfzelz	$⊢ j \in (1 \dots i + 1) \to j \in ℤ$
510	509	zcnd	$⊢ j \in (1 \dots i + 1) \to j \in ℂ$
511		1cnd	$⊢ j \in (1 \dots i + 1) \to 1 \in ℂ$
512	510 511	npcand	$⊢ j \in (1 \dots i + 1) \to j - 1 + 1 = j$
513	512	fveq2d	$⊢ j \in (1 \dots i + 1) \to C (j - 1 + 1) = C (j)$
514	513	fveq1d	$⊢ j \in (1 \dots i + 1) \to C (j - 1 + 1) (x) = C (j) (x)$
515	514	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to C (j - 1 + 1) (x) = C (j) (x)$
516	216	recnd	$⊢ i \in (0 ..^N) \to i \in ℂ$
517	516	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℂ$
518	510	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℂ$
519	511	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 1 \in ℂ$
520	517 518 519	subsub3d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i - (j - 1) = i + 1 - j$
521	520	fveq2d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to D (i - (j - 1)) = D (i + 1 - j)$
522	521	fveq1d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to D (i - (j - 1)) (x) = D (i + 1 - j) (x)$
523	515 522	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)$
524	523	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)$
525	524	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)$
526	525	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)$
527		nfv	$⊢ Ⅎ j ((φ \land i \in (0 ..^N)) \land x \in X)$
528		nfcv	$⊢ \underline{Ⅎ} j (\binom{i}{i + 1 - 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
529		fzfid	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (1 \dots i + 1) \in Fin$
530	187	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℕ_{0}$
531	509	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℤ$
532		1zzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 1 \in ℤ$
533	531 532	zsubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j - 1 \in ℤ$
534	530 533	bccld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℕ_{0}$
535	534	nn0cnd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℂ$
536	535	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℂ$
537	536	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to (\binom{i}{j - 1}) \in ℂ$
538	12	ad2antrr	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to φ$
539		0zd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 0 \in ℤ$
540	208	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to N \in ℤ$
541	539 540 531	3jca	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (0 \in ℤ \land N \in ℤ \land j \in ℤ)$
542	173	a1i	$⊢ j \in (1 \dots i + 1) \to 0 \in ℝ$
543	509	zred	$⊢ j \in (1 \dots i + 1) \to j \in ℝ$
544		1red	$⊢ j \in (1 \dots i + 1) \to 1 \in ℝ$
545		0lt1	$⊢ 0 < 1$
546	545	a1i	$⊢ j \in (1 \dots i + 1) \to 0 < 1$
547		elfzle1	$⊢ j \in (1 \dots i + 1) \to 1 \leq j$
548	542 544 543 546 547	ltletrd	$⊢ j \in (1 \dots i + 1) \to 0 < j$
549	542 543 548	ltled	$⊢ j \in (1 \dots i + 1) \to 0 \leq j$
550	549	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 0 \leq j$
551	543	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℝ$
552	216	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℝ$
553		1red	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 1 \in ℝ$
554	552 553	readdcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 \in ℝ$
555	214	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to N \in ℝ$
556		elfzle2	$⊢ j \in (1 \dots i + 1) \to j \leq i + 1$
557	556	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \leq i + 1$
558	308	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 \leq N$
559	551 554 555 557 558	letrd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \leq N$
560	541 550 559	jca32	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to ((0 \in ℤ \land N \in ℤ \land j \in ℤ) \land (0 \leq j \land j \leq N))$
561		elfz2	$⊢ j \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land j \in ℤ) \land (0 \leq j \land j \leq N))$
562	560 561	sylibr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in (0 \dots N)$
563	562	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to j \in (0 \dots N)$
564	538 563 367	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to C (j) : X ⟶ ℂ$
565	564	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to C (j) : X ⟶ ℂ$
566		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to x \in X$
567	565 566	ffvelrnd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to C (j) (x) \in ℂ$
568	237	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i \in ℤ$
569	568	peano2zd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 \in ℤ$
570	569 531	zsubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \in ℤ$
571	539 540 570	3jca	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (0 \in ℤ \land N \in ℤ \land i + 1 - j \in ℤ)$
572	554 551	subge0d	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to (0 \leq i + 1 - j \leftrightarrow j \leq i + 1)$
573	557 572	mpbird	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to 0 \leq i + 1 - j$
574	554 551	resubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \in ℝ$
575	574	leidd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \leq i + 1 - j$
576	543 548	elrpd	$⊢ j \in (1 \dots i + 1) \to j \in ℝ^{+}$
577	576	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to j \in ℝ^{+}$
578	554 577	ltsubrpd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j < i + 1$
579	574 554 555 578 558	ltletrd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j < N$
580	574 574 555 575 579	lelttrd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j < N$
581	574 555 580	ltled	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \leq N$
582	571 573 581	jca32	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to ((0 \in ℤ \land N \in ℤ \land i + 1 - j \in ℤ) \land (0 \leq i + 1 - j \land i + 1 - j \leq N))$
583		elfz2	$⊢ i + 1 - j \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land i + 1 - j \in ℤ) \land (0 \leq i + 1 - j \land i + 1 - j \leq N))$
584	582 583	sylibr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i + 1)) \to i + 1 - j \in (0 \dots N)$
585	584	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to i + 1 - j \in (0 \dots N)$
586		nfv	$⊢ Ⅎ k (φ \land i + 1 - j \in (0 \dots N))$
587		nfcv	$⊢ \underline{Ⅎ} k (i + 1 - j)$
588	473 587	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - j)$
589	588 360 361	nff	$⊢ Ⅎ k D (i + 1 - j) : X ⟶ ℂ$
590	586 589	nfim	$⊢ Ⅎ k ((φ \land i + 1 - j \in (0 \dots N)) \to D (i + 1 - j) : X ⟶ ℂ)$
591		ovex	$⊢ i + 1 - j \in V$
592		eleq1	$⊢ k = i + 1 - j \to (k \in (0 \dots N) \leftrightarrow i + 1 - j \in (0 \dots N))$
593	592	anbi2d	$⊢ k = i + 1 - j \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land i + 1 - j \in (0 \dots N)))$
594		fveq2	$⊢ k = i + 1 - j \to D (k) = D (i + 1 - j)$
595	594	feq1d	$⊢ k = i + 1 - j \to (D (k) : X ⟶ ℂ \leftrightarrow D (i + 1 - j) : X ⟶ ℂ)$
596	593 595	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 ⟶ ℂ))$
597	11	a1i	$⊢ φ \to D = (k \in (0 \dots N) ⟼ (S D^{n} G) (k))$
598		fvexd	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} G) (k) \in V$
599	597 598	fvmpt2d	$⊢ (φ \land k \in (0 \dots N)) \to D (k) = (S D^{n} G) (k)$
600	599	feq1d	$⊢ (φ \land k \in (0 \dots N)) \to (D (k) : X ⟶ ℂ \leftrightarrow (S D^{n} G) (k) : X ⟶ ℂ)$
601	9 600	mpbird	$⊢ (φ \land k \in (0 \dots N)) \to D (k) : X ⟶ ℂ$
602	590 591 596 601	vtoclf	$⊢ (φ \land i + 1 - j \in (0 \dots N)) \to D (i + 1 - j) : X ⟶ ℂ$
603	538 585 602	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i + 1)) \to D (i + 1 - j) : X ⟶ ℂ$
604	603	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to D (i + 1 - j) : X ⟶ ℂ$
605	604 566	ffvelrnd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i + 1)) \to D (i + 1 - j) (x) \in ℂ$
606	567 605	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 ℂ$
607	537 606	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 ℂ$
608		1zzd	$⊢ i \in (0 ..^N) \to 1 \in ℤ$
609	237	peano2zd	$⊢ i \in (0 ..^N) \to i + 1 \in ℤ$
610	505	eqcomi	$⊢ 1 = 0 + 1$
611	610	a1i	$⊢ i \in (0 ..^N) \to 1 = 0 + 1$
612	173	a1i	$⊢ i \in (0 ..^N) \to 0 \in ℝ$
613		1red	$⊢ i \in (0 ..^N) \to 1 \in ℝ$
614	187	nn0ge0d	$⊢ i \in (0 ..^N) \to 0 \leq i$
615	612 216 613 614	leadd1dd	$⊢ i \in (0 ..^N) \to 0 + 1 \leq i + 1$
616	611 615	eqbrtrd	$⊢ i \in (0 ..^N) \to 1 \leq i + 1$
617	608 609 616	3jca	$⊢ i \in (0 ..^N) \to (1 \in ℤ \land i + 1 \in ℤ \land 1 \leq i + 1)$
618		eluz2	$⊢ i + 1 \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land i + 1 \in ℤ \land 1 \leq i + 1)$
619	617 618	sylibr	$⊢ i \in (0 ..^N) \to i + 1 \in ℤ_{\geq 1}$
620		eluzfz2	$⊢ i + 1 \in ℤ_{\geq 1} \to i + 1 \in (1 \dots i + 1)$
621	619 620	syl	$⊢ i \in (0 ..^N) \to i + 1 \in (1 \dots i + 1)$
622	621	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to i + 1 \in (1 \dots i + 1)$
623		oveq1	$⊢ j = i + 1 \to j - 1 = i + 1 - 1$
624	623	oveq2d	$⊢ j = i + 1 \to (\binom{i}{j - 1}) = (\binom{i}{i + 1 - 1})$
625		fveq2	$⊢ j = i + 1 \to C (j) = C (i + 1)$
626	625	fveq1d	$⊢ j = i + 1 \to C (j) (x) = C (i + 1) (x)$
627		oveq2	$⊢ j = i + 1 \to i + 1 - j = i + 1 - (i + 1)$
628	627	fveq2d	$⊢ j = i + 1 \to D (i + 1 - j) = D (i + 1 - (i + 1))$
629	628	fveq1d	$⊢ j = i + 1 \to D (i + 1 - j) (x) = D (i + 1 - (i + 1)) (x)$
630	626 629	oveq12d	$⊢ j = i + 1 \to C (j) (x) D (i + 1 - j) (x) = C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
631	624 630	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)$
632	527 528 529 607 622 631	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)$
633		1cnd	$⊢ i \in (0 ..^N) \to 1 \in ℂ$
634	516 633	pncand	$⊢ i \in (0 ..^N) \to i + 1 - 1 = i$
635	634	oveq2d	$⊢ i \in (0 ..^N) \to (\binom{i}{i + 1 - 1}) = (\binom{i}{i})$
636		bcnn	$⊢ i \in ℕ_{0} \to (\binom{i}{i}) = 1$
637	187 636	syl	$⊢ i \in (0 ..^N) \to (\binom{i}{i}) = 1$
638	635 637	eqtrd	$⊢ i \in (0 ..^N) \to (\binom{i}{i + 1 - 1}) = 1$
639	516 633	addcld	$⊢ i \in (0 ..^N) \to i + 1 \in ℂ$
640	639	subidd	$⊢ i \in (0 ..^N) \to i + 1 - (i + 1) = 0$
641	640	fveq2d	$⊢ i \in (0 ..^N) \to D (i + 1 - (i + 1)) = D (0)$
642	641	fveq1d	$⊢ i \in (0 ..^N) \to D (i + 1 - (i + 1)) (x) = D (0) (x)$
643	642	oveq2d	$⊢ i \in (0 ..^N) \to C (i + 1) (x) D (i + 1 - (i + 1)) (x) = C (i + 1) (x) D (0) (x)$
644	638 643	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)$
645	644	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)$
646		simpl	$⊢ (φ \land i \in (0 ..^N)) \to φ$
647		fzofzp1	$⊢ i \in (0 ..^N) \to i + 1 \in (0 \dots N)$
648	647	adantl	$⊢ (φ \land i \in (0 ..^N)) \to i + 1 \in (0 \dots N)$
649		nfv	$⊢ Ⅎ k (φ \land i + 1 \in (0 \dots N))$
650		nfcv	$⊢ \underline{Ⅎ} k (i + 1)$
651	357 650	nffv	$⊢ \underline{Ⅎ} k C (i + 1)$
652	651 360 361	nff	$⊢ Ⅎ k C (i + 1) : X ⟶ ℂ$
653	649 652	nfim	$⊢ Ⅎ k ((φ \land i + 1 \in (0 \dots N)) \to C (i + 1) : X ⟶ ℂ)$
654		ovex	$⊢ i + 1 \in V$
655		eleq1	$⊢ k = i + 1 \to (k \in (0 \dots N) \leftrightarrow i + 1 \in (0 \dots N))$
656	655	anbi2d	$⊢ k = i + 1 \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land i + 1 \in (0 \dots N)))$
657		fveq2	$⊢ k = i + 1 \to C (k) = C (i + 1)$
658	657	feq1d	$⊢ k = i + 1 \to (C (k) : X ⟶ ℂ \leftrightarrow C (i + 1) : X ⟶ ℂ)$
659	656 658	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 ⟶ ℂ))$
660	653 654 659 232	vtoclf	$⊢ (φ \land i + 1 \in (0 \dots N)) \to C (i + 1) : X ⟶ ℂ$
661	646 648 660	syl2anc	$⊢ (φ \land i \in (0 ..^N)) \to C (i + 1) : X ⟶ ℂ$
662	661	ffvelrnda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) \in ℂ$
663		nfv	$⊢ Ⅎ k (φ \land 0 \in (0 \dots N))$
664		nfcv	$⊢ \underline{Ⅎ} k 0$
665	473 664	nffv	$⊢ \underline{Ⅎ} k D (0)$
666	665 360 361	nff	$⊢ Ⅎ k D (0) : X ⟶ ℂ$
667	663 666	nfim	$⊢ Ⅎ k ((φ \land 0 \in (0 \dots N)) \to D (0) : X ⟶ ℂ)$
668		c0ex	$⊢ 0 \in V$
669		eleq1	$⊢ k = 0 \to (k \in (0 \dots N) \leftrightarrow 0 \in (0 \dots N))$
670	669	anbi2d	$⊢ k = 0 \to ((φ \land k \in (0 \dots N)) \leftrightarrow (φ \land 0 \in (0 \dots N)))$
671		fveq2	$⊢ k = 0 \to D (k) = D (0)$
672	671	feq1d	$⊢ k = 0 \to (D (k) : X ⟶ ℂ \leftrightarrow D (0) : X ⟶ ℂ)$
673	670 672	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 ⟶ ℂ))$
674	667 668 673 601	vtoclf	$⊢ (φ \land 0 \in (0 \dots N)) \to D (0) : X ⟶ ℂ$
675	12 117 674	syl2anc	$⊢ φ \to D (0) : X ⟶ ℂ$
676	675	adantr	$⊢ (φ \land i \in (0 ..^N)) \to D (0) : X ⟶ ℂ$
677	676	ffvelrnda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (0) (x) \in ℂ$
678	662 677	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (0) (x) \in ℂ$
679	678	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)$
680	645 679	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)$
681		1m1e0	$⊢ 1 - 1 = 0$
682	681	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
683	13	eqcomi	$⊢ ℤ_{\geq 0} = ℕ_{0}$
684	682 683	eqtr2i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
685	684	a1i	$⊢ i \in (0 ..^N) \to ℕ_{0} = ℤ_{\geq (1 - 1)}$
686	187 685	eleqtrd	$⊢ i \in (0 ..^N) \to i \in ℤ_{\geq (1 - 1)}$
687		fzdifsuc2	$⊢ i \in ℤ_{\geq (1 - 1)} \to (1 \dots i) = (1 \dots i + 1) ∖ \{i + 1\}$
688	686 687	syl	$⊢ i \in (0 ..^N) \to (1 \dots i) = (1 \dots i + 1) ∖ \{i + 1\}$
689	688	eqcomd	$⊢ i \in (0 ..^N) \to (1 \dots i + 1) ∖ \{i + 1\} = (1 \dots i)$
690	689	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)$
691	690	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)$
692	680 691	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)$
693	526 632 692	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)$
694	504 508 693	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)$
695		nfcv	$⊢ \underline{Ⅎ} k (\binom{i}{0})$
696	357 664	nffv	$⊢ \underline{Ⅎ} k C (0)$
697	696 470	nffv	$⊢ \underline{Ⅎ} k C (0) (x)$
698		nfcv	$⊢ \underline{Ⅎ} k (i + 1 - 0)$
699	473 698	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - 0)$
700	699 470	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - 0) (x)$
701	697 467 700	nfov	$⊢ \underline{Ⅎ} k C (0) (x) D (i + 1 - 0) (x)$
702	695 467 701	nfov	$⊢ \underline{Ⅎ} k (\binom{i}{0}) C (0) (x) D (i + 1 - 0) (x)$
703	683	a1i	$⊢ i \in (0 ..^N) \to ℤ_{\geq 0} = ℕ_{0}$
704	187 703	eleqtrrd	$⊢ i \in (0 ..^N) \to i \in ℤ_{\geq 0}$
705		eluzfz1	$⊢ i \in ℤ_{\geq 0} \to 0 \in (0 \dots i)$
706	704 705	syl	$⊢ i \in (0 ..^N) \to 0 \in (0 \dots i)$
707	706	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to 0 \in (0 \dots i)$
708		oveq2	$⊢ k = 0 \to (\binom{i}{k}) = (\binom{i}{0})$
709	110	fveq1d	$⊢ k = 0 \to C (k) (x) = C (0) (x)$
710		oveq2	$⊢ k = 0 \to i + 1 - k = i + 1 - 0$
711	710	fveq2d	$⊢ k = 0 \to D (i + 1 - k) = D (i + 1 - 0)$
712	711	fveq1d	$⊢ k = 0 \to D (i + 1 - k) (x) = D (i + 1 - 0) (x)$
713	709 712	oveq12d	$⊢ k = 0 \to C (k) (x) D (i + 1 - k) (x) = C (0) (x) D (i + 1 - 0) (x)$
714	708 713	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)$
715	484 702 451 453 707 714	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)$
716	639	subid1d	$⊢ i \in (0 ..^N) \to i + 1 - 0 = i + 1$
717	716	fveq2d	$⊢ i \in (0 ..^N) \to D (i + 1 - 0) = D (i + 1)$
718	717	fveq1d	$⊢ i \in (0 ..^N) \to D (i + 1 - 0) (x) = D (i + 1) (x)$
719	718	oveq2d	$⊢ i \in (0 ..^N) \to C (0) (x) D (i + 1 - 0) (x) = C (0) (x) D (i + 1) (x)$
720	719	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)$
721	720	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)$
722	721	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)$
723		bcn0	$⊢ i \in ℕ_{0} \to (\binom{i}{0}) = 1$
724	187 723	syl	$⊢ i \in (0 ..^N) \to (\binom{i}{0}) = 1$
725	724	oveq1d	$⊢ i \in (0 ..^N) \to (\binom{i}{0}) C (0) (x) D (i + 1) (x) = 1 C (0) (x) D (i + 1) (x)$
726	725	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)$
727	696 360 361	nff	$⊢ Ⅎ k C (0) : X ⟶ ℂ$
728	663 727	nfim	$⊢ Ⅎ k ((φ \land 0 \in (0 \dots N)) \to C (0) : X ⟶ ℂ)$
729	110	feq1d	$⊢ k = 0 \to (C (k) : X ⟶ ℂ \leftrightarrow C (0) : X ⟶ ℂ)$
730	670 729	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 ⟶ ℂ))$
731	728 668 730 232	vtoclf	$⊢ (φ \land 0 \in (0 \dots N)) \to C (0) : X ⟶ ℂ$
732	12 117 731	syl2anc	$⊢ φ \to C (0) : X ⟶ ℂ$
733	732	adantr	$⊢ (φ \land i \in (0 ..^N)) \to C (0) : X ⟶ ℂ$
734	733	ffvelrnda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (0) (x) \in ℂ$
735	473 650	nffv	$⊢ \underline{Ⅎ} k D (i + 1)$
736	735 360 361	nff	$⊢ Ⅎ k D (i + 1) : X ⟶ ℂ$
737	649 736	nfim	$⊢ Ⅎ k ((φ \land i + 1 \in (0 \dots N)) \to D (i + 1) : X ⟶ ℂ)$
738		fveq2	$⊢ k = i + 1 \to D (k) = D (i + 1)$
739	738	feq1d	$⊢ k = i + 1 \to (D (k) : X ⟶ ℂ \leftrightarrow D (i + 1) : X ⟶ ℂ)$
740	656 739	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 ⟶ ℂ))$
741	737 654 740 601	vtoclf	$⊢ (φ \land i + 1 \in (0 \dots N)) \to D (i + 1) : X ⟶ ℂ$
742	646 648 741	syl2anc	$⊢ (φ \land i \in (0 ..^N)) \to D (i + 1) : X ⟶ ℂ$
743	742	ffvelrnda	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (i + 1) (x) \in ℂ$
744	734 743	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (0) (x) D (i + 1) (x) \in ℂ$
745	744	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)$
746	726 745	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)$
747		nfv	$⊢ Ⅎ j i \in (0 ..^N)$
748		1zzd	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to 1 \in ℤ$
749	237	adantr	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to i \in ℤ$
750		eldifi	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in (0 \dots i)$
751		elfzelz	$⊢ j \in (0 \dots i) \to j \in ℤ$
752	750 751	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in ℤ$
753	752	adantl	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to j \in ℤ$
754	748 749 753	3jca	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to (1 \in ℤ \land i \in ℤ \land j \in ℤ)$
755		elfznn0	$⊢ j \in (0 \dots i) \to j \in ℕ_{0}$
756	750 755	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in ℕ_{0}$
757		eldifsni	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \neq 0$
758	756 757	jca	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to (j \in ℕ_{0} \land j \neq 0)$
759		elnnne0	$⊢ j \in ℕ \leftrightarrow (j \in ℕ_{0} \land j \neq 0)$
760	758 759	sylibr	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \in ℕ$
761		nnge1	$⊢ j \in ℕ \to 1 \leq j$
762	760 761	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to 1 \leq j$
763	762	adantl	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to 1 \leq j$
764		elfzle2	$⊢ j \in (0 \dots i) \to j \leq i$
765	750 764	syl	$⊢ j \in ((0 \dots i) ∖ \{0\}) \to j \leq i$
766	765	adantl	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to j \leq i$
767	754 763 766	jca32	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to ((1 \in ℤ \land i \in ℤ \land j \in ℤ) \land (1 \leq j \land j \leq i))$
768		elfz2	$⊢ j \in (1 \dots i) \leftrightarrow ((1 \in ℤ \land i \in ℤ \land j \in ℤ) \land (1 \leq j \land j \leq i))$
769	767 768	sylibr	$⊢ (i \in (0 ..^N) \land j \in ((0 \dots i) ∖ \{0\})) \to j \in (1 \dots i)$
770	769	ex	$⊢ i \in (0 ..^N) \to (j \in ((0 \dots i) ∖ \{0\}) \to j \in (1 \dots i))$
771		0zd	$⊢ j \in (1 \dots i) \to 0 \in ℤ$
772		elfzel2	$⊢ j \in (1 \dots i) \to i \in ℤ$
773		elfzelz	$⊢ j \in (1 \dots i) \to j \in ℤ$
774	771 772 773	3jca	$⊢ j \in (1 \dots i) \to (0 \in ℤ \land i \in ℤ \land j \in ℤ)$
775	173	a1i	$⊢ j \in (1 \dots i) \to 0 \in ℝ$
776	773	zred	$⊢ j \in (1 \dots i) \to j \in ℝ$
777		1red	$⊢ j \in (1 \dots i) \to 1 \in ℝ$
778	545	a1i	$⊢ j \in (1 \dots i) \to 0 < 1$
779		elfzle1	$⊢ j \in (1 \dots i) \to 1 \leq j$
780	775 777 776 778 779	ltletrd	$⊢ j \in (1 \dots i) \to 0 < j$
781	775 776 780	ltled	$⊢ j \in (1 \dots i) \to 0 \leq j$
782		elfzle2	$⊢ j \in (1 \dots i) \to j \leq i$
783	774 781 782	jca32	$⊢ j \in (1 \dots i) \to ((0 \in ℤ \land i \in ℤ \land j \in ℤ) \land (0 \leq j \land j \leq i))$
784		elfz2	$⊢ j \in (0 \dots i) \leftrightarrow ((0 \in ℤ \land i \in ℤ \land j \in ℤ) \land (0 \leq j \land j \leq i))$
785	783 784	sylibr	$⊢ j \in (1 \dots i) \to j \in (0 \dots i)$
786	775 780	gtned	$⊢ j \in (1 \dots i) \to j \neq 0$
787		nelsn	$⊢ j \neq 0 \to \neg j \in \{0\}$
788	786 787	syl	$⊢ j \in (1 \dots i) \to \neg j \in \{0\}$
789	785 788	eldifd	$⊢ j \in (1 \dots i) \to j \in ((0 \dots i) ∖ \{0\})$
790	789	adantl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to j \in ((0 \dots i) ∖ \{0\})$
791	790	ex	$⊢ i \in (0 ..^N) \to (j \in (1 \dots i) \to j \in ((0 \dots i) ∖ \{0\}))$
792	770 791	impbid	$⊢ i \in (0 ..^N) \to (j \in ((0 \dots i) ∖ \{0\}) \leftrightarrow j \in (1 \dots i))$
793	747 792	alrimi	$⊢ i \in (0 ..^N) \to \forall j (j \in ((0 \dots i) ∖ \{0\}) \leftrightarrow j \in (1 \dots i))$
794		dfcleq	$⊢ (0 \dots i) ∖ \{0\} = (1 \dots i) \leftrightarrow \forall j (j \in ((0 \dots i) ∖ \{0\}) \leftrightarrow j \in (1 \dots i))$
795	793 794	sylibr	$⊢ i \in (0 ..^N) \to (0 \dots i) ∖ \{0\} = (1 \dots i)$
796	795	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)$
797	796	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)$
798	746 797	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)$
799	715 722 798	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)$
800	694 799	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)$
801		fzfid	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (1 \dots i) \in Fin$
802	187	adantr	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to i \in ℕ_{0}$
803	790 752	syl	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to j \in ℤ$
804		1zzd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to 1 \in ℤ$
805	803 804	zsubcld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to j - 1 \in ℤ$
806	802 805	bccld	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℕ_{0}$
807	806	nn0cnd	$⊢ (i \in (0 ..^N) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℂ$
808	807	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℂ$
809	808	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to (\binom{i}{j - 1}) \in ℂ$
810		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)$
811		fzelp1	$⊢ j \in (1 \dots i) \to j \in (1 \dots i + 1)$
812	811	adantl	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to j \in (1 \dots i + 1)$
813	810 812 567	syl2anc	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to C (j) (x) \in ℂ$
814	812 605	syldan	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land j \in (1 \dots i)) \to D (i + 1 - j) (x) \in ℂ$
815	813 814	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 ℂ$
816	809 815	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 ℂ$
817	801 816	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 ℂ$
818	187	adantr	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to i \in ℕ_{0}$
819		elfzelz	$⊢ k \in (1 \dots i) \to k \in ℤ$
820	819	adantl	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to k \in ℤ$
821	818 820	bccld	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℕ_{0}$
822	821	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℂ$
823	822	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℂ$
824	823	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i}{k}) \in ℂ$
825		simpll	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (φ \land i \in (0 ..^N))$
826		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to x \in X$
827	785	ssriv	$⊢ (1 \dots i) \subseteq (0 \dots i)$
828		id	$⊢ k \in (1 \dots i) \to k \in (1 \dots i)$
829	827 828	sseldi	$⊢ k \in (1 \dots i) \to k \in (0 \dots i)$
830	829	adantl	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to k \in (0 \dots i)$
831	825 826 830 445	syl21anc	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to C (k) (x) \in ℂ$
832	830 447	syldan	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to D (i + 1 - k) (x) \in ℂ$
833	831 832	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 ℂ$
834	824 833	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 ℂ$
835	801 834	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 ℂ$
836	678 817 744 835	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)$
837		oveq1	$⊢ j = k \to j - 1 = k - 1$
838	837	oveq2d	$⊢ j = k \to (\binom{i}{j - 1}) = (\binom{i}{k - 1})$
839		fveq2	$⊢ j = k \to C (j) = C (k)$
840	839	fveq1d	$⊢ j = k \to C (j) (x) = C (k) (x)$
841		oveq2	$⊢ j = k \to i + 1 - j = i + 1 - k$
842	841	fveq2d	$⊢ j = k \to D (i + 1 - j) = D (i + 1 - k)$
843	842	fveq1d	$⊢ j = k \to D (i + 1 - j) (x) = D (i + 1 - k) (x)$
844	840 843	oveq12d	$⊢ j = k \to C (j) (x) D (i + 1 - j) (x) = C (k) (x) D (i + 1 - k) (x)$
845	838 844	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)$
846		nfcv	$⊢ \underline{Ⅎ} k (1 \dots i)$
847		nfcv	$⊢ \underline{Ⅎ} j (1 \dots i)$
848		nfcv	$⊢ \underline{Ⅎ} k (\binom{i}{j - 1})$
849	359 470	nffv	$⊢ \underline{Ⅎ} k C (j) (x)$
850	588 470	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - j) (x)$
851	849 467 850	nfov	$⊢ \underline{Ⅎ} k C (j) (x) D (i + 1 - j) (x)$
852	848 467 851	nfov	$⊢ \underline{Ⅎ} k (\binom{i}{j - 1}) C (j) (x) D (i + 1 - j) (x)$
853		nfcv	$⊢ \underline{Ⅎ} j (\binom{i}{k - 1}) C (k) (x) D (i + 1 - k) (x)$
854	845 846 847 852 853	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)$
855	854	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)$
856	855	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)$
857		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
858	820 857	syl	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to k - 1 \in ℤ$
859	818 858	bccld	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℕ_{0}$
860	859	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℂ$
861	860	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℂ$
862	861	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i}{k - 1}) \in ℂ$
863	862 833	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 ℂ$
864	801 863 834	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)$
865	864	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))$
866	860 822	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})$
867		bcpasc	$⊢ (i \in ℕ_{0} \land k \in ℤ) \to (\binom{i}{k}) + (\binom{i}{k - 1}) = (\binom{i + 1}{k})$
868	818 820 867	syl2anc	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i}{k}) + (\binom{i}{k - 1}) = (\binom{i + 1}{k})$
869	866 868	eqtr2d	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) = (\binom{i}{k - 1}) + (\binom{i}{k})$
870	869	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)$
871	870	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)$
872	871	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)$
873	862 824 833	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)$
874	872 873	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)$
875	874	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)$
876	856 865 875	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)$
877	876	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)$
878		peano2nn0	$⊢ i \in ℕ_{0} \to i + 1 \in ℕ_{0}$
879	818 878	syl	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to i + 1 \in ℕ_{0}$
880	879 820	bccld	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℕ_{0}$
881	880	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
882	881	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
883	882	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (1 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
884	883 833	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 ℂ$
885	801 884	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 ℂ$
886	678 744 885	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)$
887	187 878	syl	$⊢ i \in (0 ..^N) \to i + 1 \in ℕ_{0}$
888		bcn0	$⊢ i + 1 \in ℕ_{0} \to (\binom{i + 1}{0}) = 1$
889	887 888	syl	$⊢ i \in (0 ..^N) \to (\binom{i + 1}{0}) = 1$
890	889 719	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)$
891	890	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)$
892	891 745	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)$
893	795	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (0 \dots i) ∖ \{0\} = (1 \dots i)$
894	893	eqcomd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (1 \dots i) = (0 \dots i) ∖ \{0\}$
895	894	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)$
896	892 895	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)$
897		nfcv	$⊢ \underline{Ⅎ} k (\binom{i + 1}{0})$
898	897 467 701	nfov	$⊢ \underline{Ⅎ} k (\binom{i + 1}{0}) C (0) (x) D (i + 1 - 0) (x)$
899	199 878	syl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to i + 1 \in ℕ_{0}$
900	899 201	bccld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℕ_{0}$
901	900	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
902	901	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
903	902	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i)) \to (\binom{i + 1}{k}) \in ℂ$
904	903 448	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 ℂ$
905		oveq2	$⊢ k = 0 \to (\binom{i + 1}{k}) = (\binom{i + 1}{0})$
906	905 713	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)$
907	484 898 451 904 707 906	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)$
908	907	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)$
909	896 908	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)$
910	909	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)$
911		bcnn	$⊢ i + 1 \in ℕ_{0} \to (\binom{i + 1}{i + 1}) = 1$
912	887 911	syl	$⊢ i \in (0 ..^N) \to (\binom{i + 1}{i + 1}) = 1$
913	912	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (\binom{i + 1}{i + 1}) = 1$
914	913	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)$
915	641	adantl	$⊢ (φ \land i \in (0 ..^N)) \to D (i + 1 - (i + 1)) = D (0)$
916	915	feq1d	$⊢ (φ \land i \in (0 ..^N)) \to (D (i + 1 - (i + 1)) : X ⟶ ℂ \leftrightarrow D (0) : X ⟶ ℂ)$
917	676 916	mpbird	$⊢ (φ \land i \in (0 ..^N)) \to D (i + 1 - (i + 1)) : X ⟶ ℂ$
918	917	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (i + 1 - (i + 1)) : X ⟶ ℂ$
919		simpr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to x \in X$
920	918 919	ffvelrnd	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to D (i + 1 - (i + 1)) (x) \in ℂ$
921	662 920	mulcld	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to C (i + 1) (x) D (i + 1 - (i + 1)) (x) \in ℂ$
922	921	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)$
923	643	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)$
924	914 922 923	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)$
925		fzdifsuc	$⊢ i \in ℤ_{\geq 0} \to (0 \dots i) = (0 \dots i + 1) ∖ \{i + 1\}$
926	704 925	syl	$⊢ i \in (0 ..^N) \to (0 \dots i) = (0 \dots i + 1) ∖ \{i + 1\}$
927	926	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)$
928	927	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)$
929	924 928	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)$
930		nfcv	$⊢ \underline{Ⅎ} k (\binom{i + 1}{i + 1})$
931	651 470	nffv	$⊢ \underline{Ⅎ} k C (i + 1) (x)$
932		nfcv	$⊢ \underline{Ⅎ} k (i + 1 - (i + 1))$
933	473 932	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - (i + 1))$
934	933 470	nffv	$⊢ \underline{Ⅎ} k D (i + 1 - (i + 1)) (x)$
935	931 467 934	nfov	$⊢ \underline{Ⅎ} k C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
936	930 467 935	nfov	$⊢ \underline{Ⅎ} k (\binom{i + 1}{i + 1}) C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
937		fzfid	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to (0 \dots i + 1) \in Fin$
938	887	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \in ℕ_{0}$
939		elfzelz	$⊢ k \in (0 \dots i + 1) \to k \in ℤ$
940	939	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \in ℤ$
941	938 940	bccld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℕ_{0}$
942	941	nn0cnd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℂ$
943	942	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℂ$
944	943	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to (\binom{i + 1}{k}) \in ℂ$
945	646	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to φ$
946	96	a1i	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \in ℤ$
947	208	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N \in ℤ$
948	946 947 940	3jca	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (0 \in ℤ \land N \in ℤ \land k \in ℤ)$
949		elfzle1	$⊢ k \in (0 \dots i + 1) \to 0 \leq k$
950	949	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \leq k$
951	940	zred	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \in ℝ$
952	938	nn0red	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \in ℝ$
953	214	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N \in ℝ$
954		elfzle2	$⊢ k \in (0 \dots i + 1) \to k \leq i + 1$
955	954	adantl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \leq i + 1$
956	308	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \leq N$
957	951 952 953 955 956	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \leq N$
958	948 950 957	jca32	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to ((0 \in ℤ \land N \in ℤ \land k \in ℤ) \land (0 \leq k \land k \leq N))$
959	958 225	sylibr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to k \in (0 \dots N)$
960	959	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to k \in (0 \dots N)$
961	945 960 232	syl2anc	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to C (k) : X ⟶ ℂ$
962	961	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to C (k) : X ⟶ ℂ$
963		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to x \in X$
964	962 963	ffvelrnd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to C (k) (x) \in ℂ$
965	945	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to φ$
966	609	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 \in ℤ$
967	966 940	zsubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \in ℤ$
968	946 947 967	3jca	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (0 \in ℤ \land N \in ℤ \land i + 1 - k \in ℤ)$
969	952 951	subge0d	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to (0 \leq i + 1 - k \leftrightarrow k \leq i + 1)$
970	955 969	mpbird	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \leq i + 1 - k$
971	952 951	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \in ℝ$
972	953 951	resubcld	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - k \in ℝ$
973	953 173 251	sylancl	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - 0 \in ℝ$
974	952 953 951 956	lesub1dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \leq N - k$
975	173	a1i	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to 0 \in ℝ$
976	975 951 953 950	lesub2dd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - k \leq N - 0$
977	971 972 973 974 976	letrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \leq N - 0$
978	257	adantr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to N - 0 = N$
979	977 978	breqtrd	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \leq N$
980	968 970 979	jca32	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to ((0 \in ℤ \land N \in ℤ \land i + 1 - k \in ℤ) \land (0 \leq i + 1 - k \land i + 1 - k \leq N))$
981	980 314	sylibr	$⊢ (i \in (0 ..^N) \land k \in (0 \dots i + 1)) \to i + 1 - k \in (0 \dots N)$
982	981	adantll	$⊢ ((φ \land i \in (0 ..^N)) \land k \in (0 \dots i + 1)) \to i + 1 - k \in (0 \dots N)$
983	982	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)$
984		fveq2	$⊢ j = i + 1 - k \to D (j) = D (i + 1 - k)$
985	984	feq1d	$⊢ j = i + 1 - k \to (D (j) : X ⟶ ℂ \leftrightarrow D (i + 1 - k) : X ⟶ ℂ)$
986	319 985	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 ⟶ ℂ))$
987	473 358	nffv	$⊢ \underline{Ⅎ} k D (j)$
988	987 360 361	nff	$⊢ Ⅎ k D (j) : X ⟶ ℂ$
989	355 988	nfim	$⊢ Ⅎ k ((φ \land j \in (0 \dots N)) \to D (j) : X ⟶ ℂ)$
990		fveq2	$⊢ k = j \to D (k) = D (j)$
991	990	feq1d	$⊢ k = j \to (D (k) : X ⟶ ℂ \leftrightarrow D (j) : X ⟶ ℂ)$
992	273 991	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 ⟶ ℂ))$
993	989 992 601	chvarfv	$⊢ (φ \land j \in (0 \dots N)) \to D (j) : X ⟶ ℂ$
994	317 986 993	vtocl	$⊢ (φ \land i + 1 - k \in (0 \dots N)) \to D (i + 1 - k) : X ⟶ ℂ$
995	965 983 994	syl2anc	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to D (i + 1 - k) : X ⟶ ℂ$
996	995 963	ffvelrnd	$⊢ (((φ \land i \in (0 ..^N)) \land x \in X) \land k \in (0 \dots i + 1)) \to D (i + 1 - k) (x) \in ℂ$
997	964 996	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 ℂ$
998	944 997	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 ℂ$
999	887 703	eleqtrrd	$⊢ i \in (0 ..^N) \to i + 1 \in ℤ_{\geq 0}$
1000		eluzfz2	$⊢ i + 1 \in ℤ_{\geq 0} \to i + 1 \in (0 \dots i + 1)$
1001	999 1000	syl	$⊢ i \in (0 ..^N) \to i + 1 \in (0 \dots i + 1)$
1002	1001	ad2antlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in X) \to i + 1 \in (0 \dots i + 1)$
1003		oveq2	$⊢ k = i + 1 \to (\binom{i + 1}{k}) = (\binom{i + 1}{i + 1})$
1004	657	fveq1d	$⊢ k = i + 1 \to C (k) (x) = C (i + 1) (x)$
1005		oveq2	$⊢ k = i + 1 \to i + 1 - k = i + 1 - (i + 1)$
1006	1005	fveq2d	$⊢ k = i + 1 \to D (i + 1 - k) = D (i + 1 - (i + 1))$
1007	1006	fveq1d	$⊢ k = i + 1 \to D (i + 1 - k) (x) = D (i + 1 - (i + 1)) (x)$
1008	1004 1007	oveq12d	$⊢ k = i + 1 \to C (k) (x) D (i + 1 - k) (x) = C (i + 1) (x) D (i + 1 - (i + 1)) (x)$
1009	1003 1008	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)$
1010	484 936 937 998 1002 1009	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)$
1011	1010	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)$
1012	910 929 1011	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)$
1013	877 886 1012	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)$
1014	800 836 1013	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)$
1015	450 454 1014	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)$
1016	1015	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))$
1017	434 1016	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))$
1018	1017	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))$
1019	191 193 1018	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))$
1020	180 181 184 1019	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))$
1021	1020	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))))$
1022	44 57 70 83 179 1021	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)))$
1023	31 1022	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))))$
1024	5 16 1023	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)))$
1025	12 1024	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