# Metamath Proof Explorer

## Theorem etransclem7

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

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

### Proof

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