Metamath Proof Explorer

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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )