etransclem7

Description: The given product is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem7.n	$⊢ φ \to P \in ℕ$
	etransclem7.c	$⊢ φ \to C : (0 \dots M) ⟶ (0 \dots N)$
	etransclem7.j	$⊢ φ \to J \in (0 \dots M)$
Assertion	etransclem7	$⊢ φ \to \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		etransclem7.n	$⊢ φ \to P \in ℕ$
2		etransclem7.c	$⊢ φ \to C : (0 \dots M) ⟶ (0 \dots N)$
3		etransclem7.j	$⊢ φ \to J \in (0 \dots M)$
4		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
5		0zd	$⊢ ((φ \land j \in (1 \dots M)) \land P < C (j)) \to 0 \in ℤ$
6		0zd	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to 0 \in ℤ$
7	1	nnzd	$⊢ φ \to P \in ℤ$
8	7	ad2antrr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P \in ℤ$
9	7	adantr	$⊢ (φ \land j \in (1 \dots M)) \to P \in ℤ$
10	2	adantr	$⊢ (φ \land j \in (1 \dots M)) \to C : (0 \dots M) ⟶ (0 \dots N)$
11		0zd	$⊢ j \in (1 \dots M) \to 0 \in ℤ$
12		fzp1ss	$⊢ 0 \in ℤ \to (0 + 1 \dots M) \subseteq (0 \dots M)$
13	11 12	syl	$⊢ j \in (1 \dots M) \to (0 + 1 \dots M) \subseteq (0 \dots M)$
14		id	$⊢ j \in (1 \dots M) \to j \in (1 \dots M)$
15		1e0p1	$⊢ 1 = 0 + 1$
16	15	oveq1i	$⊢ (1 \dots M) = (0 + 1 \dots M)$
17	14 16	eleqtrdi	$⊢ j \in (1 \dots M) \to j \in (0 + 1 \dots M)$
18	13 17	sseldd	$⊢ j \in (1 \dots M) \to j \in (0 \dots M)$
19	18	adantl	$⊢ (φ \land j \in (1 \dots M)) \to j \in (0 \dots M)$
20	10 19	ffvelcdmd	$⊢ (φ \land j \in (1 \dots M)) \to C (j) \in (0 \dots N)$
21	20	elfzelzd	$⊢ (φ \land j \in (1 \dots M)) \to C (j) \in ℤ$
22	9 21	zsubcld	$⊢ (φ \land j \in (1 \dots M)) \to P - C (j) \in ℤ$
23	22	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P - C (j) \in ℤ$
24	21	zred	$⊢ (φ \land j \in (1 \dots M)) \to C (j) \in ℝ$
25	24	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to C (j) \in ℝ$
26	8	zred	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P \in ℝ$
27		simpr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to \neg P < C (j)$
28	25 26 27	nltled	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to C (j) \leq P$
29	26 25	subge0d	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to (0 \leq P - C (j) \leftrightarrow C (j) \leq P)$
30	28 29	mpbird	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to 0 \leq P - C (j)$
31		elfzle1	$⊢ C (j) \in (0 \dots N) \to 0 \leq C (j)$
32	20 31	syl	$⊢ (φ \land j \in (1 \dots M)) \to 0 \leq C (j)$
33	32	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to 0 \leq C (j)$
34	26 25	subge02d	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to (0 \leq C (j) \leftrightarrow P - C (j) \leq P)$
35	33 34	mpbid	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P - C (j) \leq P$
36	6 8 23 30 35	elfzd	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P - C (j) \in (0 \dots P)$
37		permnn	$⊢ P - C (j) \in (0 \dots P) \to \frac{P!}{(P - C (j))!} \in ℕ$
38	36 37	syl	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to \frac{P!}{(P - C (j))!} \in ℕ$
39	38	nnzd	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to \frac{P!}{(P - C (j))!} \in ℤ$
40	3	elfzelzd	$⊢ φ \to J \in ℤ$
41	40	adantr	$⊢ (φ \land j \in (1 \dots M)) \to J \in ℤ$
42		elfzelz	$⊢ j \in (1 \dots M) \to j \in ℤ$
43	42	adantl	$⊢ (φ \land j \in (1 \dots M)) \to j \in ℤ$
44	41 43	zsubcld	$⊢ (φ \land j \in (1 \dots M)) \to J - j \in ℤ$
45	44	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to J - j \in ℤ$
46		elnn0z	$⊢ P - C (j) \in ℕ_{0} \leftrightarrow (P - C (j) \in ℤ \land 0 \leq P - C (j))$
47	23 30 46	sylanbrc	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P - C (j) \in ℕ_{0}$
48		zexpcl	$⊢ (J - j \in ℤ \land P - C (j) \in ℕ_{0}) \to {(J - j)}^{P - C (j)} \in ℤ$
49	45 47 48	syl2anc	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to {(J - j)}^{P - C (j)} \in ℤ$
50	39 49	zmulcld	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)} \in ℤ$
51	5 50	ifclda	$⊢ (φ \land j \in (1 \dots M)) \to if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ$
52	4 51	fprodzcl	$⊢ φ \to \prod_{j = 1}^{M} if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ$

Metamath Proof Explorer

Theorem etransclem7

Proof