Metamath Proof Explorer

Theorem etransclem14

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

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

Proof

Step Hyp Ref Expression
1 etransclem14.n 
 |-  ( ph -> P e. NN )
2 etransclem14.m 
 |-  ( ph -> M e. NN0 )
3 etransclem14.c 
 |-  ( ph -> C : ( 0 ... M ) --> ( 0 ... N ) )
4 etransclem14.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 ) ) ) ) ) ) )
5 etransclem14.j 
 |-  ( ph -> J = 0 )
6 etransclem14.cpm1 
 |-  ( ph -> ( C ` 0 ) = ( P - 1 ) )
7 fzssre 
 |-  ( 0 ... N ) C_ RR
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 2 8 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
10 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
11 9 10 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
12 3 11 ffvelrnd 
 |-  ( ph -> ( C ` 0 ) e. ( 0 ... N ) )
13 7 12 sseldi 
 |-  ( ph -> ( C ` 0 ) e. RR )
14 6 13 eqeltrrd 
 |-  ( ph -> ( P - 1 ) e. RR )
15 13 14 lttri3d 
 |-  ( ph -> ( ( C ` 0 ) = ( P - 1 ) <-> ( -. ( C ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( C ` 0 ) ) ) )
16 6 15 mpbid 
 |-  ( ph -> ( -. ( C ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( C ` 0 ) ) )
17 16 simprd 
 |-  ( ph -> -. ( P - 1 ) < ( C ` 0 ) )
18 17 iffalsed 
 |-  ( ph -> 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 ) ) ) ) )
19 14 recnd 
 |-  ( ph -> ( P - 1 ) e. CC )
20 6 eqcomd 
 |-  ( ph -> ( P - 1 ) = ( C ` 0 ) )
21 19 20 subeq0bd 
 |-  ( ph -> ( ( P - 1 ) - ( C ` 0 ) ) = 0 )
22 21 fveq2d 
 |-  ( ph -> ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) = ( ! ` 0 ) )
23 fac0 
 |-  ( ! ` 0 ) = 1
24 22 23 eqtrdi 
 |-  ( ph -> ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) = 1 )
25 24 oveq2d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / 1 ) )
26 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
27 1 26 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
28 27 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
29 28 nncnd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. CC )
30 29 div1d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
31 25 30 eqtrd 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) = ( ! ` ( P - 1 ) ) )
32 5 21 oveq12d 
 |-  ( ph -> ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) = ( 0 ^ 0 ) )
33 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
34 32 33 eqtrdi 
 |-  ( ph -> ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) = 1 )
35 31 34 oveq12d 
 |-  ( ph -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
36 29 mulid1d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
37 18 35 36 3eqtrd 
 |-  ( ph -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) = ( ! ` ( P - 1 ) ) )
38 5 oveq1d 
 |-  ( ph -> ( J - j ) = ( 0 - j ) )
39 df-neg 
 |-  -u j = ( 0 - j )
40 38 39 eqtr4di 
 |-  ( ph -> ( J - j ) = -u j )
41 40 oveq1d 
 |-  ( ph -> ( ( J - j ) ^ ( P - ( C ` j ) ) ) = ( -u j ^ ( P - ( C ` j ) ) ) )
42 41 oveq2d 
 |-  ( ph -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( -u j ^ ( P - ( C ` j ) ) ) ) )
43 42 ifeq2d 
 |-  ( ph -> if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) = if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( -u j ^ ( P - ( C ` j ) ) ) ) ) )
44 43 prodeq2ad 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) = prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( -u j ^ ( P - ( C ` j ) ) ) ) ) )
45 37 44 oveq12d 
 |-  ( 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 ) ) ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( -u j ^ ( P - ( C ` j ) ) ) ) ) ) )
46 45 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. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( -u j ^ ( P - ( C ` j ) ) ) ) ) ) ) )
47 4 46 syl5eq 
 |-  ( ph -> T = ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( -u j ^ ( P - ( C ` j ) ) ) ) ) ) ) )