etransclem15

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

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

Proof

Step	Hyp	Ref	Expression
1		etransclem15.p	$⊢ φ \to P \in ℕ$
2		etransclem15.m	$⊢ φ \to M \in ℕ_{0}$
3		etransclem15.n	$⊢ φ \to N \in ℕ_{0}$
4		etransclem15.c	$⊢ φ \to C : (0 \dots M) ⟶ (0 \dots N)$
5		etransclem15.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)})$
6		etransclem15.j	$⊢ φ \to J = 0$
7		etransclem15.cpm1	$⊢ φ \to C (0) \neq P - 1$
8	5	a1i	$⊢ φ \to 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)})$
9		iftrue	$⊢ P - 1 < C (0) \to if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) = 0$
10	9	adantl	$⊢ (φ \land P - 1 < C (0)) \to if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) = 0$
11		iffalse	$⊢ \neg P - 1 < C (0) \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)}$
12	11	adantl	$⊢ (φ \land \neg P - 1 < C (0)) \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)}$
13	6	oveq1d	$⊢ φ \to J^{P - 1 - C (0)} = 0^{P - 1 - C (0)}$
14	13	adantr	$⊢ (φ \land \neg P - 1 < C (0)) \to J^{P - 1 - C (0)} = 0^{P - 1 - C (0)}$
15	1	nnzd	$⊢ φ \to P \in ℤ$
16		1zzd	$⊢ φ \to 1 \in ℤ$
17	15 16	zsubcld	$⊢ φ \to P - 1 \in ℤ$
18		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
19	2 18	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
20		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
21	19 20	syl	$⊢ φ \to 0 \in (0 \dots M)$
22	4 21	ffvelcdmd	$⊢ φ \to C (0) \in (0 \dots N)$
23	22	elfzelzd	$⊢ φ \to C (0) \in ℤ$
24	17 23	zsubcld	$⊢ φ \to P - 1 - C (0) \in ℤ$
25	24	adantr	$⊢ (φ \land \neg P - 1 < C (0)) \to P - 1 - C (0) \in ℤ$
26	23	zred	$⊢ φ \to C (0) \in ℝ$
27	26	adantr	$⊢ (φ \land \neg P - 1 < C (0)) \to C (0) \in ℝ$
28	17	zred	$⊢ φ \to P - 1 \in ℝ$
29	28	adantr	$⊢ (φ \land \neg P - 1 < C (0)) \to P - 1 \in ℝ$
30		simpr	$⊢ (φ \land \neg P - 1 < C (0)) \to \neg P - 1 < C (0)$
31	27 29 30	nltled	$⊢ (φ \land \neg P - 1 < C (0)) \to C (0) \leq P - 1$
32	7	necomd	$⊢ φ \to P - 1 \neq C (0)$
33	32	adantr	$⊢ (φ \land \neg P - 1 < C (0)) \to P - 1 \neq C (0)$
34	27 29 31 33	leneltd	$⊢ (φ \land \neg P - 1 < C (0)) \to C (0) < P - 1$
35	27 29	posdifd	$⊢ (φ \land \neg P - 1 < C (0)) \to (C (0) < P - 1 \leftrightarrow 0 < P - 1 - C (0))$
36	34 35	mpbid	$⊢ (φ \land \neg P - 1 < C (0)) \to 0 < P - 1 - C (0)$
37		elnnz	$⊢ P - 1 - C (0) \in ℕ \leftrightarrow (P - 1 - C (0) \in ℤ \land 0 < P - 1 - C (0))$
38	25 36 37	sylanbrc	$⊢ (φ \land \neg P - 1 < C (0)) \to P - 1 - C (0) \in ℕ$
39	38	0expd	$⊢ (φ \land \neg P - 1 < C (0)) \to 0^{P - 1 - C (0)} = 0$
40	14 39	eqtrd	$⊢ (φ \land \neg P - 1 < C (0)) \to J^{P - 1 - C (0)} = 0$
41	40	oveq2d	$⊢ (φ \land \neg P - 1 < C (0)) \to (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)} = (\frac{(P - 1)!}{(P - 1 - C (0))!}) \cdot 0$
42		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
43	1 42	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
44	43	faccld	$⊢ φ \to (P - 1)! \in ℕ$
45	44	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
46	45	adantr	$⊢ (φ \land \neg P - 1 < C (0)) \to (P - 1)! \in ℂ$
47	38	nnnn0d	$⊢ (φ \land \neg P - 1 < C (0)) \to P - 1 - C (0) \in ℕ_{0}$
48	47	faccld	$⊢ (φ \land \neg P - 1 < C (0)) \to (P - 1 - C (0))! \in ℕ$
49	48	nncnd	$⊢ (φ \land \neg P - 1 < C (0)) \to (P - 1 - C (0))! \in ℂ$
50	48	nnne0d	$⊢ (φ \land \neg P - 1 < C (0)) \to (P - 1 - C (0))! \neq 0$
51	46 49 50	divcld	$⊢ (φ \land \neg P - 1 < C (0)) \to \frac{(P - 1)!}{(P - 1 - C (0))!} \in ℂ$
52	51	mul01d	$⊢ (φ \land \neg P - 1 < C (0)) \to (\frac{(P - 1)!}{(P - 1 - C (0))!}) \cdot 0 = 0$
53	12 41 52	3eqtrd	$⊢ (φ \land \neg P - 1 < C (0)) \to if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) = 0$
54	10 53	pm2.61dan	$⊢ φ \to if (P - 1 < C (0), 0, (\frac{(P - 1)!}{(P - 1 - C (0))!}) J^{P - 1 - C (0)}) = 0$
55	54	oveq1d	$⊢ φ \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)}) = 0 \cdot \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)})$
56	6 21	eqeltrd	$⊢ φ \to J \in (0 \dots M)$
57	1 4 56	etransclem7	$⊢ φ \to \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ$
58	57	zcnd	$⊢ φ \to \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℂ$
59	58	mul02d	$⊢ φ \to 0 \cdot \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) = 0$
60	55 59	eqtrd	$⊢ φ \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)}) = 0$
61	60	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)!}) \cdot 0$
62	3	faccld	$⊢ φ \to N! \in ℕ$
63	62	nncnd	$⊢ φ \to N! \in ℂ$
64		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
65		fzssnn0	$⊢ (0 \dots N) \subseteq ℕ_{0}$
66	4	ffvelcdmda	$⊢ (φ \land j \in (0 \dots M)) \to C (j) \in (0 \dots N)$
67	65 66	sselid	$⊢ (φ \land j \in (0 \dots M)) \to C (j) \in ℕ_{0}$
68	67	faccld	$⊢ (φ \land j \in (0 \dots M)) \to C (j)! \in ℕ$
69	68	nncnd	$⊢ (φ \land j \in (0 \dots M)) \to C (j)! \in ℂ$
70	64 69	fprodcl	$⊢ φ \to \prod_{j = 0}^{M} C (j)! \in ℂ$
71	68	nnne0d	$⊢ (φ \land j \in (0 \dots M)) \to C (j)! \neq 0$
72	64 69 71	fprodn0	$⊢ φ \to \prod_{j = 0}^{M} C (j)! \neq 0$
73	63 70 72	divcld	$⊢ φ \to \frac{N!}{\prod_{j = 0}^{M} C (j)!} \in ℂ$
74	73	mul01d	$⊢ φ \to (\frac{N!}{\prod_{j = 0}^{M} C (j)!}) \cdot 0 = 0$
75	8 61 74	3eqtrd	$⊢ φ \to T = 0$

Metamath Proof Explorer

Theorem etransclem15

Proof