Metamath Proof Explorer

Theorem etransclem15

Description: Value of the term T , when J = 0 and ( C0 ) = P - 1 (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem15.p 
|- ( ph -> P e. NN )
etransclem15.m 
|- ( ph -> M e. NN0 )
etransclem15.n 
|- ( ph -> N e. NN0 )
etransclem15.c 
|- ( ph -> C : ( 0 ... M ) --> ( 0 ... N ) )
etransclem15.t 
|- T = ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. ( if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) )
etransclem15.j 
|- ( ph -> J = 0 )
etransclem15.cpm1 
|- ( ph -> ( C ` 0 ) =/= ( P - 1 ) )
Assertion etransclem15 
|- ( ph -> T = 0 )

Proof

Step Hyp Ref Expression
1 etransclem15.p 
 |-  ( ph -> P e. NN )
2 etransclem15.m 
 |-  ( ph -> M e. NN0 )
3 etransclem15.n 
 |-  ( ph -> N e. NN0 )
4 etransclem15.c 
 |-  ( ph -> C : ( 0 ... M ) --> ( 0 ... N ) )
5 etransclem15.t 
 |-  T = ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. ( if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) )
6 etransclem15.j 
 |-  ( ph -> J = 0 )
7 etransclem15.cpm1 
 |-  ( ph -> ( C ` 0 ) =/= ( P - 1 ) )
8 5 a1i 
 |-  ( ph -> T = ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. ( if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) ) )
9 iftrue 
 |-  ( ( P - 1 ) < ( C ` 0 ) -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) = 0 )
10 9 adantl 
 |-  ( ( ph /\ ( P - 1 ) < ( C ` 0 ) ) -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) = 0 )
11 iffalse 
 |-  ( -. ( P - 1 ) < ( C ` 0 ) -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) )
12 11 adantl 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) )
13 6 oveq1d 
 |-  ( ph -> ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( C ` 0 ) ) ) )
14 13 adantr 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( C ` 0 ) ) ) )
15 1 nnzd 
 |-  ( ph -> P e. ZZ )
16 1zzd 
 |-  ( ph -> 1 e. ZZ )
17 15 16 zsubcld 
 |-  ( ph -> ( P - 1 ) e. ZZ )
18 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
19 2 18 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
20 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
21 19 20 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
22 4 21 ffvelrnd 
 |-  ( ph -> ( C ` 0 ) e. ( 0 ... N ) )
23 22 elfzelzd 
 |-  ( ph -> ( C ` 0 ) e. ZZ )
24 17 23 zsubcld 
 |-  ( ph -> ( ( P - 1 ) - ( C ` 0 ) ) e. ZZ )
25 24 adantr 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( P - 1 ) - ( C ` 0 ) ) e. ZZ )
26 23 zred 
 |-  ( ph -> ( C ` 0 ) e. RR )
27 26 adantr 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( C ` 0 ) e. RR )
28 17 zred 
 |-  ( ph -> ( P - 1 ) e. RR )
29 28 adantr 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( P - 1 ) e. RR )
30 simpr 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> -. ( P - 1 ) < ( C ` 0 ) )
31 27 29 30 nltled 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( C ` 0 ) <_ ( P - 1 ) )
32 7 necomd 
 |-  ( ph -> ( P - 1 ) =/= ( C ` 0 ) )
33 32 adantr 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( P - 1 ) =/= ( C ` 0 ) )
34 27 29 31 33 leneltd 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( C ` 0 ) < ( P - 1 ) )
35 27 29 posdifd 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( C ` 0 ) < ( P - 1 ) <-> 0 < ( ( P - 1 ) - ( C ` 0 ) ) ) )
36 34 35 mpbid 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> 0 < ( ( P - 1 ) - ( C ` 0 ) ) )
37 elnnz 
 |-  ( ( ( P - 1 ) - ( C ` 0 ) ) e. NN <-> ( ( ( P - 1 ) - ( C ` 0 ) ) e. ZZ /\ 0 < ( ( P - 1 ) - ( C ` 0 ) ) ) )
38 25 36 37 sylanbrc 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( P - 1 ) - ( C ` 0 ) ) e. NN )
39 38 0expd 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( 0 ^ ( ( P - 1 ) - ( C ` 0 ) ) ) = 0 )
40 14 39 eqtrd 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) = 0 )
41 40 oveq2d 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. 0 ) )
42 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
43 1 42 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
44 43 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
45 44 nncnd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. CC )
46 45 adantr 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ! ` ( P - 1 ) ) e. CC )
47 38 nnnn0d 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( P - 1 ) - ( C ` 0 ) ) e. NN0 )
48 47 faccld 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) e. NN )
49 48 nncnd 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) e. CC )
50 48 nnne0d 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) =/= 0 )
51 46 49 50 divcld 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) e. CC )
52 51 mul01d 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. 0 ) = 0 )
53 12 41 52 3eqtrd 
 |-  ( ( ph /\ -. ( P - 1 ) < ( C ` 0 ) ) -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) = 0 )
54 10 53 pm2.61dan 
 |-  ( ph -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) = 0 )
55 54 oveq1d 
 |-  ( ph -> ( if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) = ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) )
56 6 21 eqeltrd 
 |-  ( ph -> J e. ( 0 ... M ) )
57 1 4 56 etransclem7 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ )
58 57 zcnd 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. CC )
59 58 mul02d 
 |-  ( ph -> ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) = 0 )
60 55 59 eqtrd 
 |-  ( ph -> ( if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) = 0 )
61 60 oveq2d 
 |-  ( ph -> ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. ( if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) ) = ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. 0 ) )
62 3 faccld 
 |-  ( ph -> ( ! ` N ) e. NN )
63 62 nncnd 
 |-  ( ph -> ( ! ` N ) e. CC )
64 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
65 fzssnn0 
 |-  ( 0 ... N ) C_ NN0
66 4 ffvelrnda 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( C ` j ) e. ( 0 ... N ) )
67 65 66 sseldi 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( C ` j ) e. NN0 )
68 67 faccld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( C ` j ) ) e. NN )
69 68 nncnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( C ` j ) ) e. CC )
70 64 69 fprodcl 
 |-  ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) e. CC )
71 68 nnne0d 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( C ` j ) ) =/= 0 )
72 64 69 71 fprodn0 
 |-  ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) =/= 0 )
73 63 70 72 divcld 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) e. CC )
74 73 mul01d 
 |-  ( ph -> ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. 0 ) = 0 )
75 8 61 74 3eqtrd 
 |-  ( ph -> T = 0 )