etransclem24

Description: P divides the I -th derivative of F applied to J . when J = 0 and I is not equal to P - 1 . This is the second part of case 2 proven in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem24.p	$⊢ φ \to P \in ℕ$
	etransclem24.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem24.i	$⊢ φ \to I \in ℕ_{0}$
	etransclem24.ip	$⊢ φ \to I \neq P - 1$
	etransclem24.j	$⊢ φ \to J = 0$
	etransclem24.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
	etransclem24.d	$⊢ φ \to D \in C (I)$
Assertion	etransclem24	$⊢ φ \to P ∥ (\frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!})$

Proof

Step	Hyp	Ref	Expression
1		etransclem24.p	$⊢ φ \to P \in ℕ$
2		etransclem24.m	$⊢ φ \to M \in ℕ_{0}$
3		etransclem24.i	$⊢ φ \to I \in ℕ_{0}$
4		etransclem24.ip	$⊢ φ \to I \neq P - 1$
5		etransclem24.j	$⊢ φ \to J = 0$
6		etransclem24.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
7		etransclem24.d	$⊢ φ \to D \in C (I)$
8	6 3	etransclem12	$⊢ φ \to C (I) = \{c \in ({(0 \dots I)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = I\}$
9	7 8	eleqtrd	$⊢ φ \to D \in \{c \in ({(0 \dots I)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = I\}$
10		fveq1	$⊢ c = D \to c (j) = D (j)$
11	10	sumeq2sdv	$⊢ c = D \to \sum_{j = 0}^{M} c (j) = \sum_{j = 0}^{M} D (j)$
12	11	eqeq1d	$⊢ c = D \to (\sum_{j = 0}^{M} c (j) = I \leftrightarrow \sum_{j = 0}^{M} D (j) = I)$
13	12	elrab	$⊢ D \in \{c \in ({(0 \dots I)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = I\} \leftrightarrow (D \in ({(0 \dots I)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} D (j) = I)$
14	9 13	sylib	$⊢ φ \to (D \in ({(0 \dots I)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} D (j) = I)$
15	14	simprd	$⊢ φ \to \sum_{j = 0}^{M} D (j) = I$
16	15	ad2antrr	$⊢ ((φ \land D (0) = P - 1) \land \neg \exists k \in (1 \dots M) D (k) \in ℕ) \to \sum_{j = 0}^{M} D (j) = I$
17		ralnex	$⊢ \forall k \in (1 \dots M) \neg D (k) \in ℕ \leftrightarrow \neg \exists k \in (1 \dots M) D (k) \in ℕ$
18		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
19	2 18	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
20	19	ad2antrr	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to M \in ℤ_{\geq 0}$
21		fzsscn	$⊢ (0 \dots I) \subseteq ℂ$
22		ssrab2	$⊢ \{c \in ({(0 \dots I)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = I\} \subseteq {(0 \dots I)}^{(0 \dots M)}$
23	8 22	eqsstrdi	$⊢ φ \to C (I) \subseteq {(0 \dots I)}^{(0 \dots M)}$
24	23 7	sseldd	$⊢ φ \to D \in ({(0 \dots I)}^{(0 \dots M)})$
25		elmapi	$⊢ D \in ({(0 \dots I)}^{(0 \dots M)}) \to D : (0 \dots M) ⟶ (0 \dots I)$
26	24 25	syl	$⊢ φ \to D : (0 \dots M) ⟶ (0 \dots I)$
27	26	ffvelrnda	$⊢ (φ \land j \in (0 \dots M)) \to D (j) \in (0 \dots I)$
28	21 27	sselid	$⊢ (φ \land j \in (0 \dots M)) \to D (j) \in ℂ$
29	28	ad4ant14	$⊢ (((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \land j \in (0 \dots M)) \to D (j) \in ℂ$
30		fveq2	$⊢ j = 0 \to D (j) = D (0)$
31	20 29 30	fsum1p	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to \sum_{j = 0}^{M} D (j) = D (0) + \sum_{j = 0 + 1}^{M} D (j)$
32		simplr	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to D (0) = P - 1$
33		0p1e1	$⊢ 0 + 1 = 1$
34	33	oveq1i	$⊢ (0 + 1 \dots M) = (1 \dots M)$
35	34	sumeq1i	$⊢ \sum_{j = 0 + 1}^{M} D (j) = \sum_{j = 1}^{M} D (j)$
36	35	a1i	$⊢ (φ \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to \sum_{j = 0 + 1}^{M} D (j) = \sum_{j = 1}^{M} D (j)$
37		fveq2	$⊢ k = j \to D (k) = D (j)$
38	37	eleq1d	$⊢ k = j \to (D (k) \in ℕ \leftrightarrow D (j) \in ℕ)$
39	38	notbid	$⊢ k = j \to (\neg D (k) \in ℕ \leftrightarrow \neg D (j) \in ℕ)$
40	39	rspccva	$⊢ (\forall k \in (1 \dots M) \neg D (k) \in ℕ \land j \in (1 \dots M)) \to \neg D (j) \in ℕ$
41	40	adantll	$⊢ ((φ \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \land j \in (1 \dots M)) \to \neg D (j) \in ℕ$
42		fzssnn0	$⊢ (0 \dots I) \subseteq ℕ_{0}$
43		fz1ssfz0	$⊢ (1 \dots M) \subseteq (0 \dots M)$
44	43	sseli	$⊢ j \in (1 \dots M) \to j \in (0 \dots M)$
45	44 27	sylan2	$⊢ (φ \land j \in (1 \dots M)) \to D (j) \in (0 \dots I)$
46	42 45	sselid	$⊢ (φ \land j \in (1 \dots M)) \to D (j) \in ℕ_{0}$
47		elnn0	$⊢ D (j) \in ℕ_{0} \leftrightarrow (D (j) \in ℕ \lor D (j) = 0)$
48	46 47	sylib	$⊢ (φ \land j \in (1 \dots M)) \to (D (j) \in ℕ \lor D (j) = 0)$
49	48	adantlr	$⊢ ((φ \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \land j \in (1 \dots M)) \to (D (j) \in ℕ \lor D (j) = 0)$
50		orel1	$⊢ \neg D (j) \in ℕ \to ((D (j) \in ℕ \lor D (j) = 0) \to D (j) = 0)$
51	41 49 50	sylc	$⊢ ((φ \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \land j \in (1 \dots M)) \to D (j) = 0$
52	51	sumeq2dv	$⊢ (φ \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to \sum_{j = 1}^{M} D (j) = \sum_{j = 1}^{M} 0$
53		fzfi	$⊢ (1 \dots M) \in Fin$
54	53	olci	$⊢ ((1 \dots M) \subseteq ℤ_{\geq A} \lor (1 \dots M) \in Fin)$
55		sumz	$⊢ ((1 \dots M) \subseteq ℤ_{\geq A} \lor (1 \dots M) \in Fin) \to \sum_{j = 1}^{M} 0 = 0$
56	54 55	mp1i	$⊢ (φ \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to \sum_{j = 1}^{M} 0 = 0$
57	36 52 56	3eqtrd	$⊢ (φ \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to \sum_{j = 0 + 1}^{M} D (j) = 0$
58	57	adantlr	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to \sum_{j = 0 + 1}^{M} D (j) = 0$
59	32 58	oveq12d	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to D (0) + \sum_{j = 0 + 1}^{M} D (j) = P - 1 + 0$
60		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
61	1 60	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
62	61	nn0red	$⊢ φ \to P - 1 \in ℝ$
63	62	recnd	$⊢ φ \to P - 1 \in ℂ$
64	63	addid1d	$⊢ φ \to P - 1 + 0 = P - 1$
65	64	ad2antrr	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to P - 1 + 0 = P - 1$
66	31 59 65	3eqtrd	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to \sum_{j = 0}^{M} D (j) = P - 1$
67	4	necomd	$⊢ φ \to P - 1 \neq I$
68	67	ad2antrr	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to P - 1 \neq I$
69	66 68	eqnetrd	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to \sum_{j = 0}^{M} D (j) \neq I$
70	69	neneqd	$⊢ ((φ \land D (0) = P - 1) \land \forall k \in (1 \dots M) \neg D (k) \in ℕ) \to \neg \sum_{j = 0}^{M} D (j) = I$
71	17 70	sylan2br	$⊢ ((φ \land D (0) = P - 1) \land \neg \exists k \in (1 \dots M) D (k) \in ℕ) \to \neg \sum_{j = 0}^{M} D (j) = I$
72	16 71	condan	$⊢ (φ \land D (0) = P - 1) \to \exists k \in (1 \dots M) D (k) \in ℕ$
73	1	nnzd	$⊢ φ \to P \in ℤ$
74	15	eqcomd	$⊢ φ \to I = \sum_{j = 0}^{M} D (j)$
75	74	fveq2d	$⊢ φ \to I! = \sum_{j = 0}^{M} D (j)!$
76	75	oveq1d	$⊢ φ \to \frac{I!}{\prod_{j = 0}^{M} D (j)!} = \frac{\sum_{j = 0}^{M} D (j)!}{\prod_{j = 0}^{M} D (j)!}$
77		nfcv	$⊢ \underline{Ⅎ} j D$
78		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
79		nn0ex	$⊢ ℕ_{0} \in V$
80		mapss	$⊢ (ℕ_{0} \in V \land (0 \dots I) \subseteq ℕ_{0}) \to {(0 \dots I)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
81	79 42 80	mp2an	$⊢ {(0 \dots I)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
82	81 24	sselid	$⊢ φ \to D \in ({ℕ_{0}}^{(0 \dots M)})$
83	77 78 82	mccl	$⊢ φ \to \frac{\sum_{j = 0}^{M} D (j)!}{\prod_{j = 0}^{M} D (j)!} \in ℕ$
84	76 83	eqeltrd	$⊢ φ \to \frac{I!}{\prod_{j = 0}^{M} D (j)!} \in ℕ$
85	84	nnzd	$⊢ φ \to \frac{I!}{\prod_{j = 0}^{M} D (j)!} \in ℤ$
86		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
87	1	adantr	$⊢ (φ \land j \in (1 \dots M)) \to P \in ℕ$
88	26	adantr	$⊢ (φ \land j \in (1 \dots M)) \to D : (0 \dots M) ⟶ (0 \dots I)$
89	44	adantl	$⊢ (φ \land j \in (1 \dots M)) \to j \in (0 \dots M)$
90		0zd	$⊢ φ \to 0 \in ℤ$
91	5 90	eqeltrd	$⊢ φ \to J \in ℤ$
92	91	adantr	$⊢ (φ \land j \in (1 \dots M)) \to J \in ℤ$
93	87 88 89 92	etransclem3	$⊢ (φ \land j \in (1 \dots M)) \to if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ$
94	86 93	fprodzcl	$⊢ φ \to \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ$
95	73 85 94	3jca	$⊢ φ \to (P \in ℤ \land \frac{I!}{\prod_{j = 0}^{M} D (j)!} \in ℤ \land \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ)$
96	95	3ad2ant1	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to (P \in ℤ \land \frac{I!}{\prod_{j = 0}^{M} D (j)!} \in ℤ \land \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ)$
97	73	adantr	$⊢ (φ \land k \in (1 \dots M)) \to P \in ℤ$
98	1	adantr	$⊢ (φ \land k \in (1 \dots M)) \to P \in ℕ$
99	26	adantr	$⊢ (φ \land k \in (1 \dots M)) \to D : (0 \dots M) ⟶ (0 \dots I)$
100	43	sseli	$⊢ k \in (1 \dots M) \to k \in (0 \dots M)$
101	100	adantl	$⊢ (φ \land k \in (1 \dots M)) \to k \in (0 \dots M)$
102	91	adantr	$⊢ (φ \land k \in (1 \dots M)) \to J \in ℤ$
103	98 99 101 102	etransclem3	$⊢ (φ \land k \in (1 \dots M)) \to if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) \in ℤ$
104		difss	$⊢ (1 \dots M) ∖ \{k\} \subseteq (1 \dots M)$
105		ssfi	$⊢ ((1 \dots M) \in Fin \land (1 \dots M) ∖ \{k\} \subseteq (1 \dots M)) \to (1 \dots M) ∖ \{k\} \in Fin$
106	53 104 105	mp2an	$⊢ (1 \dots M) ∖ \{k\} \in Fin$
107	106	a1i	$⊢ φ \to (1 \dots M) ∖ \{k\} \in Fin$
108	1	adantr	$⊢ (φ \land j \in ((1 \dots M) ∖ \{k\})) \to P \in ℕ$
109	26	adantr	$⊢ (φ \land j \in ((1 \dots M) ∖ \{k\})) \to D : (0 \dots M) ⟶ (0 \dots I)$
110	104 43	sstri	$⊢ (1 \dots M) ∖ \{k\} \subseteq (0 \dots M)$
111	110	sseli	$⊢ j \in ((1 \dots M) ∖ \{k\}) \to j \in (0 \dots M)$
112	111	adantl	$⊢ (φ \land j \in ((1 \dots M) ∖ \{k\})) \to j \in (0 \dots M)$
113	91	adantr	$⊢ (φ \land j \in ((1 \dots M) ∖ \{k\})) \to J \in ℤ$
114	108 109 112 113	etransclem3	$⊢ (φ \land j \in ((1 \dots M) ∖ \{k\})) \to if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ$
115	107 114	fprodzcl	$⊢ φ \to \prod_{j \in (1 \dots M) ∖ \{k\}} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ$
116	115	adantr	$⊢ (φ \land k \in (1 \dots M)) \to \prod_{j \in (1 \dots M) ∖ \{k\}} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ$
117	97 103 116	3jca	$⊢ (φ \land k \in (1 \dots M)) \to (P \in ℤ \land if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) \in ℤ \land \prod_{j \in (1 \dots M) ∖ \{k\}} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ)$
118	117	3adant3	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to (P \in ℤ \land if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) \in ℤ \land \prod_{j \in (1 \dots M) ∖ \{k\}} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ)$
119		dvds0	$⊢ P \in ℤ \to P ∥ 0$
120	73 119	syl	$⊢ φ \to P ∥ 0$
121	120	adantr	$⊢ (φ \land P < D (k)) \to P ∥ 0$
122	121	3ad2antl1	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land P < D (k)) \to P ∥ 0$
123		iftrue	$⊢ P < D (k) \to if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) = 0$
124	123	eqcomd	$⊢ P < D (k) \to 0 = if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)})$
125	124	adantl	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land P < D (k)) \to 0 = if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)})$
126	122 125	breqtrd	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land P < D (k)) \to P ∥ if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)})$
127	97	adantr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to P \in ℤ$
128		0zd	$⊢ (φ \land k \in (1 \dots M)) \to 0 \in ℤ$
129	99 101	ffvelrnd	$⊢ (φ \land k \in (1 \dots M)) \to D (k) \in (0 \dots I)$
130	129	elfzelzd	$⊢ (φ \land k \in (1 \dots M)) \to D (k) \in ℤ$
131	97 130	zsubcld	$⊢ (φ \land k \in (1 \dots M)) \to P - D (k) \in ℤ$
132	128 97 131	3jca	$⊢ (φ \land k \in (1 \dots M)) \to (0 \in ℤ \land P \in ℤ \land P - D (k) \in ℤ)$
133	132	adantr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to (0 \in ℤ \land P \in ℤ \land P - D (k) \in ℤ)$
134		fzssre	$⊢ (0 \dots I) \subseteq ℝ$
135	134 129	sselid	$⊢ (φ \land k \in (1 \dots M)) \to D (k) \in ℝ$
136	135	adantr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to D (k) \in ℝ$
137	127	zred	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to P \in ℝ$
138		simpr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to \neg P < D (k)$
139	136 137 138	nltled	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to D (k) \leq P$
140	137 136	subge0d	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to (0 \leq P - D (k) \leftrightarrow D (k) \leq P)$
141	139 140	mpbird	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to 0 \leq P - D (k)$
142		elfzle1	$⊢ D (k) \in (0 \dots I) \to 0 \leq D (k)$
143	129 142	syl	$⊢ (φ \land k \in (1 \dots M)) \to 0 \leq D (k)$
144	143	adantr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to 0 \leq D (k)$
145	137 136	subge02d	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to (0 \leq D (k) \leftrightarrow P - D (k) \leq P)$
146	144 145	mpbid	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to P - D (k) \leq P$
147	133 141 146	jca32	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to ((0 \in ℤ \land P \in ℤ \land P - D (k) \in ℤ) \land (0 \leq P - D (k) \land P - D (k) \leq P))$
148		elfz2	$⊢ P - D (k) \in (0 \dots P) \leftrightarrow ((0 \in ℤ \land P \in ℤ \land P - D (k) \in ℤ) \land (0 \leq P - D (k) \land P - D (k) \leq P))$
149	147 148	sylibr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to P - D (k) \in (0 \dots P)$
150		permnn	$⊢ P - D (k) \in (0 \dots P) \to \frac{P!}{(P - D (k))!} \in ℕ$
151	149 150	syl	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to \frac{P!}{(P - D (k))!} \in ℕ$
152	151	nnzd	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to \frac{P!}{(P - D (k))!} \in ℤ$
153	101	elfzelzd	$⊢ (φ \land k \in (1 \dots M)) \to k \in ℤ$
154	102 153	zsubcld	$⊢ (φ \land k \in (1 \dots M)) \to J - k \in ℤ$
155	154	adantr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to J - k \in ℤ$
156	131	adantr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to P - D (k) \in ℤ$
157		elnn0z	$⊢ P - D (k) \in ℕ_{0} \leftrightarrow (P - D (k) \in ℤ \land 0 \leq P - D (k))$
158	156 141 157	sylanbrc	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to P - D (k) \in ℕ_{0}$
159		zexpcl	$⊢ (J - k \in ℤ \land P - D (k) \in ℕ_{0}) \to {(J - k)}^{P - D (k)} \in ℤ$
160	155 158 159	syl2anc	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to {(J - k)}^{P - D (k)} \in ℤ$
161	127 152 160	3jca	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to (P \in ℤ \land \frac{P!}{(P - D (k))!} \in ℤ \land {(J - k)}^{P - D (k)} \in ℤ)$
162	161	3adantl3	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to (P \in ℤ \land \frac{P!}{(P - D (k))!} \in ℤ \land {(J - k)}^{P - D (k)} \in ℤ)$
163	127	3adantl3	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to P \in ℤ$
164	61	nn0zd	$⊢ φ \to P - 1 \in ℤ$
165	164	adantr	$⊢ (φ \land k \in (1 \dots M)) \to P - 1 \in ℤ$
166	128 165 131	3jca	$⊢ (φ \land k \in (1 \dots M)) \to (0 \in ℤ \land P - 1 \in ℤ \land P - D (k) \in ℤ)$
167	166	3adant3	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to (0 \in ℤ \land P - 1 \in ℤ \land P - D (k) \in ℤ)$
168	167	adantr	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to (0 \in ℤ \land P - 1 \in ℤ \land P - D (k) \in ℤ)$
169	141	3adantl3	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to 0 \leq P - D (k)$
170		1red	$⊢ (φ \land D (k) \in ℕ) \to 1 \in ℝ$
171		nnre	$⊢ D (k) \in ℕ \to D (k) \in ℝ$
172	171	adantl	$⊢ (φ \land D (k) \in ℕ) \to D (k) \in ℝ$
173	1	nnred	$⊢ φ \to P \in ℝ$
174	173	adantr	$⊢ (φ \land D (k) \in ℕ) \to P \in ℝ$
175		nnge1	$⊢ D (k) \in ℕ \to 1 \leq D (k)$
176	175	adantl	$⊢ (φ \land D (k) \in ℕ) \to 1 \leq D (k)$
177	170 172 174 176	lesub2dd	$⊢ (φ \land D (k) \in ℕ) \to P - D (k) \leq P - 1$
178	177	3adant2	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to P - D (k) \leq P - 1$
179	178	adantr	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to P - D (k) \leq P - 1$
180	168 169 179	jca32	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to ((0 \in ℤ \land P - 1 \in ℤ \land P - D (k) \in ℤ) \land (0 \leq P - D (k) \land P - D (k) \leq P - 1))$
181		elfz2	$⊢ P - D (k) \in (0 \dots P - 1) \leftrightarrow ((0 \in ℤ \land P - 1 \in ℤ \land P - D (k) \in ℤ) \land (0 \leq P - D (k) \land P - D (k) \leq P - 1))$
182	180 181	sylibr	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to P - D (k) \in (0 \dots P - 1)$
183		permnn	$⊢ P - D (k) \in (0 \dots P - 1) \to \frac{(P - 1)!}{(P - D (k))!} \in ℕ$
184	182 183	syl	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to \frac{(P - 1)!}{(P - D (k))!} \in ℕ$
185	184	nnzd	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to \frac{(P - 1)!}{(P - D (k))!} \in ℤ$
186		dvdsmul1	$⊢ (P \in ℤ \land \frac{(P - 1)!}{(P - D (k))!} \in ℤ) \to P ∥ P (\frac{(P - 1)!}{(P - D (k))!})$
187	163 185 186	syl2anc	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to P ∥ P (\frac{(P - 1)!}{(P - D (k))!})$
188	1	nncnd	$⊢ φ \to P \in ℂ$
189		1cnd	$⊢ φ \to 1 \in ℂ$
190	188 189	npcand	$⊢ φ \to P - 1 + 1 = P$
191	190	eqcomd	$⊢ φ \to P = P - 1 + 1$
192	191	fveq2d	$⊢ φ \to P! = (P - 1 + 1)!$
193		facp1	$⊢ P - 1 \in ℕ_{0} \to (P - 1 + 1)! = (P - 1)! (P - 1 + 1)$
194	61 193	syl	$⊢ φ \to (P - 1 + 1)! = (P - 1)! (P - 1 + 1)$
195	190	oveq2d	$⊢ φ \to (P - 1)! (P - 1 + 1) = (P - 1)! P$
196	61	faccld	$⊢ φ \to (P - 1)! \in ℕ$
197	196	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
198	197 188	mulcomd	$⊢ φ \to (P - 1)! P = P (P - 1)!$
199	195 198	eqtrd	$⊢ φ \to (P - 1)! (P - 1 + 1) = P (P - 1)!$
200	192 194 199	3eqtrd	$⊢ φ \to P! = P (P - 1)!$
201	200	oveq1d	$⊢ φ \to \frac{P!}{(P - D (k))!} = \frac{P (P - 1)!}{(P - D (k))!}$
202	201	adantr	$⊢ (φ \land \neg P < D (k)) \to \frac{P!}{(P - D (k))!} = \frac{P (P - 1)!}{(P - D (k))!}$
203	202	3ad2antl1	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to \frac{P!}{(P - D (k))!} = \frac{P (P - 1)!}{(P - D (k))!}$
204	188	ad2antrr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to P \in ℂ$
205	197	ad2antrr	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to (P - 1)! \in ℂ$
206	158	faccld	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to (P - D (k))! \in ℕ$
207	206	nncnd	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to (P - D (k))! \in ℂ$
208	206	nnne0d	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to (P - D (k))! \neq 0$
209	204 205 207 208	divassd	$⊢ ((φ \land k \in (1 \dots M)) \land \neg P < D (k)) \to \frac{P (P - 1)!}{(P - D (k))!} = P (\frac{(P - 1)!}{(P - D (k))!})$
210	209	3adantl3	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to \frac{P (P - 1)!}{(P - D (k))!} = P (\frac{(P - 1)!}{(P - D (k))!})$
211	203 210	eqtr2d	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to P (\frac{(P - 1)!}{(P - D (k))!}) = \frac{P!}{(P - D (k))!}$
212	187 211	breqtrd	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to P ∥ (\frac{P!}{(P - D (k))!})$
213		dvdsmultr1	$⊢ (P \in ℤ \land \frac{P!}{(P - D (k))!} \in ℤ \land {(J - k)}^{P - D (k)} \in ℤ) \to (P ∥ (\frac{P!}{(P - D (k))!}) \to P ∥ (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)})$
214	162 212 213	sylc	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to P ∥ (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}$
215		iffalse	$⊢ \neg P < D (k) \to if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) = (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}$
216	215	adantl	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) = (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}$
217	214 216	breqtrrd	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land \neg P < D (k)) \to P ∥ if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)})$
218	126 217	pm2.61dan	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to P ∥ if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)})$
219		dvdsmultr1	$⊢ (P \in ℤ \land if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) \in ℤ \land \prod_{j \in (1 \dots M) ∖ \{k\}} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ) \to (P ∥ if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) \to P ∥ if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) \prod_{j \in (1 \dots M) ∖ \{k\}} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}))$
220	118 218 219	sylc	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to P ∥ if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) \prod_{j \in (1 \dots M) ∖ \{k\}} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
221		fzfid	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to (1 \dots M) \in Fin$
222	93	zcnd	$⊢ (φ \land j \in (1 \dots M)) \to if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℂ$
223	222	3ad2antl1	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land j \in (1 \dots M)) \to if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℂ$
224		simp2	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to k \in (1 \dots M)$
225		fveq2	$⊢ j = k \to D (j) = D (k)$
226	225	breq2d	$⊢ j = k \to (P < D (j) \leftrightarrow P < D (k))$
227	225	oveq2d	$⊢ j = k \to P - D (j) = P - D (k)$
228	227	fveq2d	$⊢ j = k \to (P - D (j))! = (P - D (k))!$
229	228	oveq2d	$⊢ j = k \to \frac{P!}{(P - D (j))!} = \frac{P!}{(P - D (k))!}$
230		oveq2	$⊢ j = k \to J - j = J - k$
231	230 227	oveq12d	$⊢ j = k \to {(J - j)}^{P - D (j)} = {(J - k)}^{P - D (k)}$
232	229 231	oveq12d	$⊢ j = k \to (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)} = (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}$
233	226 232	ifbieq2d	$⊢ j = k \to if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)})$
234	233	adantl	$⊢ ((φ \land k \in (1 \dots M) \land D (k) \in ℕ) \land j = k) \to if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)})$
235	221 223 224 234	fprodsplit1	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = if (P < D (k), 0, (\frac{P!}{(P - D (k))!}) {(J - k)}^{P - D (k)}) \prod_{j \in (1 \dots M) ∖ \{k\}} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
236	220 235	breqtrrd	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to P ∥ \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
237		dvdsmultr2	$⊢ (P \in ℤ \land \frac{I!}{\prod_{j = 0}^{M} D (j)!} \in ℤ \land \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ) \to (P ∥ \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \to P ∥ (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}))$
238	96 236 237	sylc	$⊢ (φ \land k \in (1 \dots M) \land D (k) \in ℕ) \to P ∥ (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
239	238	3adant1r	$⊢ ((φ \land D (0) = P - 1) \land k \in (1 \dots M) \land D (k) \in ℕ) \to P ∥ (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
240		simpr	$⊢ (φ \land D (0) = P - 1) \to D (0) = P - 1$
241		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
242	19 241	syl	$⊢ φ \to 0 \in (0 \dots M)$
243	26 242	ffvelrnd	$⊢ φ \to D (0) \in (0 \dots I)$
244	134 243	sselid	$⊢ φ \to D (0) \in ℝ$
245	244	adantr	$⊢ (φ \land D (0) = P - 1) \to D (0) \in ℝ$
246	62	adantr	$⊢ (φ \land D (0) = P - 1) \to P - 1 \in ℝ$
247	245 246	lttri3d	$⊢ (φ \land D (0) = P - 1) \to (D (0) = P - 1 \leftrightarrow (\neg D (0) < P - 1 \land \neg P - 1 < D (0)))$
248	240 247	mpbid	$⊢ (φ \land D (0) = P - 1) \to (\neg D (0) < P - 1 \land \neg P - 1 < D (0))$
249	248	simprd	$⊢ (φ \land D (0) = P - 1) \to \neg P - 1 < D (0)$
250	249	iffalsed	$⊢ (φ \land D (0) = P - 1) \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) = (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}$
251		oveq2	$⊢ D (0) = P - 1 \to P - 1 - D (0) = P - 1 - (P - 1)$
252	63	subidd	$⊢ φ \to P - 1 - (P - 1) = 0$
253	251 252	sylan9eqr	$⊢ (φ \land D (0) = P - 1) \to P - 1 - D (0) = 0$
254	253	fveq2d	$⊢ (φ \land D (0) = P - 1) \to (P - 1 - D (0))! = 0!$
255		fac0	$⊢ 0! = 1$
256	254 255	eqtrdi	$⊢ (φ \land D (0) = P - 1) \to (P - 1 - D (0))! = 1$
257	256	oveq2d	$⊢ (φ \land D (0) = P - 1) \to \frac{(P - 1)!}{(P - 1 - D (0))!} = \frac{(P - 1)!}{1}$
258	197	div1d	$⊢ φ \to \frac{(P - 1)!}{1} = (P - 1)!$
259	258	adantr	$⊢ (φ \land D (0) = P - 1) \to \frac{(P - 1)!}{1} = (P - 1)!$
260	257 259	eqtrd	$⊢ (φ \land D (0) = P - 1) \to \frac{(P - 1)!}{(P - 1 - D (0))!} = (P - 1)!$
261	253	oveq2d	$⊢ (φ \land D (0) = P - 1) \to J^{P - 1 - D (0)} = J^{0}$
262	91	zcnd	$⊢ φ \to J \in ℂ$
263	262	exp0d	$⊢ φ \to J^{0} = 1$
264	263	adantr	$⊢ (φ \land D (0) = P - 1) \to J^{0} = 1$
265	261 264	eqtrd	$⊢ (φ \land D (0) = P - 1) \to J^{P - 1 - D (0)} = 1$
266	260 265	oveq12d	$⊢ (φ \land D (0) = P - 1) \to (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)} = (P - 1)! \cdot 1$
267	197	mulid1d	$⊢ φ \to (P - 1)! \cdot 1 = (P - 1)!$
268	267	adantr	$⊢ (φ \land D (0) = P - 1) \to (P - 1)! \cdot 1 = (P - 1)!$
269	250 266 268	3eqtrd	$⊢ (φ \land D (0) = P - 1) \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) = (P - 1)!$
270	269	oveq1d	$⊢ (φ \land D (0) = P - 1) \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
271	270	oveq2d	$⊢ (φ \land D (0) = P - 1) \to (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
272	271	oveq1d	$⊢ (φ \land D (0) = P - 1) \to \frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!} = \frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!}$
273	84	nncnd	$⊢ φ \to \frac{I!}{\prod_{j = 0}^{M} D (j)!} \in ℂ$
274	94	zcnd	$⊢ φ \to \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℂ$
275	197 274	mulcld	$⊢ φ \to (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℂ$
276	196	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
277	273 275 197 276	divassd	$⊢ φ \to \frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!} = (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) (\frac{(P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!})$
278	277	adantr	$⊢ (φ \land D (0) = P - 1) \to \frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!} = (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) (\frac{(P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!})$
279	274 197 276	divcan3d	$⊢ φ \to \frac{(P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!} = \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
280	279	oveq2d	$⊢ φ \to (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) (\frac{(P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!}) = (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
281	280	adantr	$⊢ (φ \land D (0) = P - 1) \to (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) (\frac{(P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!}) = (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
282	272 278 281	3eqtrd	$⊢ (φ \land D (0) = P - 1) \to \frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!} = (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
283	282	3ad2ant1	$⊢ ((φ \land D (0) = P - 1) \land k \in (1 \dots M) \land D (k) \in ℕ) \to \frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!} = (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
284	239 283	breqtrrd	$⊢ ((φ \land D (0) = P - 1) \land k \in (1 \dots M) \land D (k) \in ℕ) \to P ∥ (\frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!})$
285	284	rexlimdv3a	$⊢ (φ \land D (0) = P - 1) \to (\exists k \in (1 \dots M) D (k) \in ℕ \to P ∥ (\frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!}))$
286	72 285	mpd	$⊢ (φ \land D (0) = P - 1) \to P ∥ (\frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!})$
287	120	adantr	$⊢ (φ \land D (0) \neq P - 1) \to P ∥ 0$
288		simpr	$⊢ ((φ \land D (0) \neq P - 1) \land P - 1 < D (0)) \to P - 1 < D (0)$
289	288	iftrued	$⊢ ((φ \land D (0) \neq P - 1) \land P - 1 < D (0)) \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) = 0$
290		simpr	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to \neg P - 1 < D (0)$
291	290	iffalsed	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) = (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}$
292		simpll	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to φ$
293	244	ad2antrr	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to D (0) \in ℝ$
294	62	ad2antrr	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to P - 1 \in ℝ$
295	293 294 290	nltled	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to D (0) \leq P - 1$
296		id	$⊢ D (0) \neq P - 1 \to D (0) \neq P - 1$
297	296	necomd	$⊢ D (0) \neq P - 1 \to P - 1 \neq D (0)$
298	297	ad2antlr	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to P - 1 \neq D (0)$
299	293 294 295 298	leneltd	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to D (0) < P - 1$
300	5	oveq1d	$⊢ φ \to J^{P - 1 - D (0)} = 0^{P - 1 - D (0)}$
301	300	adantr	$⊢ (φ \land D (0) < P - 1) \to J^{P - 1 - D (0)} = 0^{P - 1 - D (0)}$
302	243	elfzelzd	$⊢ φ \to D (0) \in ℤ$
303	164 302	zsubcld	$⊢ φ \to P - 1 - D (0) \in ℤ$
304	303	adantr	$⊢ (φ \land D (0) < P - 1) \to P - 1 - D (0) \in ℤ$
305		simpr	$⊢ (φ \land D (0) < P - 1) \to D (0) < P - 1$
306	244	adantr	$⊢ (φ \land D (0) < P - 1) \to D (0) \in ℝ$
307	62	adantr	$⊢ (φ \land D (0) < P - 1) \to P - 1 \in ℝ$
308	306 307	posdifd	$⊢ (φ \land D (0) < P - 1) \to (D (0) < P - 1 \leftrightarrow 0 < P - 1 - D (0))$
309	305 308	mpbid	$⊢ (φ \land D (0) < P - 1) \to 0 < P - 1 - D (0)$
310		elnnz	$⊢ P - 1 - D (0) \in ℕ \leftrightarrow (P - 1 - D (0) \in ℤ \land 0 < P - 1 - D (0))$
311	304 309 310	sylanbrc	$⊢ (φ \land D (0) < P - 1) \to P - 1 - D (0) \in ℕ$
312	311	0expd	$⊢ (φ \land D (0) < P - 1) \to 0^{P - 1 - D (0)} = 0$
313	301 312	eqtrd	$⊢ (φ \land D (0) < P - 1) \to J^{P - 1 - D (0)} = 0$
314	313	oveq2d	$⊢ (φ \land D (0) < P - 1) \to (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)} = (\frac{(P - 1)!}{(P - 1 - D (0))!}) \cdot 0$
315	197	adantr	$⊢ (φ \land D (0) < P - 1) \to (P - 1)! \in ℂ$
316	311	nnnn0d	$⊢ (φ \land D (0) < P - 1) \to P - 1 - D (0) \in ℕ_{0}$
317	316	faccld	$⊢ (φ \land D (0) < P - 1) \to (P - 1 - D (0))! \in ℕ$
318	317	nncnd	$⊢ (φ \land D (0) < P - 1) \to (P - 1 - D (0))! \in ℂ$
319	317	nnne0d	$⊢ (φ \land D (0) < P - 1) \to (P - 1 - D (0))! \neq 0$
320	315 318 319	divcld	$⊢ (φ \land D (0) < P - 1) \to \frac{(P - 1)!}{(P - 1 - D (0))!} \in ℂ$
321	320	mul01d	$⊢ (φ \land D (0) < P - 1) \to (\frac{(P - 1)!}{(P - 1 - D (0))!}) \cdot 0 = 0$
322	314 321	eqtrd	$⊢ (φ \land D (0) < P - 1) \to (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)} = 0$
323	292 299 322	syl2anc	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)} = 0$
324	291 323	eqtrd	$⊢ ((φ \land D (0) \neq P - 1) \land \neg P - 1 < D (0)) \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) = 0$
325	289 324	pm2.61dan	$⊢ (φ \land D (0) \neq P - 1) \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) = 0$
326	325	oveq1d	$⊢ (φ \land D (0) \neq P - 1) \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = 0 \cdot \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
327	274	mul02d	$⊢ φ \to 0 \cdot \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = 0$
328	327	adantr	$⊢ (φ \land D (0) \neq P - 1) \to 0 \cdot \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = 0$
329	326 328	eqtrd	$⊢ (φ \land D (0) \neq P - 1) \to if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = 0$
330	329	oveq2d	$⊢ (φ \land D (0) \neq P - 1) \to (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \cdot 0$
331	273	mul01d	$⊢ φ \to (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \cdot 0 = 0$
332	331	adantr	$⊢ (φ \land D (0) \neq P - 1) \to (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) \cdot 0 = 0$
333	330 332	eqtrd	$⊢ (φ \land D (0) \neq P - 1) \to (\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) = 0$
334	333	oveq1d	$⊢ (φ \land D (0) \neq P - 1) \to \frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!} = \frac{0}{(P - 1)!}$
335	197 276	div0d	$⊢ φ \to \frac{0}{(P - 1)!} = 0$
336	335	adantr	$⊢ (φ \land D (0) \neq P - 1) \to \frac{0}{(P - 1)!} = 0$
337	334 336	eqtrd	$⊢ (φ \land D (0) \neq P - 1) \to \frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!} = 0$
338	287 337	breqtrrd	$⊢ (φ \land D (0) \neq P - 1) \to P ∥ (\frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!})$
339	286 338	pm2.61dane	$⊢ φ \to P ∥ (\frac{(\frac{I!}{\prod_{j = 0}^{M} D (j)!}) if (P - 1 < D (0), 0, (\frac{(P - 1)!}{(P - 1 - D (0))!}) J^{P - 1 - D (0)}) \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})}{(P - 1)!})$

Metamath Proof Explorer

Theorem etransclem24

Proof