Metamath Proof Explorer

Theorem etransclem7

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

Ref Expression
Hypotheses etransclem7.n 
|- ( ph -> P e. NN )
etransclem7.c 
|- ( ph -> C : ( 0 ... M ) --> ( 0 ... N ) )
etransclem7.j 
|- ( ph -> J e. ( 0 ... M ) )
Assertion etransclem7 
|- ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ )

Proof

Step Hyp Ref Expression
1 etransclem7.n 
 |-  ( ph -> P e. NN )
2 etransclem7.c 
 |-  ( ph -> C : ( 0 ... M ) --> ( 0 ... N ) )
3 etransclem7.j 
 |-  ( ph -> J e. ( 0 ... M ) )
4 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
5 0zd 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ P < ( C ` j ) ) -> 0 e. ZZ )
6 0zd 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> 0 e. ZZ )
7 1 nnzd 
 |-  ( ph -> P e. ZZ )
8 7 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> P e. ZZ )
9 7 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> P e. ZZ )
10 2 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> C : ( 0 ... M ) --> ( 0 ... N ) )
11 0zd 
 |-  ( j e. ( 1 ... M ) -> 0 e. ZZ )
12 fzp1ss 
 |-  ( 0 e. ZZ -> ( ( 0 + 1 ) ... M ) C_ ( 0 ... M ) )
13 11 12 syl 
 |-  ( j e. ( 1 ... M ) -> ( ( 0 + 1 ) ... M ) C_ ( 0 ... M ) )
14 id 
 |-  ( j e. ( 1 ... M ) -> j e. ( 1 ... M ) )
15 1e0p1 
 |-  1 = ( 0 + 1 )
16 15 oveq1i 
 |-  ( 1 ... M ) = ( ( 0 + 1 ) ... M )
17 14 16 eleqtrdi 
 |-  ( j e. ( 1 ... M ) -> j e. ( ( 0 + 1 ) ... M ) )
18 13 17 sseldd 
 |-  ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
19 18 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
20 10 19 ffvelrnd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( C ` j ) e. ( 0 ... N ) )
21 20 elfzelzd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( C ` j ) e. ZZ )
22 9 21 zsubcld 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - ( C ` j ) ) e. ZZ )
23 22 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( P - ( C ` j ) ) e. ZZ )
24 21 zred 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( C ` j ) e. RR )
25 24 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( C ` j ) e. RR )
26 8 zred 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> P e. RR )
27 simpr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> -. P < ( C ` j ) )
28 25 26 27 nltled 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( C ` j ) <_ P )
29 26 25 subge0d 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( 0 <_ ( P - ( C ` j ) ) <-> ( C ` j ) <_ P ) )
30 28 29 mpbird 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> 0 <_ ( P - ( C ` j ) ) )
31 elfzle1 
 |-  ( ( C ` j ) e. ( 0 ... N ) -> 0 <_ ( C ` j ) )
32 20 31 syl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> 0 <_ ( C ` j ) )
33 32 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> 0 <_ ( C ` j ) )
34 26 25 subge02d 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( 0 <_ ( C ` j ) <-> ( P - ( C ` j ) ) <_ P ) )
35 33 34 mpbid 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( P - ( C ` j ) ) <_ P )
36 6 8 23 30 35 elfzd 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( P - ( C ` j ) ) e. ( 0 ... P ) )
37 permnn 
 |-  ( ( P - ( C ` j ) ) e. ( 0 ... P ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) e. NN )
38 36 37 syl 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) e. NN )
39 38 nnzd 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) e. ZZ )
40 3 elfzelzd 
 |-  ( ph -> J e. ZZ )
41 40 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> J e. ZZ )
42 elfzelz 
 |-  ( j e. ( 1 ... M ) -> j e. ZZ )
43 42 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ZZ )
44 41 43 zsubcld 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( J - j ) e. ZZ )
45 44 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( J - j ) e. ZZ )
46 elnn0z 
 |-  ( ( P - ( C ` j ) ) e. NN0 <-> ( ( P - ( C ` j ) ) e. ZZ /\ 0 <_ ( P - ( C ` j ) ) ) )
47 23 30 46 sylanbrc 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( P - ( C ` j ) ) e. NN0 )
48 zexpcl 
 |-  ( ( ( J - j ) e. ZZ /\ ( P - ( C ` j ) ) e. NN0 ) -> ( ( J - j ) ^ ( P - ( C ` j ) ) ) e. ZZ )
49 45 47 48 syl2anc 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( ( J - j ) ^ ( P - ( C ` j ) ) ) e. ZZ )
50 39 49 zmulcld 
 |-  ( ( ( ph /\ j e. ( 1 ... M ) ) /\ -. P < ( C ` j ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) e. ZZ )
51 5 50 ifclda 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ )
52 4 51 fprodzcl 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ )