# Metamath Proof Explorer

## Theorem etransclem10

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

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

### Proof

Step Hyp Ref Expression
1 etransclem10.n ${⊢}{\phi }\to {P}\in ℕ$
2 etransclem10.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
3 etransclem10.c ${⊢}{\phi }\to {C}:\left(0\dots {M}\right)⟶\left(0\dots {N}\right)$
4 etransclem10.j ${⊢}{\phi }\to {J}\in ℤ$
5 0zd ${⊢}\left({\phi }\wedge {P}-1<{C}\left(0\right)\right)\to 0\in ℤ$
6 0zd ${⊢}{\phi }\to 0\in ℤ$
7 nnm1nn0 ${⊢}{P}\in ℕ\to {P}-1\in {ℕ}_{0}$
8 1 7 syl ${⊢}{\phi }\to {P}-1\in {ℕ}_{0}$
9 8 nn0zd ${⊢}{\phi }\to {P}-1\in ℤ$
10 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
11 2 10 eleqtrdi ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
12 eluzfz1 ${⊢}{M}\in {ℤ}_{\ge 0}\to 0\in \left(0\dots {M}\right)$
13 11 12 syl ${⊢}{\phi }\to 0\in \left(0\dots {M}\right)$
14 3 13 ffvelrnd ${⊢}{\phi }\to {C}\left(0\right)\in \left(0\dots {N}\right)$
15 14 elfzelzd ${⊢}{\phi }\to {C}\left(0\right)\in ℤ$
16 9 15 zsubcld ${⊢}{\phi }\to {P}-1-{C}\left(0\right)\in ℤ$
17 6 9 16 3jca ${⊢}{\phi }\to \left(0\in ℤ\wedge {P}-1\in ℤ\wedge {P}-1-{C}\left(0\right)\in ℤ\right)$
18 17 adantr ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to \left(0\in ℤ\wedge {P}-1\in ℤ\wedge {P}-1-{C}\left(0\right)\in ℤ\right)$
19 15 zred ${⊢}{\phi }\to {C}\left(0\right)\in ℝ$
20 19 adantr ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to {C}\left(0\right)\in ℝ$
21 8 nn0red ${⊢}{\phi }\to {P}-1\in ℝ$
22 21 adantr ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to {P}-1\in ℝ$
23 simpr ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to ¬{P}-1<{C}\left(0\right)$
24 20 22 23 nltled ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to {C}\left(0\right)\le {P}-1$
25 22 20 subge0d ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to \left(0\le {P}-1-{C}\left(0\right)↔{C}\left(0\right)\le {P}-1\right)$
26 24 25 mpbird ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to 0\le {P}-1-{C}\left(0\right)$
27 elfzle1 ${⊢}{C}\left(0\right)\in \left(0\dots {N}\right)\to 0\le {C}\left(0\right)$
28 14 27 syl ${⊢}{\phi }\to 0\le {C}\left(0\right)$
29 28 adantr ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to 0\le {C}\left(0\right)$
30 22 20 subge02d ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to \left(0\le {C}\left(0\right)↔{P}-1-{C}\left(0\right)\le {P}-1\right)$
31 29 30 mpbid ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to {P}-1-{C}\left(0\right)\le {P}-1$
32 18 26 31 jca32 ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to \left(\left(0\in ℤ\wedge {P}-1\in ℤ\wedge {P}-1-{C}\left(0\right)\in ℤ\right)\wedge \left(0\le {P}-1-{C}\left(0\right)\wedge {P}-1-{C}\left(0\right)\le {P}-1\right)\right)$
33 elfz2 ${⊢}{P}-1-{C}\left(0\right)\in \left(0\dots {P}-1\right)↔\left(\left(0\in ℤ\wedge {P}-1\in ℤ\wedge {P}-1-{C}\left(0\right)\in ℤ\right)\wedge \left(0\le {P}-1-{C}\left(0\right)\wedge {P}-1-{C}\left(0\right)\le {P}-1\right)\right)$
34 32 33 sylibr ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to {P}-1-{C}\left(0\right)\in \left(0\dots {P}-1\right)$
35 permnn ${⊢}{P}-1-{C}\left(0\right)\in \left(0\dots {P}-1\right)\to \frac{\left({P}-1\right)!}{\left({P}-1-{C}\left(0\right)\right)!}\in ℕ$
36 34 35 syl ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to \frac{\left({P}-1\right)!}{\left({P}-1-{C}\left(0\right)\right)!}\in ℕ$
37 36 nnzd ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to \frac{\left({P}-1\right)!}{\left({P}-1-{C}\left(0\right)\right)!}\in ℤ$
38 4 adantr ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to {J}\in ℤ$
39 16 adantr ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to {P}-1-{C}\left(0\right)\in ℤ$
40 elnn0z ${⊢}{P}-1-{C}\left(0\right)\in {ℕ}_{0}↔\left({P}-1-{C}\left(0\right)\in ℤ\wedge 0\le {P}-1-{C}\left(0\right)\right)$
41 39 26 40 sylanbrc ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to {P}-1-{C}\left(0\right)\in {ℕ}_{0}$
42 zexpcl ${⊢}\left({J}\in ℤ\wedge {P}-1-{C}\left(0\right)\in {ℕ}_{0}\right)\to {{J}}^{{P}-1-{C}\left(0\right)}\in ℤ$
43 38 41 42 syl2anc ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to {{J}}^{{P}-1-{C}\left(0\right)}\in ℤ$
44 37 43 zmulcld ${⊢}\left({\phi }\wedge ¬{P}-1<{C}\left(0\right)\right)\to \left(\frac{\left({P}-1\right)!}{\left({P}-1-{C}\left(0\right)\right)!}\right){{J}}^{{P}-1-{C}\left(0\right)}\in ℤ$
45 5 44 ifclda ${⊢}{\phi }\to if\left({P}-1<{C}\left(0\right),0,\left(\frac{\left({P}-1\right)!}{\left({P}-1-{C}\left(0\right)\right)!}\right){{J}}^{{P}-1-{C}\left(0\right)}\right)\in ℤ$