Metamath Proof Explorer

Theorem etransclem19

Description: The N -th derivative of H is 0 if N is large enough. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem19.s 
|- ( ph -> S e. { RR , CC } )
etransclem19.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
etransclem19.p 
|- ( ph -> P e. NN )
etransclem19.1 
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
etransclem19.J 
|- ( ph -> J e. ( 0 ... M ) )
etransclem19.n 
|- ( ph -> N e. ZZ )
etransclem19.7 
|- ( ph -> if ( J = 0 , ( P - 1 ) , P ) < N )
Assertion etransclem19 
|- ( ph -> ( ( S Dn ( H ` J ) ) ` N ) = ( x e. X |-> 0 ) )

Proof

Step Hyp Ref Expression
1 etransclem19.s 
 |-  ( ph -> S e. { RR , CC } )
2 etransclem19.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem19.p 
 |-  ( ph -> P e. NN )
4 etransclem19.1 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
5 etransclem19.J 
 |-  ( ph -> J e. ( 0 ... M ) )
6 etransclem19.n 
 |-  ( ph -> N e. ZZ )
7 etransclem19.7 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) < N )
8 0red 
 |-  ( ph -> 0 e. RR )
9 6 zred 
 |-  ( ph -> N e. RR )
10 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
11 3 10 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
12 11 nn0red 
 |-  ( ph -> ( P - 1 ) e. RR )
13 3 nnred 
 |-  ( ph -> P e. RR )
14 12 13 ifcld 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. RR )
15 11 nn0ge0d 
 |-  ( ph -> 0 <_ ( P - 1 ) )
16 15 adantr 
 |-  ( ( ph /\ J = 0 ) -> 0 <_ ( P - 1 ) )
17 iftrue 
 |-  ( J = 0 -> if ( J = 0 , ( P - 1 ) , P ) = ( P - 1 ) )
18 17 eqcomd 
 |-  ( J = 0 -> ( P - 1 ) = if ( J = 0 , ( P - 1 ) , P ) )
19 18 adantl 
 |-  ( ( ph /\ J = 0 ) -> ( P - 1 ) = if ( J = 0 , ( P - 1 ) , P ) )
20 16 19 breqtrd 
 |-  ( ( ph /\ J = 0 ) -> 0 <_ if ( J = 0 , ( P - 1 ) , P ) )
21 3 nnnn0d 
 |-  ( ph -> P e. NN0 )
22 21 nn0ge0d 
 |-  ( ph -> 0 <_ P )
23 22 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> 0 <_ P )
24 iffalse 
 |-  ( -. J = 0 -> if ( J = 0 , ( P - 1 ) , P ) = P )
25 24 eqcomd 
 |-  ( -. J = 0 -> P = if ( J = 0 , ( P - 1 ) , P ) )
26 25 adantl 
 |-  ( ( ph /\ -. J = 0 ) -> P = if ( J = 0 , ( P - 1 ) , P ) )
27 23 26 breqtrd 
 |-  ( ( ph /\ -. J = 0 ) -> 0 <_ if ( J = 0 , ( P - 1 ) , P ) )
28 20 27 pm2.61dan 
 |-  ( ph -> 0 <_ if ( J = 0 , ( P - 1 ) , P ) )
29 8 14 9 28 7 lelttrd 
 |-  ( ph -> 0 < N )
30 8 9 29 ltled 
 |-  ( ph -> 0 <_ N )
31 elnn0z 
 |-  ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )
32 6 30 31 sylanbrc 
 |-  ( ph -> N e. NN0 )
33 1 2 3 4 5 32 etransclem17 
 |-  ( ph -> ( ( S Dn ( H ` J ) ) ` N ) = ( x e. X |-> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) )
34 7 iftrued 
 |-  ( ph -> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) = 0 )
35 34 mpteq2dv 
 |-  ( ph -> ( x e. X |-> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) = ( x e. X |-> 0 ) )
36 33 35 eqtrd 
 |-  ( ph -> ( ( S Dn ( H ` J ) ) ` N ) = ( x e. X |-> 0 ) )