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	ffvelrnd	$⊢ φ \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	6 8 12	3jca	$⊢ (φ \land \neg P < C (J)) \to (0 \in ℤ \land P \in ℤ \land P - C (J) \in ℤ)$
14	10	zred	$⊢ φ \to C (J) \in ℝ$
15	14	adantr	$⊢ (φ \land \neg P < C (J)) \to C (J) \in ℝ$
16	8	zred	$⊢ (φ \land \neg P < C (J)) \to P \in ℝ$
17		simpr	$⊢ (φ \land \neg P < C (J)) \to \neg P < C (J)$
18	15 16 17	nltled	$⊢ (φ \land \neg P < C (J)) \to C (J) \leq P$
19	16 15	subge0d	$⊢ (φ \land \neg P < C (J)) \to (0 \leq P - C (J) \leftrightarrow C (J) \leq P)$
20	18 19	mpbird	$⊢ (φ \land \neg P < C (J)) \to 0 \leq P - C (J)$
21		elfzle1	$⊢ C (J) \in (0 \dots N) \to 0 \leq C (J)$
22	9 21	syl	$⊢ φ \to 0 \leq C (J)$
23	1	nnred	$⊢ φ \to P \in ℝ$
24	23 14	subge02d	$⊢ φ \to (0 \leq C (J) \leftrightarrow P - C (J) \leq P)$
25	22 24	mpbid	$⊢ φ \to P - C (J) \leq P$
26	25	adantr	$⊢ (φ \land \neg P < C (J)) \to P - C (J) \leq P$
27	13 20 26	jca32	$⊢ (φ \land \neg P < C (J)) \to ((0 \in ℤ \land P \in ℤ \land P - C (J) \in ℤ) \land (0 \leq P - C (J) \land P - C (J) \leq P))$
28		elfz2	$⊢ P - C (J) \in (0 \dots P) \leftrightarrow ((0 \in ℤ \land P \in ℤ \land P - C (J) \in ℤ) \land (0 \leq P - C (J) \land P - C (J) \leq P))$
29	27 28	sylibr	$⊢ (φ \land \neg P < C (J)) \to P - C (J) \in (0 \dots P)$
30		permnn	$⊢ P - C (J) \in (0 \dots P) \to \frac{P!}{(P - C (J))!} \in ℕ$
31	29 30	syl	$⊢ (φ \land \neg P < C (J)) \to \frac{P!}{(P - C (J))!} \in ℕ$
32	31	nnzd	$⊢ (φ \land \neg P < C (J)) \to \frac{P!}{(P - C (J))!} \in ℤ$
33	3	elfzelzd	$⊢ φ \to J \in ℤ$
34	4 33	zsubcld	$⊢ φ \to K - J \in ℤ$
35	34	adantr	$⊢ (φ \land \neg P < C (J)) \to K - J \in ℤ$
36		elnn0z	$⊢ P - C (J) \in ℕ_{0} \leftrightarrow (P - C (J) \in ℤ \land 0 \leq P - C (J))$
37	12 20 36	sylanbrc	$⊢ (φ \land \neg P < C (J)) \to P - C (J) \in ℕ_{0}$
38		zexpcl	$⊢ (K - J \in ℤ \land P - C (J) \in ℕ_{0}) \to {(K - J)}^{P - C (J)} \in ℤ$
39	35 37 38	syl2anc	$⊢ (φ \land \neg P < C (J)) \to {(K - J)}^{P - C (J)} \in ℤ$
40	32 39	zmulcld	$⊢ (φ \land \neg P < C (J)) \to (\frac{P!}{(P - C (J))!}) {(K - J)}^{P - C (J)} \in ℤ$
41	5 40	ifclda	$⊢ φ \to if (P < C (J), 0, (\frac{P!}{(P - C (J))!}) {(K - J)}^{P - C (J)}) \in ℤ$

Metamath Proof Explorer

Theorem etransclem3

Proof