# Metamath Proof Explorer

## Theorem etransclem3

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

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

### Proof

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