etransclem25

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

	Ref	Expression
Hypotheses	etransclem25.p	$⊢ φ \to P \in ℕ$
	etransclem25.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem25.n	$⊢ φ \to N \in ℕ_{0}$
	etransclem25.c	$⊢ φ \to C : (0 \dots M) ⟶ (0 \dots N)$
	etransclem25.sumc	$⊢ φ \to \sum_{j = 0}^{M} C (j) = N$
	etransclem25.t	$⊢ T = (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)})$
	etransclem25.j	$⊢ φ \to J \in (1 \dots M)$
Assertion	etransclem25	$⊢ φ \to P! ∥ T$

Proof

Step	Hyp	Ref	Expression
1		etransclem25.p	$⊢ φ \to P \in ℕ$
2		etransclem25.m	$⊢ φ \to M \in ℕ_{0}$
3		etransclem25.n	$⊢ φ \to N \in ℕ_{0}$
4		etransclem25.c	$⊢ φ \to C : (0 \dots M) ⟶ (0 \dots N)$
5		etransclem25.sumc	$⊢ φ \to \sum_{j = 0}^{M} C (j) = N$
6		etransclem25.t	$⊢ T = (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)})$
7		etransclem25.j	$⊢ φ \to J \in (1 \dots M)$
8	1	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
9	8	faccld	$⊢ φ \to P! \in ℕ$
10	9	nnzd	$⊢ φ \to P! \in ℤ$
11	5	eqcomd	$⊢ φ \to N = \sum_{j = 0}^{M} C (j)$
12	11	fveq2d	$⊢ φ \to N! = \sum_{j = 0}^{M} C (j)!$
13	12	oveq1d	$⊢ φ \to \frac{N!}{\prod_{j = 0}^{M} C (j)!} = \frac{\sum_{j = 0}^{M} C (j)!}{\prod_{j = 0}^{M} C (j)!}$
14		nfcv	$⊢ \underline{Ⅎ} j C$
15		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
16		nn0ex	$⊢ ℕ_{0} \in V$
17		fzssnn0	$⊢ (0 \dots N) \subseteq ℕ_{0}$
18		mapss	$⊢ (ℕ_{0} \in V \land (0 \dots N) \subseteq ℕ_{0}) \to {(0 \dots N)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
19	16 17 18	mp2an	$⊢ {(0 \dots N)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
20		ovex	$⊢ (0 \dots N) \in V$
21		ovexd	$⊢ C : (0 \dots M) ⟶ (0 \dots N) \to (0 \dots M) \in V$
22		elmapg	$⊢ ((0 \dots N) \in V \land (0 \dots M) \in V) \to (C \in ({(0 \dots N)}^{(0 \dots M)}) \leftrightarrow C : (0 \dots M) ⟶ (0 \dots N))$
23	20 21 22	sylancr	$⊢ C : (0 \dots M) ⟶ (0 \dots N) \to (C \in ({(0 \dots N)}^{(0 \dots M)}) \leftrightarrow C : (0 \dots M) ⟶ (0 \dots N))$
24	23	ibir	$⊢ C : (0 \dots M) ⟶ (0 \dots N) \to C \in ({(0 \dots N)}^{(0 \dots M)})$
25	19 24	sseldi	$⊢ C : (0 \dots M) ⟶ (0 \dots N) \to C \in ({ℕ_{0}}^{(0 \dots M)})$
26	4 25	syl	$⊢ φ \to C \in ({ℕ_{0}}^{(0 \dots M)})$
27	14 15 26	mccl	$⊢ φ \to \frac{\sum_{j = 0}^{M} C (j)!}{\prod_{j = 0}^{M} C (j)!} \in ℕ$
28	13 27	eqeltrd	$⊢ φ \to \frac{N!}{\prod_{j = 0}^{M} C (j)!} \in ℕ$
29	28	nnzd	$⊢ φ \to \frac{N!}{\prod_{j = 0}^{M} C (j)!} \in ℤ$
30	7	elfzelzd	$⊢ φ \to J \in ℤ$
31	1 2 4 30	etransclem10	$⊢ φ \to if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \in ℤ$
32	29 31	zmulcld	$⊢ φ \to (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \in ℤ$
33		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
34	1	adantr	$⊢ (φ \land j \in (1 \dots M)) \to P \in ℕ$
35	4	adantr	$⊢ (φ \land j \in (1 \dots M)) \to C : (0 \dots M) ⟶ (0 \dots N)$
36		0z	$⊢ 0 \in ℤ$
37		fzp1ss	$⊢ 0 \in ℤ \to (0 + 1 \dots M) \subseteq (0 \dots M)$
38	36 37	ax-mp	$⊢ (0 + 1 \dots M) \subseteq (0 \dots M)$
39		id	$⊢ j \in (1 \dots M) \to j \in (1 \dots M)$
40		1e0p1	$⊢ 1 = 0 + 1$
41	40	oveq1i	$⊢ (1 \dots M) = (0 + 1 \dots M)$
42	39 41	eleqtrdi	$⊢ j \in (1 \dots M) \to j \in (0 + 1 \dots M)$
43	38 42	sseldi	$⊢ j \in (1 \dots M) \to j \in (0 \dots M)$
44	43	adantl	$⊢ (φ \land j \in (1 \dots M)) \to j \in (0 \dots M)$
45	30	adantr	$⊢ (φ \land j \in (1 \dots M)) \to J \in ℤ$
46	34 35 44 45	etransclem3	$⊢ (φ \land j \in (1 \dots M)) \to if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ$
47	33 46	fprodzcl	$⊢ φ \to \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ$
48	10 32 47	3jca	$⊢ φ \to (P! \in ℤ \land (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \in ℤ \land \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ)$
49	30	zcnd	$⊢ φ \to J \in ℂ$
50	49	subidd	$⊢ φ \to J - J = 0$
51	50	eqcomd	$⊢ φ \to 0 = J - J$
52	51	oveq1d	$⊢ φ \to 0^{P - C (J)} = {(J - J)}^{P - C (J)}$
53	52	oveq2d	$⊢ φ \to (\frac{P!}{(P - C (J))!}) 0^{P - C (J)} = (\frac{P!}{(P - C (J))!}) {(J - J)}^{P - C (J)}$
54	53	ifeq2d	$⊢ φ \to if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}) = if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) {(J - J)}^{P - C (J)})$
55		id	$⊢ J \in (1 \dots M) \to J \in (1 \dots M)$
56	55 41	eleqtrdi	$⊢ J \in (1 \dots M) \to J \in (0 + 1 \dots M)$
57	38 56	sseldi	$⊢ J \in (1 \dots M) \to J \in (0 \dots M)$
58	7 57	syl	$⊢ φ \to J \in (0 \dots M)$
59	1 4 58 30	etransclem3	$⊢ φ \to if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) {(J - J)}^{P - C (J)}) \in ℤ$
60	54 59	eqeltrd	$⊢ φ \to if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}) \in ℤ$
61		fzfi	$⊢ (1 \dots M) \in Fin$
62		diffi	$⊢ (1 \dots M) \in Fin \to (1 \dots M) ∖ \{J\} \in Fin$
63	61 62	mp1i	$⊢ φ \to (1 \dots M) ∖ \{J\} \in Fin$
64	1	adantr	$⊢ (φ \land j \in ((1 \dots M) ∖ \{J\})) \to P \in ℕ$
65	4	adantr	$⊢ (φ \land j \in ((1 \dots M) ∖ \{J\})) \to C : (0 \dots M) ⟶ (0 \dots N)$
66		eldifi	$⊢ j \in ((1 \dots M) ∖ \{J\}) \to j \in (1 \dots M)$
67	66 43	syl	$⊢ j \in ((1 \dots M) ∖ \{J\}) \to j \in (0 \dots M)$
68	67	adantl	$⊢ (φ \land j \in ((1 \dots M) ∖ \{J\})) \to j \in (0 \dots M)$
69	30	adantr	$⊢ (φ \land j \in ((1 \dots M) ∖ \{J\})) \to J \in ℤ$
70	64 65 68 69	etransclem3	$⊢ (φ \land j \in ((1 \dots M) ∖ \{J\})) \to if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ$
71	63 70	fprodzcl	$⊢ φ \to \prod_{j \in (1 \dots M) ∖ \{J\}} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ$
72		dvds0	$⊢ P! \in ℤ \to P! ∥ 0$
73	10 72	syl	$⊢ φ \to P! ∥ 0$
74	73	adantr	$⊢ (φ \land P < C (J)) \to P! ∥ 0$
75		iftrue	$⊢ P < C (J) \to if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}) = 0$
76	75	eqcomd	$⊢ P < C (J) \to 0 = if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
77	76	adantl	$⊢ (φ \land P < C (J)) \to 0 = if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
78	74 77	breqtrd	$⊢ (φ \land P < C (J)) \to P! ∥ if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
79		iddvds	$⊢ P! \in ℤ \to P! ∥ P!$
80	10 79	syl	$⊢ φ \to P! ∥ P!$
81	80	ad2antrr	$⊢ ((φ \land \neg P < C (J)) \land P = C (J)) \to P! ∥ P!$
82		iffalse	$⊢ \neg P < C (J) \to if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}) = (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}$
83	82	ad2antlr	$⊢ ((φ \land \neg P < C (J)) \land P = C (J)) \to if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}) = (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}$
84		oveq1	$⊢ P = C (J) \to P - C (J) = C (J) - C (J)$
85	84	adantl	$⊢ (φ \land P = C (J)) \to P - C (J) = C (J) - C (J)$
86	4 58	ffvelrnd	$⊢ φ \to C (J) \in (0 \dots N)$
87	86	elfzelzd	$⊢ φ \to C (J) \in ℤ$
88	87	zcnd	$⊢ φ \to C (J) \in ℂ$
89	88	adantr	$⊢ (φ \land P = C (J)) \to C (J) \in ℂ$
90	89	subidd	$⊢ (φ \land P = C (J)) \to C (J) - C (J) = 0$
91	85 90	eqtrd	$⊢ (φ \land P = C (J)) \to P - C (J) = 0$
92	91	fveq2d	$⊢ (φ \land P = C (J)) \to (P - C (J))! = 0!$
93		fac0	$⊢ 0! = 1$
94	92 93	eqtrdi	$⊢ (φ \land P = C (J)) \to (P - C (J))! = 1$
95	94	oveq2d	$⊢ (φ \land P = C (J)) \to \frac{P!}{(P - C (J))!} = \frac{P!}{1}$
96	9	nncnd	$⊢ φ \to P! \in ℂ$
97	96	div1d	$⊢ φ \to \frac{P!}{1} = P!$
98	97	adantr	$⊢ (φ \land P = C (J)) \to \frac{P!}{1} = P!$
99	95 98	eqtrd	$⊢ (φ \land P = C (J)) \to \frac{P!}{(P - C (J))!} = P!$
100	91	oveq2d	$⊢ (φ \land P = C (J)) \to 0^{P - C (J)} = 0^{0}$
101		0cnd	$⊢ (φ \land P = C (J)) \to 0 \in ℂ$
102	101	exp0d	$⊢ (φ \land P = C (J)) \to 0^{0} = 1$
103	100 102	eqtrd	$⊢ (φ \land P = C (J)) \to 0^{P - C (J)} = 1$
104	99 103	oveq12d	$⊢ (φ \land P = C (J)) \to (\frac{P!}{(P - C (J))!}) 0^{P - C (J)} = P! \cdot 1$
105	96	mulid1d	$⊢ φ \to P! \cdot 1 = P!$
106	105	adantr	$⊢ (φ \land P = C (J)) \to P! \cdot 1 = P!$
107	104 106	eqtrd	$⊢ (φ \land P = C (J)) \to (\frac{P!}{(P - C (J))!}) 0^{P - C (J)} = P!$
108	107	adantlr	$⊢ ((φ \land \neg P < C (J)) \land P = C (J)) \to (\frac{P!}{(P - C (J))!}) 0^{P - C (J)} = P!$
109	83 108	eqtr2d	$⊢ ((φ \land \neg P < C (J)) \land P = C (J)) \to P! = if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
110	81 109	breqtrd	$⊢ ((φ \land \neg P < C (J)) \land P = C (J)) \to P! ∥ if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
111	73	ad2antrr	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to P! ∥ 0$
112		simpr	$⊢ (φ \land \neg P < C (J)) \to \neg P < C (J)$
113	112	adantr	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to \neg P < C (J)$
114	113	iffalsed	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}) = (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}$
115		simpll	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to φ$
116	87	zred	$⊢ φ \to C (J) \in ℝ$
117	116	ad2antrr	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to C (J) \in ℝ$
118	1	nnred	$⊢ φ \to P \in ℝ$
119	118	ad2antrr	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to P \in ℝ$
120	116	adantr	$⊢ (φ \land \neg P < C (J)) \to C (J) \in ℝ$
121	118	adantr	$⊢ (φ \land \neg P < C (J)) \to P \in ℝ$
122	120 121 112	nltled	$⊢ (φ \land \neg P < C (J)) \to C (J) \leq P$
123	122	adantr	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to C (J) \leq P$
124		neqne	$⊢ \neg P = C (J) \to P \neq C (J)$
125	124	adantl	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to P \neq C (J)$
126	117 119 123 125	leneltd	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to C (J) < P$
127	1	nnzd	$⊢ φ \to P \in ℤ$
128	127	adantr	$⊢ (φ \land C (J) < P) \to P \in ℤ$
129	87	adantr	$⊢ (φ \land C (J) < P) \to C (J) \in ℤ$
130	128 129	zsubcld	$⊢ (φ \land C (J) < P) \to P - C (J) \in ℤ$
131		simpr	$⊢ (φ \land C (J) < P) \to C (J) < P$
132	116	adantr	$⊢ (φ \land C (J) < P) \to C (J) \in ℝ$
133	118	adantr	$⊢ (φ \land C (J) < P) \to P \in ℝ$
134	132 133	posdifd	$⊢ (φ \land C (J) < P) \to (C (J) < P \leftrightarrow 0 < P - C (J))$
135	131 134	mpbid	$⊢ (φ \land C (J) < P) \to 0 < P - C (J)$
136		elnnz	$⊢ P - C (J) \in ℕ \leftrightarrow (P - C (J) \in ℤ \land 0 < P - C (J))$
137	130 135 136	sylanbrc	$⊢ (φ \land C (J) < P) \to P - C (J) \in ℕ$
138	137	0expd	$⊢ (φ \land C (J) < P) \to 0^{P - C (J)} = 0$
139	138	oveq2d	$⊢ (φ \land C (J) < P) \to (\frac{P!}{(P - C (J))!}) 0^{P - C (J)} = (\frac{P!}{(P - C (J))!}) \cdot 0$
140	96	adantr	$⊢ (φ \land C (J) < P) \to P! \in ℂ$
141	137	nnnn0d	$⊢ (φ \land C (J) < P) \to P - C (J) \in ℕ_{0}$
142	141	faccld	$⊢ (φ \land C (J) < P) \to (P - C (J))! \in ℕ$
143	142	nncnd	$⊢ (φ \land C (J) < P) \to (P - C (J))! \in ℂ$
144	142	nnne0d	$⊢ (φ \land C (J) < P) \to (P - C (J))! \neq 0$
145	140 143 144	divcld	$⊢ (φ \land C (J) < P) \to \frac{P!}{(P - C (J))!} \in ℂ$
146	145	mul01d	$⊢ (φ \land C (J) < P) \to (\frac{P!}{(P - C (J))!}) \cdot 0 = 0$
147	139 146	eqtrd	$⊢ (φ \land C (J) < P) \to (\frac{P!}{(P - C (J))!}) 0^{P - C (J)} = 0$
148	115 126 147	syl2anc	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to (\frac{P!}{(P - C (J))!}) 0^{P - C (J)} = 0$
149	114 148	eqtr2d	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to 0 = if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
150	111 149	breqtrd	$⊢ ((φ \land \neg P < C (J)) \land \neg P = C (J)) \to P! ∥ if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
151	110 150	pm2.61dan	$⊢ (φ \land \neg P < C (J)) \to P! ∥ if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
152	78 151	pm2.61dan	$⊢ φ \to P! ∥ if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
153	10 60 71 152	dvdsmultr1d	$⊢ φ \to P! ∥ if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}) \prod_{j \in (1 \dots M) ∖ \{J\}} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)})$
154	46	zcnd	$⊢ (φ \land j \in (1 \dots M)) \to if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℂ$
155		fveq2	$⊢ j = J \to C (j) = C (J)$
156	155	breq2d	$⊢ j = J \to (P < C (j) \leftrightarrow P < C (J))$
157	156	adantl	$⊢ (φ \land j = J) \to (P < C (j) \leftrightarrow P < C (J))$
158	155	oveq2d	$⊢ j = J \to P - C (j) = P - C (J)$
159	158	fveq2d	$⊢ j = J \to (P - C (j))! = (P - C (J))!$
160	159	oveq2d	$⊢ j = J \to \frac{P!}{(P - C (j))!} = \frac{P!}{(P - C (J))!}$
161	160	adantl	$⊢ (φ \land j = J) \to \frac{P!}{(P - C (j))!} = \frac{P!}{(P - C (J))!}$
162		oveq2	$⊢ j = J \to J - j = J - J$
163	162 50	sylan9eqr	$⊢ (φ \land j = J) \to J - j = 0$
164	158	adantl	$⊢ (φ \land j = J) \to P - C (j) = P - C (J)$
165	163 164	oveq12d	$⊢ (φ \land j = J) \to {(J - j)}^{P - C (j)} = 0^{P - C (J)}$
166	161 165	oveq12d	$⊢ (φ \land j = J) \to (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)} = (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}$
167	157 166	ifbieq2d	$⊢ (φ \land j = J) \to if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) = if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)})$
168	33 154 7 167	fprodsplit1	$⊢ φ \to \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) = if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) 0^{P - C (J)}) \prod_{j \in (1 \dots M) ∖ \{J\}} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)})$
169	153 168	breqtrrd	$⊢ φ \to P! ∥ \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)})$
170		dvdsmultr2	$⊢ (P! \in ℤ \land (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \in ℤ \land \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ) \to (P! ∥ \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \to P! ∥ (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}))$
171	48 169 170	sylc	$⊢ φ \to P! ∥ (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)})$
172	3	faccld	$⊢ φ \to N! \in ℕ$
173	172	nncnd	$⊢ φ \to N! \in ℂ$
174	4	ffvelrnda	$⊢ (φ \land j \in (0 \dots M)) \to C (j) \in (0 \dots N)$
175	17 174	sseldi	$⊢ (φ \land j \in (0 \dots M)) \to C (j) \in ℕ_{0}$
176	175	faccld	$⊢ (φ \land j \in (0 \dots M)) \to C (j)! \in ℕ$
177	176	nncnd	$⊢ (φ \land j \in (0 \dots M)) \to C (j)! \in ℂ$
178	15 177	fprodcl	$⊢ φ \to \prod_{j = 0}^{M} C (j)! \in ℂ$
179	176	nnne0d	$⊢ (φ \land j \in (0 \dots M)) \to C (j)! \neq 0$
180	15 177 179	fprodn0	$⊢ φ \to \prod_{j = 0}^{M} C (j)! \neq 0$
181	173 178 180	divcld	$⊢ φ \to \frac{N!}{\prod_{j = 0}^{M} C (j)!} \in ℂ$
182	31	zcnd	$⊢ φ \to if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \in ℂ$
183	33 154	fprodcl	$⊢ φ \to \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℂ$
184	181 182 183	mulassd	$⊢ φ \to (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) = (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)})$
185	184 6	eqtr4di	$⊢ φ \to (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) = T$
186	171 185	breqtrd	$⊢ φ \to P! ∥ T$

Metamath Proof Explorer

Theorem etransclem25

Proof