etransclem35

Description: P does not divide the P-1 -th derivative of F applied to 0 . This is case 2 of the proof in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem35.p	$⊢ φ \to P \in ℕ$
	etransclem35.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem35.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem35.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
	etransclem35.d	$⊢ D = (j \in (0 \dots M) ⟼ if (j = 0, P - 1, 0))$
Assertion	etransclem35	$⊢ φ \to (ℝ D^{n} F) (P - 1) (0) = (P - 1)! {\prod_{j = 1}^{M} (- j)}^{P}$

Proof

Step	Hyp	Ref	Expression
1		etransclem35.p	$⊢ φ \to P \in ℕ$
2		etransclem35.m	$⊢ φ \to M \in ℕ_{0}$
3		etransclem35.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
4		etransclem35.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
5		etransclem35.d	$⊢ D = (j \in (0 \dots M) ⟼ if (j = 0, P - 1, 0))$
6		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
7	6	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
8		reopn	$⊢ ℝ \in topGen (ran (.))$
9		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
10	9	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
11	8 10	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
12	11	a1i	$⊢ φ \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
13		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
14	1 13	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
15		etransclem5	$⊢ (k \in (0 \dots M) ⟼ (y \in ℝ ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) = (j \in (0 \dots M) ⟼ (x \in ℝ ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
16		0red	$⊢ φ \to 0 \in ℝ$
17	7 12 1 2 3 14 15 4 16	etransclem31	$⊢ φ \to (ℝ D^{n} F) (P - 1) (0) = \sum_{c \in C (P - 1)} (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)})$
18		nfv	$⊢ Ⅎ c φ$
19		nfcv	$⊢ \underline{Ⅎ} c (\frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)})$
20	4 14	etransclem16	$⊢ φ \to C (P - 1) \in Fin$
21		simpr	$⊢ (φ \land c \in C (P - 1)) \to c \in C (P - 1)$
22	4 14	etransclem12	$⊢ φ \to C (P - 1) = \{c \in ({(0 \dots P - 1)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = P - 1\}$
23	22	adantr	$⊢ (φ \land c \in C (P - 1)) \to C (P - 1) = \{c \in ({(0 \dots P - 1)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = P - 1\}$
24	21 23	eleqtrd	$⊢ (φ \land c \in C (P - 1)) \to c \in \{c \in ({(0 \dots P - 1)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = P - 1\}$
25		rabid	$⊢ c \in \{c \in ({(0 \dots P - 1)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = P - 1\} \leftrightarrow (c \in ({(0 \dots P - 1)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} c (j) = P - 1)$
26	24 25	sylib	$⊢ (φ \land c \in C (P - 1)) \to (c \in ({(0 \dots P - 1)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} c (j) = P - 1)$
27	26	simprd	$⊢ (φ \land c \in C (P - 1)) \to \sum_{j = 0}^{M} c (j) = P - 1$
28	27	eqcomd	$⊢ (φ \land c \in C (P - 1)) \to P - 1 = \sum_{j = 0}^{M} c (j)$
29	28	fveq2d	$⊢ (φ \land c \in C (P - 1)) \to (P - 1)! = \sum_{j = 0}^{M} c (j)!$
30	29	oveq1d	$⊢ (φ \land c \in C (P - 1)) \to \frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!} = \frac{\sum_{j = 0}^{M} c (j)!}{\prod_{j = 0}^{M} c (j)!}$
31		nfcv	$⊢ \underline{Ⅎ} j c$
32		fzfid	$⊢ (φ \land c \in C (P - 1)) \to (0 \dots M) \in Fin$
33		nn0ex	$⊢ ℕ_{0} \in V$
34		fzssnn0	$⊢ (0 \dots P - 1) \subseteq ℕ_{0}$
35		mapss	$⊢ (ℕ_{0} \in V \land (0 \dots P - 1) \subseteq ℕ_{0}) \to {(0 \dots P - 1)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
36	33 34 35	mp2an	$⊢ {(0 \dots P - 1)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
37	26	simpld	$⊢ (φ \land c \in C (P - 1)) \to c \in ({(0 \dots P - 1)}^{(0 \dots M)})$
38	36 37	sseldi	$⊢ (φ \land c \in C (P - 1)) \to c \in ({ℕ_{0}}^{(0 \dots M)})$
39	31 32 38	mccl	$⊢ (φ \land c \in C (P - 1)) \to \frac{\sum_{j = 0}^{M} c (j)!}{\prod_{j = 0}^{M} c (j)!} \in ℕ$
40	30 39	eqeltrd	$⊢ (φ \land c \in C (P - 1)) \to \frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!} \in ℕ$
41	40	nnzd	$⊢ (φ \land c \in C (P - 1)) \to \frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!} \in ℤ$
42	1	adantr	$⊢ (φ \land c \in C (P - 1)) \to P \in ℕ$
43	2	adantr	$⊢ (φ \land c \in C (P - 1)) \to M \in ℕ_{0}$
44		elmapi	$⊢ c \in ({(0 \dots P - 1)}^{(0 \dots M)}) \to c : (0 \dots M) ⟶ (0 \dots P - 1)$
45	37 44	syl	$⊢ (φ \land c \in C (P - 1)) \to c : (0 \dots M) ⟶ (0 \dots P - 1)$
46		0zd	$⊢ (φ \land c \in C (P - 1)) \to 0 \in ℤ$
47	42 43 45 46	etransclem10	$⊢ (φ \land c \in C (P - 1)) \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \in ℤ$
48		fzfid	$⊢ (φ \land c \in C (P - 1)) \to (1 \dots M) \in Fin$
49	1	ad2antrr	$⊢ ((φ \land c \in C (P - 1)) \land j \in (1 \dots M)) \to P \in ℕ$
50	45	adantr	$⊢ ((φ \land c \in C (P - 1)) \land j \in (1 \dots M)) \to c : (0 \dots M) ⟶ (0 \dots P - 1)$
51		fz1ssfz0	$⊢ (1 \dots M) \subseteq (0 \dots M)$
52	51	sseli	$⊢ j \in (1 \dots M) \to j \in (0 \dots M)$
53	52	adantl	$⊢ ((φ \land c \in C (P - 1)) \land j \in (1 \dots M)) \to j \in (0 \dots M)$
54		0zd	$⊢ ((φ \land c \in C (P - 1)) \land j \in (1 \dots M)) \to 0 \in ℤ$
55	49 50 53 54	etransclem3	$⊢ ((φ \land c \in C (P - 1)) \land j \in (1 \dots M)) \to if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) \in ℤ$
56	48 55	fprodzcl	$⊢ (φ \land c \in C (P - 1)) \to \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) \in ℤ$
57	47 56	zmulcld	$⊢ (φ \land c \in C (P - 1)) \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) \in ℤ$
58	41 57	zmulcld	$⊢ (φ \land c \in C (P - 1)) \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) \in ℤ$
59	58	zcnd	$⊢ (φ \land c \in C (P - 1)) \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) \in ℂ$
60		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
61	14 60	eleqtrdi	$⊢ φ \to P - 1 \in ℤ_{\geq 0}$
62		eluzfz2	$⊢ P - 1 \in ℤ_{\geq 0} \to P - 1 \in (0 \dots P - 1)$
63	61 62	syl	$⊢ φ \to P - 1 \in (0 \dots P - 1)$
64		eluzfz1	$⊢ P - 1 \in ℤ_{\geq 0} \to 0 \in (0 \dots P - 1)$
65	61 64	syl	$⊢ φ \to 0 \in (0 \dots P - 1)$
66	63 65	ifcld	$⊢ φ \to if (j = 0, P - 1, 0) \in (0 \dots P - 1)$
67	66	adantr	$⊢ (φ \land j \in (0 \dots M)) \to if (j = 0, P - 1, 0) \in (0 \dots P - 1)$
68	67 5	fmptd	$⊢ φ \to D : (0 \dots M) ⟶ (0 \dots P - 1)$
69		ovex	$⊢ (0 \dots P - 1) \in V$
70		ovex	$⊢ (0 \dots M) \in V$
71	69 70	elmap	$⊢ D \in ({(0 \dots P - 1)}^{(0 \dots M)}) \leftrightarrow D : (0 \dots M) ⟶ (0 \dots P - 1)$
72	68 71	sylibr	$⊢ φ \to D \in ({(0 \dots P - 1)}^{(0 \dots M)})$
73	2 60	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
74		fzsscn	$⊢ (0 \dots P - 1) \subseteq ℂ$
75	68	ffvelrnda	$⊢ (φ \land j \in (0 \dots M)) \to D (j) \in (0 \dots P - 1)$
76	74 75	sseldi	$⊢ (φ \land j \in (0 \dots M)) \to D (j) \in ℂ$
77		fveq2	$⊢ j = 0 \to D (j) = D (0)$
78	73 76 77	fsum1p	$⊢ φ \to \sum_{j = 0}^{M} D (j) = D (0) + \sum_{j = 0 + 1}^{M} D (j)$
79	5	a1i	$⊢ φ \to D = (j \in (0 \dots M) ⟼ if (j = 0, P - 1, 0))$
80		simpr	$⊢ (φ \land j = 0) \to j = 0$
81	80	iftrued	$⊢ (φ \land j = 0) \to if (j = 0, P - 1, 0) = P - 1$
82		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
83	73 82	syl	$⊢ φ \to 0 \in (0 \dots M)$
84	79 81 83 14	fvmptd	$⊢ φ \to D (0) = P - 1$
85		0p1e1	$⊢ 0 + 1 = 1$
86	85	oveq1i	$⊢ (0 + 1 \dots M) = (1 \dots M)$
87	86	sumeq1i	$⊢ \sum_{j = 0 + 1}^{M} D (j) = \sum_{j = 1}^{M} D (j)$
88	87	a1i	$⊢ φ \to \sum_{j = 0 + 1}^{M} D (j) = \sum_{j = 1}^{M} D (j)$
89	5	fvmpt2	$⊢ (j \in (0 \dots M) \land if (j = 0, P - 1, 0) \in (0 \dots P - 1)) \to D (j) = if (j = 0, P - 1, 0)$
90	52 66 89	syl2anr	$⊢ (φ \land j \in (1 \dots M)) \to D (j) = if (j = 0, P - 1, 0)$
91		0red	$⊢ j \in (1 \dots M) \to 0 \in ℝ$
92		1red	$⊢ j \in (1 \dots M) \to 1 \in ℝ$
93		elfzelz	$⊢ j \in (1 \dots M) \to j \in ℤ$
94	93	zred	$⊢ j \in (1 \dots M) \to j \in ℝ$
95		0lt1	$⊢ 0 < 1$
96	95	a1i	$⊢ j \in (1 \dots M) \to 0 < 1$
97		elfzle1	$⊢ j \in (1 \dots M) \to 1 \leq j$
98	91 92 94 96 97	ltletrd	$⊢ j \in (1 \dots M) \to 0 < j$
99	91 98	gtned	$⊢ j \in (1 \dots M) \to j \neq 0$
100	99	neneqd	$⊢ j \in (1 \dots M) \to \neg j = 0$
101	100	iffalsed	$⊢ j \in (1 \dots M) \to if (j = 0, P - 1, 0) = 0$
102	101	adantl	$⊢ (φ \land j \in (1 \dots M)) \to if (j = 0, P - 1, 0) = 0$
103	90 102	eqtrd	$⊢ (φ \land j \in (1 \dots M)) \to D (j) = 0$
104	103	sumeq2dv	$⊢ φ \to \sum_{j = 1}^{M} D (j) = \sum_{j = 1}^{M} 0$
105		fzfi	$⊢ (1 \dots M) \in Fin$
106	105	olci	$⊢ ((1 \dots M) \subseteq ℤ_{\geq A} \lor (1 \dots M) \in Fin)$
107		sumz	$⊢ ((1 \dots M) \subseteq ℤ_{\geq A} \lor (1 \dots M) \in Fin) \to \sum_{j = 1}^{M} 0 = 0$
108	106 107	mp1i	$⊢ φ \to \sum_{j = 1}^{M} 0 = 0$
109	88 104 108	3eqtrd	$⊢ φ \to \sum_{j = 0 + 1}^{M} D (j) = 0$
110	84 109	oveq12d	$⊢ φ \to D (0) + \sum_{j = 0 + 1}^{M} D (j) = P - 1 + 0$
111	1	nncnd	$⊢ φ \to P \in ℂ$
112		1cnd	$⊢ φ \to 1 \in ℂ$
113	111 112	subcld	$⊢ φ \to P - 1 \in ℂ$
114	113	addid1d	$⊢ φ \to P - 1 + 0 = P - 1$
115	78 110 114	3eqtrd	$⊢ φ \to \sum_{j = 0}^{M} D (j) = P - 1$
116		fveq1	$⊢ c = D \to c (j) = D (j)$
117	116	sumeq2sdv	$⊢ c = D \to \sum_{j = 0}^{M} c (j) = \sum_{j = 0}^{M} D (j)$
118	117	eqeq1d	$⊢ c = D \to (\sum_{j = 0}^{M} c (j) = P - 1 \leftrightarrow \sum_{j = 0}^{M} D (j) = P - 1)$
119	118	elrab	$⊢ D \in \{c \in ({(0 \dots P - 1)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = P - 1\} \leftrightarrow (D \in ({(0 \dots P - 1)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} D (j) = P - 1)$
120	72 115 119	sylanbrc	$⊢ φ \to D \in \{c \in ({(0 \dots P - 1)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = P - 1\}$
121	120 22	eleqtrrd	$⊢ φ \to D \in C (P - 1)$
122	116	fveq2d	$⊢ c = D \to c (j)! = D (j)!$
123	122	prodeq2ad	$⊢ c = D \to \prod_{j = 0}^{M} c (j)! = \prod_{j = 0}^{M} D (j)!$
124	123	oveq2d	$⊢ c = D \to \frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!} = \frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!}$
125		fveq1	$⊢ c = D \to c (0) = D (0)$
126	125	breq2d	$⊢ c = D \to (P - 1 < c (0) \leftrightarrow P - 1 < D (0))$
127	125	oveq2d	$⊢ c = D \to P - 1 - c (0) = P - 1 - D (0)$
128	127	fveq2d	$⊢ c = D \to (P - 1 - c (0))! = (P - 1 - D (0))!$
129	128	oveq2d	$⊢ c = D \to \frac{(P - 1)!}{(P - 1 - c (0))!} = \frac{(P - 1)!}{(P - 1 - D (0))!}$
130	127	oveq2d	$⊢ c = D \to 0^{P - 1 - c (0)} = 0^{P - 1 - D (0)}$
131	129 130	oveq12d	$⊢ c = D \to (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)} = (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}$
132	126 131	ifbieq2d	$⊢ c = D \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) = if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)})$
133	116	breq2d	$⊢ c = D \to (P < c (j) \leftrightarrow P < D (j))$
134	116	oveq2d	$⊢ c = D \to P - c (j) = P - D (j)$
135	134	fveq2d	$⊢ c = D \to (P - c (j))! = (P - D (j))!$
136	135	oveq2d	$⊢ c = D \to \frac{P!}{(P - c (j))!} = \frac{P!}{(P - D (j))!}$
137	134	oveq2d	$⊢ c = D \to {(0 - j)}^{P - c (j)} = {(0 - j)}^{P - D (j)}$
138	136 137	oveq12d	$⊢ c = D \to (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)} = (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}$
139	133 138	ifbieq2d	$⊢ c = D \to if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)})$
140	139	prodeq2ad	$⊢ c = D \to \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)})$
141	132 140	oveq12d	$⊢ c = D \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)})$
142	124 141	oveq12d	$⊢ c = D \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = (\frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)})$
143	18 19 20 59 121 142	fsumsplit1	$⊢ φ \to \sum_{c \in C (P - 1)} (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = (\frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}) + \sum_{c \in C (P - 1) ∖ \{D\}} (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)})$
144	34 75	sseldi	$⊢ (φ \land j \in (0 \dots M)) \to D (j) \in ℕ_{0}$
145	144	faccld	$⊢ (φ \land j \in (0 \dots M)) \to D (j)! \in ℕ$
146	145	nncnd	$⊢ (φ \land j \in (0 \dots M)) \to D (j)! \in ℂ$
147	77	fveq2d	$⊢ j = 0 \to D (j)! = D (0)!$
148	73 146 147	fprod1p	$⊢ φ \to \prod_{j = 0}^{M} D (j)! = D (0)! \prod_{j = 0 + 1}^{M} D (j)!$
149	84	fveq2d	$⊢ φ \to D (0)! = (P - 1)!$
150	86	prodeq1i	$⊢ \prod_{j = 0 + 1}^{M} D (j)! = \prod_{j = 1}^{M} D (j)!$
151	150	a1i	$⊢ φ \to \prod_{j = 0 + 1}^{M} D (j)! = \prod_{j = 1}^{M} D (j)!$
152	103	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to D (j)! = 0!$
153		fac0	$⊢ 0! = 1$
154	152 153	eqtrdi	$⊢ (φ \land j \in (1 \dots M)) \to D (j)! = 1$
155	154	prodeq2dv	$⊢ φ \to \prod_{j = 1}^{M} D (j)! = \prod_{j = 1}^{M} 1$
156		prod1	$⊢ ((1 \dots M) \subseteq ℤ_{\geq A} \lor (1 \dots M) \in Fin) \to \prod_{j = 1}^{M} 1 = 1$
157	106 156	mp1i	$⊢ φ \to \prod_{j = 1}^{M} 1 = 1$
158	151 155 157	3eqtrd	$⊢ φ \to \prod_{j = 0 + 1}^{M} D (j)! = 1$
159	149 158	oveq12d	$⊢ φ \to D (0)! \prod_{j = 0 + 1}^{M} D (j)! = (P - 1)! \cdot 1$
160	14	faccld	$⊢ φ \to (P - 1)! \in ℕ$
161	160	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
162	161	mulid1d	$⊢ φ \to (P - 1)! \cdot 1 = (P - 1)!$
163	148 159 162	3eqtrd	$⊢ φ \to \prod_{j = 0}^{M} D (j)! = (P - 1)!$
164	163	oveq2d	$⊢ φ \to \frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!} = \frac{(P - 1)!}{(P - 1)!}$
165	160	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
166	161 165	dividd	$⊢ φ \to \frac{(P - 1)!}{(P - 1)!} = 1$
167	164 166	eqtrd	$⊢ φ \to \frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!} = 1$
168	14	nn0red	$⊢ φ \to P - 1 \in ℝ$
169	84 168	eqeltrd	$⊢ φ \to D (0) \in ℝ$
170	169 168	lttri3d	$⊢ φ \to (D (0) = P - 1 \leftrightarrow (\neg D (0) < P - 1 \land \neg P - 1 < D (0)))$
171	84 170	mpbid	$⊢ φ \to (\neg D (0) < P - 1 \land \neg P - 1 < D (0))$
172	171	simprd	$⊢ φ \to \neg P - 1 < D (0)$
173	172	iffalsed	$⊢ φ \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) = (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}$
174	84	eqcomd	$⊢ φ \to P - 1 = D (0)$
175	113 174	subeq0bd	$⊢ φ \to P - 1 - D (0) = 0$
176	175	fveq2d	$⊢ φ \to (P - 1 - D (0))! = 0!$
177	176 153	eqtrdi	$⊢ φ \to (P - 1 - D (0))! = 1$
178	177	oveq2d	$⊢ φ \to \frac{(P - 1)!}{(P - 1 - D (0))!} = \frac{(P - 1)!}{1}$
179	161	div1d	$⊢ φ \to \frac{(P - 1)!}{1} = (P - 1)!$
180	178 179	eqtrd	$⊢ φ \to \frac{(P - 1)!}{(P - 1 - D (0))!} = (P - 1)!$
181	175	oveq2d	$⊢ φ \to 0^{P - 1 - D (0)} = 0^{0}$
182		0cnd	$⊢ φ \to 0 \in ℂ$
183	182	exp0d	$⊢ φ \to 0^{0} = 1$
184	181 183	eqtrd	$⊢ φ \to 0^{P - 1 - D (0)} = 1$
185	180 184	oveq12d	$⊢ φ \to (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)} = (P - 1)! \cdot 1$
186	173 185 162	3eqtrd	$⊢ φ \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) = (P - 1)!$
187		fzssre	$⊢ (0 \dots P - 1) \subseteq ℝ$
188	68	adantr	$⊢ (φ \land j \in (1 \dots M)) \to D : (0 \dots M) ⟶ (0 \dots P - 1)$
189	52	adantl	$⊢ (φ \land j \in (1 \dots M)) \to j \in (0 \dots M)$
190	188 189	ffvelrnd	$⊢ (φ \land j \in (1 \dots M)) \to D (j) \in (0 \dots P - 1)$
191	187 190	sseldi	$⊢ (φ \land j \in (1 \dots M)) \to D (j) \in ℝ$
192	1	nnred	$⊢ φ \to P \in ℝ$
193	192	adantr	$⊢ (φ \land j \in (1 \dots M)) \to P \in ℝ$
194	1	nngt0d	$⊢ φ \to 0 < P$
195	16 192 194	ltled	$⊢ φ \to 0 \leq P$
196	195	adantr	$⊢ (φ \land j \in (1 \dots M)) \to 0 \leq P$
197	103 196	eqbrtrd	$⊢ (φ \land j \in (1 \dots M)) \to D (j) \leq P$
198	191 193 197	lensymd	$⊢ (φ \land j \in (1 \dots M)) \to \neg P < D (j)$
199	198	iffalsed	$⊢ (φ \land j \in (1 \dots M)) \to if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}) = (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}$
200	103	oveq2d	$⊢ (φ \land j \in (1 \dots M)) \to P - D (j) = P - 0$
201	111	adantr	$⊢ (φ \land j \in (1 \dots M)) \to P \in ℂ$
202	201	subid1d	$⊢ (φ \land j \in (1 \dots M)) \to P - 0 = P$
203	200 202	eqtrd	$⊢ (φ \land j \in (1 \dots M)) \to P - D (j) = P$
204	203	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to (P - D (j))! = P!$
205	204	oveq2d	$⊢ (φ \land j \in (1 \dots M)) \to \frac{P!}{(P - D (j))!} = \frac{P!}{P!}$
206	1	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
207	206	faccld	$⊢ φ \to P! \in ℕ$
208	207	nncnd	$⊢ φ \to P! \in ℂ$
209	207	nnne0d	$⊢ φ \to P! \neq 0$
210	208 209	dividd	$⊢ φ \to \frac{P!}{P!} = 1$
211	210	adantr	$⊢ (φ \land j \in (1 \dots M)) \to \frac{P!}{P!} = 1$
212	205 211	eqtrd	$⊢ (φ \land j \in (1 \dots M)) \to \frac{P!}{(P - D (j))!} = 1$
213		df-neg	$⊢ - j = 0 - j$
214	213	eqcomi	$⊢ 0 - j = - j$
215	214	a1i	$⊢ (φ \land j \in (1 \dots M)) \to 0 - j = - j$
216	215 203	oveq12d	$⊢ (φ \land j \in (1 \dots M)) \to {(0 - j)}^{P - D (j)} = {(- j)}^{P}$
217	212 216	oveq12d	$⊢ (φ \land j \in (1 \dots M)) \to (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)} = 1 {(- j)}^{P}$
218	93	znegcld	$⊢ j \in (1 \dots M) \to - j \in ℤ$
219	218	zcnd	$⊢ j \in (1 \dots M) \to - j \in ℂ$
220	219	adantl	$⊢ (φ \land j \in (1 \dots M)) \to - j \in ℂ$
221	206	adantr	$⊢ (φ \land j \in (1 \dots M)) \to P \in ℕ_{0}$
222	220 221	expcld	$⊢ (φ \land j \in (1 \dots M)) \to {(- j)}^{P} \in ℂ$
223	222	mulid2d	$⊢ (φ \land j \in (1 \dots M)) \to 1 {(- j)}^{P} = {(- j)}^{P}$
224	199 217 223	3eqtrd	$⊢ (φ \land j \in (1 \dots M)) \to if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}) = {(- j)}^{P}$
225	224	prodeq2dv	$⊢ φ \to \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}) = \prod_{j = 1}^{M} {(- j)}^{P}$
226	186 225	oveq12d	$⊢ φ \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}) = (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P}$
227	167 226	oveq12d	$⊢ φ \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}) = 1 (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P}$
228		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
229		zexpcl	$⊢ (- j \in ℤ \land P \in ℕ_{0}) \to {(- j)}^{P} \in ℤ$
230	218 206 229	syl2anr	$⊢ (φ \land j \in (1 \dots M)) \to {(- j)}^{P} \in ℤ$
231	228 230	fprodzcl	$⊢ φ \to \prod_{j = 1}^{M} {(- j)}^{P} \in ℤ$
232	231	zcnd	$⊢ φ \to \prod_{j = 1}^{M} {(- j)}^{P} \in ℂ$
233	161 232	mulcld	$⊢ φ \to (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P} \in ℂ$
234	233	mulid2d	$⊢ φ \to 1 (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P} = (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P}$
235	227 234	eqtrd	$⊢ φ \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}) = (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P}$
236		eldifi	$⊢ c \in (C (P - 1) ∖ \{D\}) \to c \in C (P - 1)$
237	83	adantr	$⊢ (φ \land c \in C (P - 1)) \to 0 \in (0 \dots M)$
238	45 237	ffvelrnd	$⊢ (φ \land c \in C (P - 1)) \to c (0) \in (0 \dots P - 1)$
239	236 238	sylan2	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to c (0) \in (0 \dots P - 1)$
240	187 239	sseldi	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to c (0) \in ℝ$
241	168	adantr	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to P - 1 \in ℝ$
242		elfzle2	$⊢ c (0) \in (0 \dots P - 1) \to c (0) \leq P - 1$
243	239 242	syl	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to c (0) \leq P - 1$
244	240 241 243	lensymd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to \neg P - 1 < c (0)$
245	244	iffalsed	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) = (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}$
246	14	nn0zd	$⊢ φ \to P - 1 \in ℤ$
247	246	adantr	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to P - 1 \in ℤ$
248	239	elfzelzd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to c (0) \in ℤ$
249	247 248	zsubcld	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to P - 1 - c (0) \in ℤ$
250	45	ffnd	$⊢ (φ \land c \in C (P - 1)) \to c Fn (0 \dots M)$
251	250	adantr	$⊢ ((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \to c Fn (0 \dots M)$
252	68	ffnd	$⊢ φ \to D Fn (0 \dots M)$
253	252	ad2antrr	$⊢ ((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \to D Fn (0 \dots M)$
254		fveq2	$⊢ j = 0 \to c (j) = c (0)$
255	254	adantl	$⊢ ((φ \land P - 1 = c (0)) \land j = 0) \to c (j) = c (0)$
256		id	$⊢ P - 1 = c (0) \to P - 1 = c (0)$
257	256	eqcomd	$⊢ P - 1 = c (0) \to c (0) = P - 1$
258	257	ad2antlr	$⊢ ((φ \land P - 1 = c (0)) \land j = 0) \to c (0) = P - 1$
259	77	adantl	$⊢ (φ \land j = 0) \to D (j) = D (0)$
260	84	adantr	$⊢ (φ \land j = 0) \to D (0) = P - 1$
261	259 260	eqtr2d	$⊢ (φ \land j = 0) \to P - 1 = D (j)$
262	261	adantlr	$⊢ ((φ \land P - 1 = c (0)) \land j = 0) \to P - 1 = D (j)$
263	255 258 262	3eqtrd	$⊢ ((φ \land P - 1 = c (0)) \land j = 0) \to c (j) = D (j)$
264	263	adantllr	$⊢ (((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j = 0) \to c (j) = D (j)$
265	264	adantlr	$⊢ ((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land j = 0) \to c (j) = D (j)$
266	27	ad4antr	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to \sum_{j = 0}^{M} c (j) = P - 1$
267	168	ad5antr	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to P - 1 \in ℝ$
268	168	ad4antr	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to P - 1 \in ℝ$
269	45	adantr	$⊢ ((φ \land c \in C (P - 1)) \land k \in (1 \dots M)) \to c : (0 \dots M) ⟶ (0 \dots P - 1)$
270	51	sseli	$⊢ k \in (1 \dots M) \to k \in (0 \dots M)$
271	270	adantl	$⊢ ((φ \land c \in C (P - 1)) \land k \in (1 \dots M)) \to k \in (0 \dots M)$
272	269 271	ffvelrnd	$⊢ ((φ \land c \in C (P - 1)) \land k \in (1 \dots M)) \to c (k) \in (0 \dots P - 1)$
273	34 272	sseldi	$⊢ ((φ \land c \in C (P - 1)) \land k \in (1 \dots M)) \to c (k) \in ℕ_{0}$
274	48 273	fsumnn0cl	$⊢ (φ \land c \in C (P - 1)) \to \sum_{k = 1}^{M} c (k) \in ℕ_{0}$
275	274	nn0red	$⊢ (φ \land c \in C (P - 1)) \to \sum_{k = 1}^{M} c (k) \in ℝ$
276	275	ad3antrrr	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to \sum_{k = 1}^{M} c (k) \in ℝ$
277		0red	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to 0 \in ℝ$
278	45	ffvelrnda	$⊢ ((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \to c (j) \in (0 \dots P - 1)$
279	187 278	sseldi	$⊢ ((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \to c (j) \in ℝ$
280	279	ad2antrr	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to c (j) \in ℝ$
281		nfv	$⊢ Ⅎ k ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0)$
282		nfcv	$⊢ \underline{Ⅎ} k c (j)$
283		fzfid	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to (1 \dots M) \in Fin$
284		simp-4l	$⊢ (((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \land k \in (1 \dots M)) \to (φ \land c \in C (P - 1))$
285	74 272	sseldi	$⊢ ((φ \land c \in C (P - 1)) \land k \in (1 \dots M)) \to c (k) \in ℂ$
286	284 285	sylancom	$⊢ (((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \land k \in (1 \dots M)) \to c (k) \in ℂ$
287		1zzd	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to 1 \in ℤ$
288		elfzel2	$⊢ j \in (0 \dots M) \to M \in ℤ$
289	288	adantr	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to M \in ℤ$
290		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
291	290	adantr	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to j \in ℤ$
292	287 289 291	3jca	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to (1 \in ℤ \land M \in ℤ \land j \in ℤ)$
293		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
294	293	adantr	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to j \in ℕ_{0}$
295		neqne	$⊢ \neg j = 0 \to j \neq 0$
296	295	adantl	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to j \neq 0$
297		elnnne0	$⊢ j \in ℕ \leftrightarrow (j \in ℕ_{0} \land j \neq 0)$
298	294 296 297	sylanbrc	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to j \in ℕ$
299	298	nnge1d	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to 1 \leq j$
300		elfzle2	$⊢ j \in (0 \dots M) \to j \leq M$
301	300	adantr	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to j \leq M$
302	292 299 301	jca32	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to ((1 \in ℤ \land M \in ℤ \land j \in ℤ) \land (1 \leq j \land j \leq M))$
303		elfz2	$⊢ j \in (1 \dots M) \leftrightarrow ((1 \in ℤ \land M \in ℤ \land j \in ℤ) \land (1 \leq j \land j \leq M))$
304	302 303	sylibr	$⊢ (j \in (0 \dots M) \land \neg j = 0) \to j \in (1 \dots M)$
305	304	adantr	$⊢ ((j \in (0 \dots M) \land \neg j = 0) \land \neg c (j) = 0) \to j \in (1 \dots M)$
306	305	adantlll	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to j \in (1 \dots M)$
307		fveq2	$⊢ k = j \to c (k) = c (j)$
308	281 282 283 286 306 307	fsumsplit1	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to \sum_{k = 1}^{M} c (k) = c (j) + \sum_{k \in (1 \dots M) ∖ \{j\}} c (k)$
309	308	eqcomd	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to c (j) + \sum_{k \in (1 \dots M) ∖ \{j\}} c (k) = \sum_{k = 1}^{M} c (k)$
310	309 276	eqeltrd	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to c (j) + \sum_{k \in (1 \dots M) ∖ \{j\}} c (k) \in ℝ$
311		elfzle1	$⊢ c (j) \in (0 \dots P - 1) \to 0 \leq c (j)$
312	278 311	syl	$⊢ ((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \to 0 \leq c (j)$
313	312	ad2antrr	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to 0 \leq c (j)$
314		neqne	$⊢ \neg c (j) = 0 \to c (j) \neq 0$
315	314	adantl	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to c (j) \neq 0$
316	277 280 313 315	leneltd	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to 0 < c (j)$
317		diffi	$⊢ (1 \dots M) \in Fin \to (1 \dots M) ∖ \{j\} \in Fin$
318	105 317	mp1i	$⊢ (φ \land c \in C (P - 1)) \to (1 \dots M) ∖ \{j\} \in Fin$
319		eldifi	$⊢ k \in ((1 \dots M) ∖ \{j\}) \to k \in (1 \dots M)$
320	319	adantl	$⊢ ((φ \land c \in C (P - 1)) \land k \in ((1 \dots M) ∖ \{j\})) \to k \in (1 \dots M)$
321	51 320	sseldi	$⊢ ((φ \land c \in C (P - 1)) \land k \in ((1 \dots M) ∖ \{j\})) \to k \in (0 \dots M)$
322	45	ffvelrnda	$⊢ ((φ \land c \in C (P - 1)) \land k \in (0 \dots M)) \to c (k) \in (0 \dots P - 1)$
323	187 322	sseldi	$⊢ ((φ \land c \in C (P - 1)) \land k \in (0 \dots M)) \to c (k) \in ℝ$
324	321 323	syldan	$⊢ ((φ \land c \in C (P - 1)) \land k \in ((1 \dots M) ∖ \{j\})) \to c (k) \in ℝ$
325		elfzle1	$⊢ c (k) \in (0 \dots P - 1) \to 0 \leq c (k)$
326	322 325	syl	$⊢ ((φ \land c \in C (P - 1)) \land k \in (0 \dots M)) \to 0 \leq c (k)$
327	321 326	syldan	$⊢ ((φ \land c \in C (P - 1)) \land k \in ((1 \dots M) ∖ \{j\})) \to 0 \leq c (k)$
328	318 324 327	fsumge0	$⊢ (φ \land c \in C (P - 1)) \to 0 \leq \sum_{k \in (1 \dots M) ∖ \{j\}} c (k)$
329	328	adantr	$⊢ ((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \to 0 \leq \sum_{k \in (1 \dots M) ∖ \{j\}} c (k)$
330	318 324	fsumrecl	$⊢ (φ \land c \in C (P - 1)) \to \sum_{k \in (1 \dots M) ∖ \{j\}} c (k) \in ℝ$
331	330	adantr	$⊢ ((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \to \sum_{k \in (1 \dots M) ∖ \{j\}} c (k) \in ℝ$
332	279 331	addge01d	$⊢ ((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \to (0 \leq \sum_{k \in (1 \dots M) ∖ \{j\}} c (k) \leftrightarrow c (j) \leq c (j) + \sum_{k \in (1 \dots M) ∖ \{j\}} c (k))$
333	329 332	mpbid	$⊢ ((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \to c (j) \leq c (j) + \sum_{k \in (1 \dots M) ∖ \{j\}} c (k)$
334	333	ad2antrr	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to c (j) \leq c (j) + \sum_{k \in (1 \dots M) ∖ \{j\}} c (k)$
335	277 280 310 316 334	ltletrd	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to 0 < c (j) + \sum_{k \in (1 \dots M) ∖ \{j\}} c (k)$
336	335 309	breqtrd	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to 0 < \sum_{k = 1}^{M} c (k)$
337	276 336	elrpd	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to \sum_{k = 1}^{M} c (k) \in ℝ^{+}$
338	268 337	ltaddrpd	$⊢ ((((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to P - 1 < P - 1 + \sum_{k = 1}^{M} c (k)$
339	338	adantl3r	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to P - 1 < P - 1 + \sum_{k = 1}^{M} c (k)$
340		fveq2	$⊢ j = k \to c (j) = c (k)$
341	340	cbvsumv	$⊢ \sum_{j = 0}^{M} c (j) = \sum_{k = 0}^{M} c (k)$
342	341	a1i	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to \sum_{j = 0}^{M} c (j) = \sum_{k = 0}^{M} c (k)$
343	73	ad5antr	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to M \in ℤ_{\geq 0}$
344		simp-5l	$⊢ ((((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \land k \in (0 \dots M)) \to (φ \land c \in C (P - 1))$
345	74 322	sseldi	$⊢ ((φ \land c \in C (P - 1)) \land k \in (0 \dots M)) \to c (k) \in ℂ$
346	344 345	sylancom	$⊢ ((((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \land k \in (0 \dots M)) \to c (k) \in ℂ$
347		fveq2	$⊢ k = 0 \to c (k) = c (0)$
348	343 346 347	fsum1p	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to \sum_{k = 0}^{M} c (k) = c (0) + \sum_{k = 0 + 1}^{M} c (k)$
349	257	ad4antlr	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to c (0) = P - 1$
350	86	sumeq1i	$⊢ \sum_{k = 0 + 1}^{M} c (k) = \sum_{k = 1}^{M} c (k)$
351	350	a1i	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to \sum_{k = 0 + 1}^{M} c (k) = \sum_{k = 1}^{M} c (k)$
352	349 351	oveq12d	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to c (0) + \sum_{k = 0 + 1}^{M} c (k) = P - 1 + \sum_{k = 1}^{M} c (k)$
353	342 348 352	3eqtrrd	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to P - 1 + \sum_{k = 1}^{M} c (k) = \sum_{j = 0}^{M} c (j)$
354	339 353	breqtrd	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to P - 1 < \sum_{j = 0}^{M} c (j)$
355	267 354	gtned	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to \sum_{j = 0}^{M} c (j) \neq P - 1$
356	355	neneqd	$⊢ (((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \land \neg c (j) = 0) \to \neg \sum_{j = 0}^{M} c (j) = P - 1$
357	266 356	condan	$⊢ ((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \to c (j) = 0$
358		simpr	$⊢ (φ \land j \in (0 \dots M)) \to j \in (0 \dots M)$
359	34 67	sseldi	$⊢ (φ \land j \in (0 \dots M)) \to if (j = 0, P - 1, 0) \in ℕ_{0}$
360	5	fvmpt2	$⊢ (j \in (0 \dots M) \land if (j = 0, P - 1, 0) \in ℕ_{0}) \to D (j) = if (j = 0, P - 1, 0)$
361	358 359 360	syl2anc	$⊢ (φ \land j \in (0 \dots M)) \to D (j) = if (j = 0, P - 1, 0)$
362	361	adantr	$⊢ ((φ \land j \in (0 \dots M)) \land \neg j = 0) \to D (j) = if (j = 0, P - 1, 0)$
363		simpr	$⊢ ((φ \land j \in (0 \dots M)) \land \neg j = 0) \to \neg j = 0$
364	363	iffalsed	$⊢ ((φ \land j \in (0 \dots M)) \land \neg j = 0) \to if (j = 0, P - 1, 0) = 0$
365	362 364	eqtr2d	$⊢ ((φ \land j \in (0 \dots M)) \land \neg j = 0) \to 0 = D (j)$
366	365	adantllr	$⊢ (((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \land \neg j = 0) \to 0 = D (j)$
367	366	adantllr	$⊢ ((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \to 0 = D (j)$
368	357 367	eqtrd	$⊢ ((((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \land \neg j = 0) \to c (j) = D (j)$
369	265 368	pm2.61dan	$⊢ (((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \land j \in (0 \dots M)) \to c (j) = D (j)$
370	251 253 369	eqfnfvd	$⊢ ((φ \land c \in C (P - 1)) \land P - 1 = c (0)) \to c = D$
371	236 370	sylanl2	$⊢ ((φ \land c \in (C (P - 1) ∖ \{D\})) \land P - 1 = c (0)) \to c = D$
372		eldifsni	$⊢ c \in (C (P - 1) ∖ \{D\}) \to c \neq D$
373	372	neneqd	$⊢ c \in (C (P - 1) ∖ \{D\}) \to \neg c = D$
374	373	ad2antlr	$⊢ ((φ \land c \in (C (P - 1) ∖ \{D\})) \land P - 1 = c (0)) \to \neg c = D$
375	371 374	pm2.65da	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to \neg P - 1 = c (0)$
376	375	neqned	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to P - 1 \neq c (0)$
377	240 241 243 376	leneltd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to c (0) < P - 1$
378	240 241	posdifd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (c (0) < P - 1 \leftrightarrow 0 < P - 1 - c (0))$
379	377 378	mpbid	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to 0 < P - 1 - c (0)$
380		elnnz	$⊢ P - 1 - c (0) \in ℕ \leftrightarrow (P - 1 - c (0) \in ℤ \land 0 < P - 1 - c (0))$
381	249 379 380	sylanbrc	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to P - 1 - c (0) \in ℕ$
382	381	0expd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to 0^{P - 1 - c (0)} = 0$
383	382	oveq2d	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)} = (\frac{(P - 1)!}{(P - 1 - c (0))!}) \cdot 0$
384	161	adantr	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (P - 1)! \in ℂ$
385	381	nnnn0d	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to P - 1 - c (0) \in ℕ_{0}$
386	385	faccld	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (P - 1 - c (0))! \in ℕ$
387	386	nncnd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (P - 1 - c (0))! \in ℂ$
388	386	nnne0d	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (P - 1 - c (0))! \neq 0$
389	384 387 388	divcld	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to \frac{(P - 1)!}{(P - 1 - c (0))!} \in ℂ$
390	389	mul01d	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (\frac{(P - 1)!}{(P - 1 - c (0))!}) \cdot 0 = 0$
391	245 383 390	3eqtrd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) = 0$
392	391	oveq1d	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = 0 \cdot \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)})$
393	236 56	sylan2	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) \in ℤ$
394	393	zcnd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) \in ℂ$
395	394	mul02d	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to 0 \cdot \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = 0$
396	392 395	eqtrd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = 0$
397	396	oveq2d	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) \cdot 0$
398		fzfid	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (0 \dots M) \in Fin$
399	34 278	sseldi	$⊢ ((φ \land c \in C (P - 1)) \land j \in (0 \dots M)) \to c (j) \in ℕ_{0}$
400	236 399	sylanl2	$⊢ ((φ \land c \in (C (P - 1) ∖ \{D\})) \land j \in (0 \dots M)) \to c (j) \in ℕ_{0}$
401	400	faccld	$⊢ ((φ \land c \in (C (P - 1) ∖ \{D\})) \land j \in (0 \dots M)) \to c (j)! \in ℕ$
402	398 401	fprodnncl	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to \prod_{j = 0}^{M} c (j)! \in ℕ$
403	402	nncnd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to \prod_{j = 0}^{M} c (j)! \in ℂ$
404	402	nnne0d	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to \prod_{j = 0}^{M} c (j)! \neq 0$
405	384 403 404	divcld	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to \frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!} \in ℂ$
406	405	mul01d	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) \cdot 0 = 0$
407	397 406	eqtrd	$⊢ (φ \land c \in (C (P - 1) ∖ \{D\})) \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = 0$
408	407	sumeq2dv	$⊢ φ \to \sum_{c \in C (P - 1) ∖ \{D\}} (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = \sum_{c \in C (P - 1) ∖ \{D\}} 0$
409		diffi	$⊢ C (P - 1) \in Fin \to C (P - 1) ∖ \{D\} \in Fin$
410	20 409	syl	$⊢ φ \to C (P - 1) ∖ \{D\} \in Fin$
411	410	olcd	$⊢ φ \to (C (P - 1) ∖ \{D\} \subseteq ℤ_{\geq 0} \lor C (P - 1) ∖ \{D\} \in Fin)$
412		sumz	$⊢ (C (P - 1) ∖ \{D\} \subseteq ℤ_{\geq 0} \lor C (P - 1) ∖ \{D\} \in Fin) \to \sum_{c \in C (P - 1) ∖ \{D\}} 0 = 0$
413	411 412	syl	$⊢ φ \to \sum_{c \in C (P - 1) ∖ \{D\}} 0 = 0$
414	408 413	eqtrd	$⊢ φ \to \sum_{c \in C (P - 1) ∖ \{D\}} (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = 0$
415	235 414	oveq12d	$⊢ φ \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}) + \sum_{c \in C (P - 1) ∖ \{D\}} (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P} + 0$
416	233	addid1d	$⊢ φ \to (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P} + 0 = (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P}$
417		nfv	$⊢ Ⅎ j φ$
418	417 206 228 220	fprodexp	$⊢ φ \to \prod_{j = 1}^{M} {(- j)}^{P} = {\prod_{j = 1}^{M} (- j)}^{P}$
419	418	oveq2d	$⊢ φ \to (P - 1)! \prod_{j = 1}^{M} {(- j)}^{P} = (P - 1)! {\prod_{j = 1}^{M} (- j)}^{P}$
420	415 416 419	3eqtrd	$⊢ φ \to (\frac{(P - 1)!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) 0^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(0 - j)}^{P - D (j)}) + \sum_{c \in C (P - 1) ∖ \{D\}} (\frac{(P - 1)!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) 0^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(0 - j)}^{P - c (j)}) = (P - 1)! {\prod_{j = 1}^{M} (- j)}^{P}$
421	17 143 420	3eqtrd	$⊢ φ \to (ℝ D^{n} F) (P - 1) (0) = (P - 1)! {\prod_{j = 1}^{M} (- j)}^{P}$

Metamath Proof Explorer

Theorem etransclem35

Proof