etransclem3

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

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

Proof

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

Metamath Proof Explorer

Theorem etransclem3

Proof