etransclem14

Description: Value of the term T , when J = 0 and ( C0 ) = P - 1 (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem14.n	$⊢ φ \to P \in ℕ$
	etransclem14.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem14.c	$⊢ φ \to C : (0 \dots M) ⟶ (0 \dots N)$
	etransclem14.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)})$
	etransclem14.j	$⊢ φ \to J = 0$
	etransclem14.cpm1	$⊢ φ \to C (0) = P - 1$
Assertion	etransclem14	$⊢ φ \to T = (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(- j)}^{P - C (j)})$

Proof

Step	Hyp	Ref	Expression
1		etransclem14.n	$⊢ φ \to P \in ℕ$
2		etransclem14.m	$⊢ φ \to M \in ℕ_{0}$
3		etransclem14.c	$⊢ φ \to C : (0 \dots M) ⟶ (0 \dots N)$
4		etransclem14.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)})$
5		etransclem14.j	$⊢ φ \to J = 0$
6		etransclem14.cpm1	$⊢ φ \to C (0) = P - 1$
7		fzssre	$⊢ (0 \dots N) \subseteq ℝ$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9	2 8	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
10		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
11	9 10	syl	$⊢ φ \to 0 \in (0 \dots M)$
12	3 11	ffvelrnd	$⊢ φ \to C (0) \in (0 \dots N)$
13	7 12	sseldi	$⊢ φ \to C (0) \in ℝ$
14	6 13	eqeltrrd	$⊢ φ \to P - 1 \in ℝ$
15	13 14	lttri3d	$⊢ φ \to (C (0) = P - 1 \leftrightarrow (\neg C (0) < P - 1 \land \neg P - 1 < C (0)))$
16	6 15	mpbid	$⊢ φ \to (\neg C (0) < P - 1 \land \neg P - 1 < C (0))$
17	16	simprd	$⊢ φ \to \neg P - 1 < C (0)$
18	17	iffalsed	$⊢ φ \to if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) = (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}$
19	14	recnd	$⊢ φ \to P - 1 \in ℂ$
20	6	eqcomd	$⊢ φ \to P - 1 = C (0)$
21	19 20	subeq0bd	$⊢ φ \to P - 1 - C (0) = 0$
22	21	fveq2d	$⊢ φ \to (P - 1 - C (0))! = 0!$
23		fac0	$⊢ 0! = 1$
24	22 23	eqtrdi	$⊢ φ \to (P - 1 - C (0))! = 1$
25	24	oveq2d	$⊢ φ \to \frac{(P - 1)!}{(P - 1 - C (0))!} = \frac{(P - 1)!}{1}$
26		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
27	1 26	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
28	27	faccld	$⊢ φ \to (P - 1)! \in ℕ$
29	28	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
30	29	div1d	$⊢ φ \to \frac{(P - 1)!}{1} = (P - 1)!$
31	25 30	eqtrd	$⊢ φ \to \frac{(P - 1)!}{(P - 1 - C (0))!} = (P - 1)!$
32	5 21	oveq12d	$⊢ φ \to J^{P - 1 - C (0)} = 0^{0}$
33		0exp0e1	$⊢ 0^{0} = 1$
34	32 33	eqtrdi	$⊢ φ \to J^{P - 1 - C (0)} = 1$
35	31 34	oveq12d	$⊢ φ \to (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)} = (P - 1)! \cdot 1$
36	29	mulid1d	$⊢ φ \to (P - 1)! \cdot 1 = (P - 1)!$
37	18 35 36	3eqtrd	$⊢ φ \to if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) = (P - 1)!$
38	5	oveq1d	$⊢ φ \to J - j = 0 - j$
39		df-neg	$⊢ - j = 0 - j$
40	38 39	eqtr4di	$⊢ φ \to J - j = - j$
41	40	oveq1d	$⊢ φ \to {(J - j)}^{P - C (j)} = {(- j)}^{P - C (j)}$
42	41	oveq2d	$⊢ φ \to (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)} = (\frac{P!}{(P - C (j))!}) {(- j)}^{P - C (j)}$
43	42	ifeq2d	$⊢ φ \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))!}) {(- j)}^{P - C (j)})$
44	43	prodeq2ad	$⊢ φ \to \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) = \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(- j)}^{P - C (j)})$
45	37 44	oveq12d	$⊢ φ \to 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)}) = (P - 1)! \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(- j)}^{P - C (j)})$
46	45	oveq2d	$⊢ φ \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)!}) (P - 1)! \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(- j)}^{P - C (j)})$
47	4 46	syl5eq	$⊢ φ \to T = (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) (P - 1)! \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(- j)}^{P - C (j)})$

Metamath Proof Explorer

Theorem etransclem14

Proof