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	ffvelrnd	$⊢ (φ \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	6 8 23	3jca	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to (0 \in ℤ \land P \in ℤ \land P - C (j) \in ℤ)$
25	21	zred	$⊢ (φ \land j \in (1 \dots M)) \to C (j) \in ℝ$
26	25	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to C (j) \in ℝ$
27	8	zred	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P \in ℝ$
28		simpr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to \neg P < C (j)$
29	26 27 28	nltled	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to C (j) \leq P$
30	27 26	subge0d	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to (0 \leq P - C (j) \leftrightarrow C (j) \leq P)$
31	29 30	mpbird	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to 0 \leq P - C (j)$
32		elfzle1	$⊢ C (j) \in (0 \dots N) \to 0 \leq C (j)$
33	20 32	syl	$⊢ (φ \land j \in (1 \dots M)) \to 0 \leq C (j)$
34	33	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to 0 \leq C (j)$
35	27 26	subge02d	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to (0 \leq C (j) \leftrightarrow P - C (j) \leq P)$
36	34 35	mpbid	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P - C (j) \leq P$
37	24 31 36	jca32	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to ((0 \in ℤ \land P \in ℤ \land P - C (j) \in ℤ) \land (0 \leq P - C (j) \land P - C (j) \leq P))$
38		elfz2	$⊢ P - C (j) \in (0 \dots P) \leftrightarrow ((0 \in ℤ \land P \in ℤ \land P - C (j) \in ℤ) \land (0 \leq P - C (j) \land P - C (j) \leq P))$
39	37 38	sylibr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P - C (j) \in (0 \dots P)$
40		permnn	$⊢ P - C (j) \in (0 \dots P) \to \frac{P!}{(P - C (j))!} \in ℕ$
41	39 40	syl	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to \frac{P!}{(P - C (j))!} \in ℕ$
42	41	nnzd	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to \frac{P!}{(P - C (j))!} \in ℤ$
43	3	elfzelzd	$⊢ φ \to J \in ℤ$
44	43	adantr	$⊢ (φ \land j \in (1 \dots M)) \to J \in ℤ$
45		elfzelz	$⊢ j \in (1 \dots M) \to j \in ℤ$
46	45	adantl	$⊢ (φ \land j \in (1 \dots M)) \to j \in ℤ$
47	44 46	zsubcld	$⊢ (φ \land j \in (1 \dots M)) \to J - j \in ℤ$
48	47	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to J - j \in ℤ$
49		elnn0z	$⊢ P - C (j) \in ℕ_{0} \leftrightarrow (P - C (j) \in ℤ \land 0 \leq P - C (j))$
50	23 31 49	sylanbrc	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to P - C (j) \in ℕ_{0}$
51		zexpcl	$⊢ (J - j \in ℤ \land P - C (j) \in ℕ_{0}) \to {(J - j)}^{P - C (j)} \in ℤ$
52	48 50 51	syl2anc	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to {(J - j)}^{P - C (j)} \in ℤ$
53	42 52	zmulcld	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P < C (j)) \to (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)} \in ℤ$
54	5 53	ifclda	$⊢ (φ \land j \in (1 \dots M)) \to if (P < C (j), 0, (\frac{P!}{(P - C (j))!}) {(J - j)}^{P - C (j)}) \in ℤ$
55	4 54	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