Metamath Proof Explorer

Theorem etransclem10

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

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

Proof

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