# 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( C ` 0 ) e. RR )`
21 8 nn0red
` |-  ( ph -> ( P - 1 ) e. RR )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> J e. ZZ )`
` |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( P - 1 ) - ( C ` 0 ) ) e. ZZ )`
` |-  ( ( ( P - 1 ) - ( C ` 0 ) ) e. NN0 <-> ( ( ( P - 1 ) - ( C ` 0 ) ) e. ZZ /\ 0 <_ ( ( P - 1 ) - ( C ` 0 ) ) ) )`
` |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( P - 1 ) - ( C ` 0 ) ) e. NN0 )`
` |-  ( ( J e. ZZ /\ ( ( P - 1 ) - ( C ` 0 ) ) e. NN0 ) -> ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) e. ZZ )`
` |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) e. ZZ )`
` |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) e. ZZ )`
` |-  ( ph -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) e. ZZ )`