Theorem etransclem3

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

	Ref	Expression
Hypotheses	etransclem3.n	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem3.c	⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
	etransclem3.j	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
	etransclem3.4	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
Assertion	etransclem3	⊢ ( 𝜑 → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( ( 𝐾 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		etransclem3.n	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2		etransclem3.c	⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
3		etransclem3.j	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
4		etransclem3.4	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
5		0zd	⊢ ( ( 𝜑 ∧ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → 0 ∈ ℤ )
6		0zd	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → 0 ∈ ℤ )
7	1	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
8	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → 𝑃 ∈ ℤ )
9	2 3	ffvelrnd	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ( 0 ... 𝑁 ) )
10	9	elfzelzd	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ℤ )
11	7 10	zsubcld	⊢ ( 𝜑 → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℤ )
12	11	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℤ )
13	10	zred	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
14	13	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
15	8	zred	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → 𝑃 ∈ ℝ )
16		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) )
17	14 15 16	nltled	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ≤ 𝑃 )
18	15 14	subge0d	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ↔ ( 𝐶 ‘ 𝐽 ) ≤ 𝑃 ) )
19	17 18	mpbird	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) )
20		elfzle1	⊢ ( ( 𝐶 ‘ 𝐽 ) ∈ ( 0 ... 𝑁 ) → 0 ≤ ( 𝐶 ‘ 𝐽 ) )
21	9 20	syl	⊢ ( 𝜑 → 0 ≤ ( 𝐶 ‘ 𝐽 ) )
22	1	nnred	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
23	22 13	subge02d	⊢ ( 𝜑 → ( 0 ≤ ( 𝐶 ‘ 𝐽 ) ↔ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ≤ 𝑃 ) )
24	21 23	mpbid	⊢ ( 𝜑 → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ≤ 𝑃 )
25	24	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ≤ 𝑃 )
26	6 8 12 19 25	elfzd	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ( 0 ... 𝑃 ) )
27		permnn	⊢ ( ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ( 0 ... 𝑃 ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ∈ ℕ )
28	26 27	syl	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ∈ ℕ )
29	28	nnzd	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ∈ ℤ )
30	3	elfzelzd	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
31	4 30	zsubcld	⊢ ( 𝜑 → ( 𝐾 − 𝐽 ) ∈ ℤ )
32	31	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝐾 − 𝐽 ) ∈ ℤ )
33		elnn0z	⊢ ( ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℕ0 ↔ ( ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℤ ∧ 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
34	12 19 33	sylanbrc	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℕ0 )
35		zexpcl	⊢ ( ( ( 𝐾 − 𝐽 ) ∈ ℤ ∧ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℕ0 ) → ( ( 𝐾 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ∈ ℤ )
36	32 34 35	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ( 𝐾 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ∈ ℤ )
37	29 36	zmulcld	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( ( 𝐾 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ∈ ℤ )
38	5 37	ifclda	⊢ ( 𝜑 → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( ( 𝐾 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) ∈ ℤ )