Theorem etransclem7

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

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

Proof

Step	Hyp	Ref	Expression
1		etransclem7.n	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2		etransclem7.c	⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
3		etransclem7.j	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
4		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
5		0zd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → 0 ∈ ℤ )
6		0zd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → 0 ∈ ℤ )
7	1	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
8	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → 𝑃 ∈ ℤ )
9	7	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℤ )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
11		0zd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 ∈ ℤ )
12		fzp1ss	⊢ ( 0 ∈ ℤ → ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
13	11 12	syl	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
14		id	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
15		1e0p1	⊢ 1 = ( 0 + 1 )
16	15	oveq1i	⊢ ( 1 ... 𝑀 ) = ( ( 0 + 1 ) ... 𝑀 )
17	14 16	eleqtrdi	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) )
18	13 17	sseldd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
20	10 19	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) )
21	20	elfzelzd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℤ )
22	9 21	zsubcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℤ )
23	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℤ )
24	21	zred	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ )
26	8	zred	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → 𝑃 ∈ ℝ )
27		simpr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) )
28	25 26 27	nltled	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝐶 ‘ 𝑗 ) ≤ 𝑃 )
29	26 25	subge0d	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ↔ ( 𝐶 ‘ 𝑗 ) ≤ 𝑃 ) )
30	28 29	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) )
31		elfzle1	⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) → 0 ≤ ( 𝐶 ‘ 𝑗 ) )
32	20 31	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( 𝐶 ‘ 𝑗 ) )
33	32	adantr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → 0 ≤ ( 𝐶 ‘ 𝑗 ) )
34	26 25	subge02d	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 0 ≤ ( 𝐶 ‘ 𝑗 ) ↔ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ≤ 𝑃 ) )
35	33 34	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ≤ 𝑃 )
36	6 8 23 30 35	elfzd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ( 0 ... 𝑃 ) )
37		permnn	⊢ ( ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ( 0 ... 𝑃 ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ∈ ℕ )
38	36 37	syl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ∈ ℕ )
39	38	nnzd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ∈ ℤ )
40	3	elfzelzd	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐽 ∈ ℤ )
42		elfzelz	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℤ )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ℤ )
44	41 43	zsubcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐽 − 𝑗 ) ∈ ℤ )
45	44	adantr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝐽 − 𝑗 ) ∈ ℤ )
46		elnn0z	⊢ ( ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℕ0 ↔ ( ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℤ ∧ 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) )
47	23 30 46	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℕ0 )
48		zexpcl	⊢ ( ( ( 𝐽 − 𝑗 ) ∈ ℤ ∧ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℕ0 ) → ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℤ )
49	45 47 48	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℤ )
50	39 49	zmulcld	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ∈ ℤ )
51	5 50	ifclda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
52	4 51	fprodzcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )