Metamath Proof Explorer

Theorem etransclem3

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

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

Proof

Step Hyp Ref Expression
1 etransclem3.n 
 |-  ( ph -> P e. NN )
2 etransclem3.c 
 |-  ( ph -> C : ( 0 ... M ) --> ( 0 ... N ) )
3 etransclem3.j 
 |-  ( ph -> J e. ( 0 ... M ) )
4 etransclem3.4 
 |-  ( ph -> K e. ZZ )
5 0zd 
 |-  ( ( ph /\ P < ( C ` J ) ) -> 0 e. ZZ )
6 0zd 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> 0 e. ZZ )
7 1 nnzd 
 |-  ( ph -> P e. ZZ )
8 7 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> P e. ZZ )
9 2 3 ffvelrnd 
 |-  ( ph -> ( C ` J ) e. ( 0 ... N ) )
10 9 elfzelzd 
 |-  ( ph -> ( C ` J ) e. ZZ )
11 7 10 zsubcld 
 |-  ( ph -> ( P - ( C ` J ) ) e. ZZ )
12 11 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( P - ( C ` J ) ) e. ZZ )
13 10 zred 
 |-  ( ph -> ( C ` J ) e. RR )
14 13 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( C ` J ) e. RR )
15 8 zred 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> P e. RR )
16 simpr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> -. P < ( C ` J ) )
17 14 15 16 nltled 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( C ` J ) <_ P )
18 15 14 subge0d 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( 0 <_ ( P - ( C ` J ) ) <-> ( C ` J ) <_ P ) )
19 17 18 mpbird 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> 0 <_ ( P - ( C ` J ) ) )
20 elfzle1 
 |-  ( ( C ` J ) e. ( 0 ... N ) -> 0 <_ ( C ` J ) )
21 9 20 syl 
 |-  ( ph -> 0 <_ ( C ` J ) )
22 1 nnred 
 |-  ( ph -> P e. RR )
23 22 13 subge02d 
 |-  ( ph -> ( 0 <_ ( C ` J ) <-> ( P - ( C ` J ) ) <_ P ) )
24 21 23 mpbid 
 |-  ( ph -> ( P - ( C ` J ) ) <_ P )
25 24 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( P - ( C ` J ) ) <_ P )
26 6 8 12 19 25 elfzd 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( P - ( C ` J ) ) e. ( 0 ... P ) )
27 permnn 
 |-  ( ( P - ( C ` J ) ) e. ( 0 ... P ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) e. NN )
28 26 27 syl 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) e. NN )
29 28 nnzd 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) e. ZZ )
30 3 elfzelzd 
 |-  ( ph -> J e. ZZ )
31 4 30 zsubcld 
 |-  ( ph -> ( K - J ) e. ZZ )
32 31 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( K - J ) e. ZZ )
33 elnn0z 
 |-  ( ( P - ( C ` J ) ) e. NN0 <-> ( ( P - ( C ` J ) ) e. ZZ /\ 0 <_ ( P - ( C ` J ) ) ) )
34 12 19 33 sylanbrc 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( P - ( C ` J ) ) e. NN0 )
35 zexpcl 
 |-  ( ( ( K - J ) e. ZZ /\ ( P - ( C ` J ) ) e. NN0 ) -> ( ( K - J ) ^ ( P - ( C ` J ) ) ) e. ZZ )
36 32 34 35 syl2anc 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ( K - J ) ^ ( P - ( C ` J ) ) ) e. ZZ )
37 29 36 zmulcld 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( ( K - J ) ^ ( P - ( C ` J ) ) ) ) e. ZZ )
38 5 37 ifclda 
 |-  ( ph -> if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( ( K - J ) ^ ( P - ( C ` J ) ) ) ) ) e. ZZ )