etransclem10

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

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

Proof

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

Metamath Proof Explorer

Theorem etransclem10

Proof