etransclem28

Description: ( P - 1 ) factorial divides the N -th derivative of F applied to J . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem28.p	$⊢ φ \to P \in ℕ$
	etransclem28.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem28.n	$⊢ φ \to N \in ℕ_{0}$
	etransclem28.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
	etransclem28.d	$⊢ φ \to D \in C (N)$
	etransclem28.j	$⊢ φ \to J \in (0 \dots M)$
	etransclem28.t	$⊢ T = (\frac{N!}{\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)})$
Assertion	etransclem28	$⊢ φ \to (P - 1)! ∥ T$

Proof

Step	Hyp	Ref	Expression
1		etransclem28.p	$⊢ φ \to P \in ℕ$
2		etransclem28.m	$⊢ φ \to M \in ℕ_{0}$
3		etransclem28.n	$⊢ φ \to N \in ℕ_{0}$
4		etransclem28.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
5		etransclem28.d	$⊢ φ \to D \in C (N)$
6		etransclem28.j	$⊢ φ \to J \in (0 \dots M)$
7		etransclem28.t	$⊢ T = (\frac{N!}{\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)})$
8		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
9	1 8	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
10	9	faccld	$⊢ φ \to (P - 1)! \in ℕ$
11	10	nnzd	$⊢ φ \to (P - 1)! \in ℤ$
12	11	adantr	$⊢ (φ \land J = 0) \to (P - 1)! \in ℤ$
13	4 3	etransclem12	$⊢ φ \to C (N) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
14	5 13	eleqtrd	$⊢ φ \to D \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
15		fveq1	$⊢ c = D \to c (j) = D (j)$
16	15	sumeq2sdv	$⊢ c = D \to \sum_{j = 0}^{M} c (j) = \sum_{j = 0}^{M} D (j)$
17	16	eqeq1d	$⊢ c = D \to (\sum_{j = 0}^{M} c (j) = N \leftrightarrow \sum_{j = 0}^{M} D (j) = N)$
18	17	elrab	$⊢ D \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \leftrightarrow (D \in ({(0 \dots N)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} D (j) = N)$
19	18	simprbi	$⊢ D \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to \sum_{j = 0}^{M} D (j) = N$
20	14 19	syl	$⊢ φ \to \sum_{j = 0}^{M} D (j) = N$
21	20	eqcomd	$⊢ φ \to N = \sum_{j = 0}^{M} D (j)$
22	21	fveq2d	$⊢ φ \to N! = \sum_{j = 0}^{M} D (j)!$
23	22	oveq1d	$⊢ φ \to \frac{N!}{\prod_{j = 0}^{M} D (j)!} = \frac{\sum_{j = 0}^{M} D (j)!}{\prod_{j = 0}^{M} D (j)!}$
24		nfcv	$⊢ \underline{Ⅎ} j D$
25		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
26		nn0ex	$⊢ ℕ_{0} \in V$
27		fzssnn0	$⊢ (0 \dots N) \subseteq ℕ_{0}$
28	27	a1i	$⊢ D \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to (0 \dots N) \subseteq ℕ_{0}$
29		mapss	$⊢ (ℕ_{0} \in V \land (0 \dots N) \subseteq ℕ_{0}) \to {(0 \dots N)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
30	26 28 29	sylancr	$⊢ D \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to {(0 \dots N)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
31		elrabi	$⊢ D \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to D \in ({(0 \dots N)}^{(0 \dots M)})$
32	30 31	sseldd	$⊢ D \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to D \in ({ℕ_{0}}^{(0 \dots M)})$
33	14 32	syl	$⊢ φ \to D \in ({ℕ_{0}}^{(0 \dots M)})$
34	24 25 33	mccl	$⊢ φ \to \frac{\sum_{j = 0}^{M} D (j)!}{\prod_{j = 0}^{M} D (j)!} \in ℕ$
35	23 34	eqeltrd	$⊢ φ \to \frac{N!}{\prod_{j = 0}^{M} D (j)!} \in ℕ$
36	35	nnzd	$⊢ φ \to \frac{N!}{\prod_{j = 0}^{M} D (j)!} \in ℤ$
37	36	adantr	$⊢ (φ \land J = 0) \to \frac{N!}{\prod_{j = 0}^{M} D (j)!} \in ℤ$
38		df-neg	$⊢ - j = 0 - j$
39		oveq1	$⊢ J = 0 \to J - j = 0 - j$
40	38 39	eqtr4id	$⊢ J = 0 \to - j = J - j$
41	40	oveq1d	$⊢ J = 0 \to {(- j)}^{P - D (j)} = {(J - j)}^{P - D (j)}$
42	41	oveq2d	$⊢ J = 0 \to (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)} = (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}$
43	42	ifeq2d	$⊢ J = 0 \to if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}) = if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
44	43	prodeq2ad	$⊢ J = 0 \to \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}) = \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
45	44	adantl	$⊢ (φ \land J = 0) \to \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}) = \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)})$
46	14 31	syl	$⊢ φ \to D \in ({(0 \dots N)}^{(0 \dots M)})$
47		elmapi	$⊢ D \in ({(0 \dots N)}^{(0 \dots M)}) \to D : (0 \dots M) ⟶ (0 \dots N)$
48	46 47	syl	$⊢ φ \to D : (0 \dots M) ⟶ (0 \dots N)$
49	1 48 6	etransclem7	$⊢ φ \to \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ$
50	49	adantr	$⊢ (φ \land J = 0) \to \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(J - j)}^{P - D (j)}) \in ℤ$
51	45 50	eqeltrd	$⊢ (φ \land J = 0) \to \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}) \in ℤ$
52	12 51	zmulcld	$⊢ (φ \land J = 0) \to (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}) \in ℤ$
53	12 37 52	3jca	$⊢ (φ \land J = 0) \to ((P - 1)! \in ℤ \land \frac{N!}{\prod_{j = 0}^{M} D (j)!} \in ℤ \land (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}) \in ℤ)$
54		dvdsmul1	$⊢ ((P - 1)! \in ℤ \land \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}) \in ℤ) \to (P - 1)! ∥ (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)})$
55	12 51 54	syl2anc	$⊢ (φ \land J = 0) \to (P - 1)! ∥ (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)})$
56		dvdsmultr2	$⊢ ((P - 1)! \in ℤ \land \frac{N!}{\prod_{j = 0}^{M} D (j)!} \in ℤ \land (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}) \in ℤ) \to ((P - 1)! ∥ (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}) \to (P - 1)! ∥ (\frac{N!}{\prod_{j = 0}^{M} D (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)}))$
57	53 55 56	sylc	$⊢ (φ \land J = 0) \to (P - 1)! ∥ (\frac{N!}{\prod_{j = 0}^{M} D (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)})$
58	57	adantr	$⊢ ((φ \land J = 0) \land D (0) = P - 1) \to (P - 1)! ∥ (\frac{N!}{\prod_{j = 0}^{M} D (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)})$
59	1	ad2antrr	$⊢ ((φ \land J = 0) \land D (0) = P - 1) \to P \in ℕ$
60	2	ad2antrr	$⊢ ((φ \land J = 0) \land D (0) = P - 1) \to M \in ℕ_{0}$
61	48	ad2antrr	$⊢ ((φ \land J = 0) \land D (0) = P - 1) \to D : (0 \dots M) ⟶ (0 \dots N)$
62		eqid	$⊢ (\frac{N!}{\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{N!}{\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)})$
63		simplr	$⊢ ((φ \land J = 0) \land D (0) = P - 1) \to J = 0$
64		simpr	$⊢ ((φ \land J = 0) \land D (0) = P - 1) \to D (0) = P - 1$
65	59 60 61 62 63 64	etransclem14	$⊢ ((φ \land J = 0) \land D (0) = P - 1) \to (\frac{N!}{\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{N!}{\prod_{j = 0}^{M} D (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < D (j), 0, (\frac{P!}{(P - D (j))!}) {(- j)}^{P - D (j)})$
66	58 65	breqtrrd	$⊢ ((φ \land J = 0) \land D (0) = P - 1) \to (P - 1)! ∥ (\frac{N!}{\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)})$
67		dvds0	$⊢ (P - 1)! \in ℤ \to (P - 1)! ∥ 0$
68	11 67	syl	$⊢ φ \to (P - 1)! ∥ 0$
69	68	ad2antrr	$⊢ ((φ \land J = 0) \land \neg D (0) = P - 1) \to (P - 1)! ∥ 0$
70	1	ad2antrr	$⊢ ((φ \land J = 0) \land \neg D (0) = P - 1) \to P \in ℕ$
71	2	ad2antrr	$⊢ ((φ \land J = 0) \land \neg D (0) = P - 1) \to M \in ℕ_{0}$
72	3	ad2antrr	$⊢ ((φ \land J = 0) \land \neg D (0) = P - 1) \to N \in ℕ_{0}$
73	48	ad2antrr	$⊢ ((φ \land J = 0) \land \neg D (0) = P - 1) \to D : (0 \dots M) ⟶ (0 \dots N)$
74		simplr	$⊢ ((φ \land J = 0) \land \neg D (0) = P - 1) \to J = 0$
75		neqne	$⊢ \neg D (0) = P - 1 \to D (0) \neq P - 1$
76	75	adantl	$⊢ ((φ \land J = 0) \land \neg D (0) = P - 1) \to D (0) \neq P - 1$
77	70 71 72 73 62 74 76	etransclem15	$⊢ ((φ \land J = 0) \land \neg D (0) = P - 1) \to (\frac{N!}{\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$
78	69 77	breqtrrd	$⊢ ((φ \land J = 0) \land \neg D (0) = P - 1) \to (P - 1)! ∥ (\frac{N!}{\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)})$
79	66 78	pm2.61dan	$⊢ (φ \land J = 0) \to (P - 1)! ∥ (\frac{N!}{\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)})$
80	1	nnzd	$⊢ φ \to P \in ℤ$
81		elfznn0	$⊢ J \in (0 \dots M) \to J \in ℕ_{0}$
82	6 81	syl	$⊢ φ \to J \in ℕ_{0}$
83	82	nn0zd	$⊢ φ \to J \in ℤ$
84	1 2 3 83 4 5	etransclem26	$⊢ φ \to (\frac{N!}{\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)}) \in ℤ$
85	11 80 84	3jca	$⊢ φ \to ((P - 1)! \in ℤ \land P \in ℤ \land (\frac{N!}{\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)}) \in ℤ)$
86	85	adantr	$⊢ (φ \land \neg J = 0) \to ((P - 1)! \in ℤ \land P \in ℤ \land (\frac{N!}{\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)}) \in ℤ)$
87	1	nncnd	$⊢ φ \to P \in ℂ$
88		1cnd	$⊢ φ \to 1 \in ℂ$
89	87 88	npcand	$⊢ φ \to P - 1 + 1 = P$
90	89	eqcomd	$⊢ φ \to P = P - 1 + 1$
91	90	fveq2d	$⊢ φ \to P! = (P - 1 + 1)!$
92		facp1	$⊢ P - 1 \in ℕ_{0} \to (P - 1 + 1)! = (P - 1)! (P - 1 + 1)$
93	9 92	syl	$⊢ φ \to (P - 1 + 1)! = (P - 1)! (P - 1 + 1)$
94	89	oveq2d	$⊢ φ \to (P - 1)! (P - 1 + 1) = (P - 1)! P$
95	91 93 94	3eqtrrd	$⊢ φ \to (P - 1)! P = P!$
96	95	adantr	$⊢ (φ \land \neg J = 0) \to (P - 1)! P = P!$
97	1	adantr	$⊢ (φ \land \neg J = 0) \to P \in ℕ$
98	2	adantr	$⊢ (φ \land \neg J = 0) \to M \in ℕ_{0}$
99	3	adantr	$⊢ (φ \land \neg J = 0) \to N \in ℕ_{0}$
100	48	adantr	$⊢ (φ \land \neg J = 0) \to D : (0 \dots M) ⟶ (0 \dots N)$
101	20	adantr	$⊢ (φ \land \neg J = 0) \to \sum_{j = 0}^{M} D (j) = N$
102		1zzd	$⊢ (φ \land \neg J = 0) \to 1 \in ℤ$
103	2	nn0zd	$⊢ φ \to M \in ℤ$
104	103	adantr	$⊢ (φ \land \neg J = 0) \to M \in ℤ$
105	83	adantr	$⊢ (φ \land \neg J = 0) \to J \in ℤ$
106	102 104 105	3jca	$⊢ (φ \land \neg J = 0) \to (1 \in ℤ \land M \in ℤ \land J \in ℤ)$
107	82	adantr	$⊢ (φ \land \neg J = 0) \to J \in ℕ_{0}$
108		neqne	$⊢ \neg J = 0 \to J \neq 0$
109	108	adantl	$⊢ (φ \land \neg J = 0) \to J \neq 0$
110		elnnne0	$⊢ J \in ℕ \leftrightarrow (J \in ℕ_{0} \land J \neq 0)$
111	107 109 110	sylanbrc	$⊢ (φ \land \neg J = 0) \to J \in ℕ$
112	111	nnge1d	$⊢ (φ \land \neg J = 0) \to 1 \leq J$
113		elfzle2	$⊢ J \in (0 \dots M) \to J \leq M$
114	6 113	syl	$⊢ φ \to J \leq M$
115	114	adantr	$⊢ (φ \land \neg J = 0) \to J \leq M$
116	106 112 115	jca32	$⊢ (φ \land \neg J = 0) \to ((1 \in ℤ \land M \in ℤ \land J \in ℤ) \land (1 \leq J \land J \leq M))$
117		elfz2	$⊢ J \in (1 \dots M) \leftrightarrow ((1 \in ℤ \land M \in ℤ \land J \in ℤ) \land (1 \leq J \land J \leq M))$
118	116 117	sylibr	$⊢ (φ \land \neg J = 0) \to J \in (1 \dots M)$
119	97 98 99 100 101 62 118	etransclem25	$⊢ (φ \land \neg J = 0) \to P! ∥ (\frac{N!}{\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)})$
120	96 119	eqbrtrd	$⊢ (φ \land \neg J = 0) \to (P - 1)! P ∥ (\frac{N!}{\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)})$
121		muldvds1	$⊢ ((P - 1)! \in ℤ \land P \in ℤ \land (\frac{N!}{\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)}) \in ℤ) \to ((P - 1)! P ∥ (\frac{N!}{\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)}) \to (P - 1)! ∥ (\frac{N!}{\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)}))$
122	86 120 121	sylc	$⊢ (φ \land \neg J = 0) \to (P - 1)! ∥ (\frac{N!}{\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)})$
123	79 122	pm2.61dan	$⊢ φ \to (P - 1)! ∥ (\frac{N!}{\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)})$
124	123 7	breqtrrdi	$⊢ φ \to (P - 1)! ∥ T$

Metamath Proof Explorer

Theorem etransclem28

Proof