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 6 8 23 3jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℤ ) )
25 21 zred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ )
26 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ )
27 8 zred ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → 𝑃 ∈ ℝ )
28 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) )
29 26 27 28 nltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝐶 ‘ 𝑗 ) ≤ 𝑃 )
30 27 26 subge0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ↔ ( 𝐶 ‘ 𝑗 ) ≤ 𝑃 ) )
31 29 30 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) )
32 elfzle1 ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) → 0 ≤ ( 𝐶 ‘ 𝑗 ) )
33 20 32 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( 𝐶 ‘ 𝑗 ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → 0 ≤ ( 𝐶 ‘ 𝑗 ) )
35 27 26 subge02d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 0 ≤ ( 𝐶 ‘ 𝑗 ) ↔ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ≤ 𝑃 ) )
36 34 35 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ≤ 𝑃 )
37 24 31 36 jca32 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( ( 0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℤ ) ∧ ( 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∧ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ≤ 𝑃 ) ) )
38 elfz2 ⊢ ( ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ( 0 ... 𝑃 ) ↔ ( ( 0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℤ ) ∧ ( 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∧ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ≤ 𝑃 ) ) )
39 37 38 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ( 0 ... 𝑃 ) )
40 permnn ⊢ ( ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ( 0 ... 𝑃 ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ∈ ℕ )
41 39 40 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ∈ ℕ )
42 41 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ∈ ℤ )
43 3 elfzelzd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐽 ∈ ℤ )
45 elfzelz ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℤ )
46 45 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ℤ )
47 44 46 zsubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐽 − 𝑗 ) ∈ ℤ )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝐽 − 𝑗 ) ∈ ℤ )
49 elnn0z ⊢ ( ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℕ0 ↔ ( ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℤ ∧ 0 ≤ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) )
50 23 31 49 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℕ0 )
51 zexpcl ⊢ ( ( ( 𝐽 − 𝑗 ) ∈ ℤ ∧ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ∈ ℕ0 ) → ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℤ )
52 48 50 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℤ )
53 42 52 zmulcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝑗 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ∈ ℤ )
54 5 53 ifclda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
55 4 54 fprodzcl ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )