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 6 8 12 3jca 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( C ` J ) ) e. ZZ ) )
14 10 zred 
 |-  ( ph -> ( C ` J ) e. RR )
15 14 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( C ` J ) e. RR )
16 8 zred 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> P e. RR )
17 simpr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> -. P < ( C ` J ) )
18 15 16 17 nltled 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( C ` J ) <_ P )
19 16 15 subge0d 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( 0 <_ ( P - ( C ` J ) ) <-> ( C ` J ) <_ P ) )
20 18 19 mpbird 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> 0 <_ ( P - ( C ` J ) ) )
21 elfzle1 
 |-  ( ( C ` J ) e. ( 0 ... N ) -> 0 <_ ( C ` J ) )
22 9 21 syl 
 |-  ( ph -> 0 <_ ( C ` J ) )
23 1 nnred 
 |-  ( ph -> P e. RR )
24 23 14 subge02d 
 |-  ( ph -> ( 0 <_ ( C ` J ) <-> ( P - ( C ` J ) ) <_ P ) )
25 22 24 mpbid 
 |-  ( ph -> ( P - ( C ` J ) ) <_ P )
26 25 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( P - ( C ` J ) ) <_ P )
27 13 20 26 jca32 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( C ` J ) ) e. ZZ ) /\ ( 0 <_ ( P - ( C ` J ) ) /\ ( P - ( C ` J ) ) <_ P ) ) )
28 elfz2 
 |-  ( ( P - ( C ` J ) ) e. ( 0 ... P ) <-> ( ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( C ` J ) ) e. ZZ ) /\ ( 0 <_ ( P - ( C ` J ) ) /\ ( P - ( C ` J ) ) <_ P ) ) )
29 27 28 sylibr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( P - ( C ` J ) ) e. ( 0 ... P ) )
30 permnn 
 |-  ( ( P - ( C ` J ) ) e. ( 0 ... P ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) e. NN )
31 29 30 syl 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) e. NN )
32 31 nnzd 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) e. ZZ )
33 3 elfzelzd 
 |-  ( ph -> J e. ZZ )
34 4 33 zsubcld 
 |-  ( ph -> ( K - J ) e. ZZ )
35 34 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( K - J ) e. ZZ )
36 elnn0z 
 |-  ( ( P - ( C ` J ) ) e. NN0 <-> ( ( P - ( C ` J ) ) e. ZZ /\ 0 <_ ( P - ( C ` J ) ) ) )
37 12 20 36 sylanbrc 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( P - ( C ` J ) ) e. NN0 )
38 zexpcl 
 |-  ( ( ( K - J ) e. ZZ /\ ( P - ( C ` J ) ) e. NN0 ) -> ( ( K - J ) ^ ( P - ( C ` J ) ) ) e. ZZ )
39 35 37 38 syl2anc 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ( K - J ) ^ ( P - ( C ` J ) ) ) e. ZZ )
40 32 39 zmulcld 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( ( K - J ) ^ ( P - ( C ` J ) ) ) ) e. ZZ )
41 5 40 ifclda 
 |-  ( ph -> if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( ( K - J ) ^ ( P - ( C ` J ) ) ) ) ) e. ZZ )