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

Metamath Proof Explorer

Theorem etransclem35

Proof