Metamath Proof Explorer

Theorem dvnmptconst

Description: The N -th derivative of a constant function. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnmptconst.s 
|- ( ph -> S e. { RR , CC } )
dvnmptconst.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
dvnmptconst.a 
|- ( ph -> A e. CC )
dvnmptconst.n 
|- ( ph -> N e. NN )
Assertion dvnmptconst 
|- ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` N ) = ( x e. X |-> 0 ) )

Proof

Step Hyp Ref Expression
1 dvnmptconst.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvnmptconst.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 dvnmptconst.a 
 |-  ( ph -> A e. CC )
4 dvnmptconst.n 
 |-  ( ph -> N e. NN )
5 id 
 |-  ( ph -> ph )
6 fveq2 
 |-  ( n = 1 -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( ( S Dn ( x e. X |-> A ) ) ` 1 ) )
7 6 eqeq1d 
 |-  ( n = 1 -> ( ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> 0 ) <-> ( ( S Dn ( x e. X |-> A ) ) ` 1 ) = ( x e. X |-> 0 ) ) )
8 7 imbi2d 
 |-  ( n = 1 -> ( ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> 0 ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` 1 ) = ( x e. X |-> 0 ) ) ) )
9 fveq2 
 |-  ( n = m -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( ( S Dn ( x e. X |-> A ) ) ` m ) )
10 9 eqeq1d 
 |-  ( n = m -> ( ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> 0 ) <-> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) )
11 10 imbi2d 
 |-  ( n = m -> ( ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> 0 ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) ) )
12 fveq2 
 |-  ( n = ( m + 1 ) -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( ( S Dn ( x e. X |-> A ) ) ` ( m + 1 ) ) )
13 12 eqeq1d 
 |-  ( n = ( m + 1 ) -> ( ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> 0 ) <-> ( ( S Dn ( x e. X |-> A ) ) ` ( m + 1 ) ) = ( x e. X |-> 0 ) ) )
14 13 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> 0 ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` ( m + 1 ) ) = ( x e. X |-> 0 ) ) ) )
15 fveq2 
 |-  ( n = N -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( ( S Dn ( x e. X |-> A ) ) ` N ) )
16 15 eqeq1d 
 |-  ( n = N -> ( ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> 0 ) <-> ( ( S Dn ( x e. X |-> A ) ) ` N ) = ( x e. X |-> 0 ) ) )
17 16 imbi2d 
 |-  ( n = N -> ( ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> 0 ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` N ) = ( x e. X |-> 0 ) ) ) )
18 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
19 1 18 syl 
 |-  ( ph -> S C_ CC )
20 3 adantr 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
21 restsspw 
 |-  ( ( TopOpen ` CCfld ) |`t S ) C_ ~P S
22 21 2 sselid 
 |-  ( ph -> X e. ~P S )
23 elpwi 
 |-  ( X e. ~P S -> X C_ S )
24 22 23 syl 
 |-  ( ph -> X C_ S )
25 cnex 
 |-  CC e. _V
26 25 a1i 
 |-  ( ph -> CC e. _V )
27 20 24 26 1 mptelpm 
 |-  ( ph -> ( x e. X |-> A ) e. ( CC ^pm S ) )
28 dvn1 
 |-  ( ( S C_ CC /\ ( x e. X |-> A ) e. ( CC ^pm S ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` 1 ) = ( S _D ( x e. X |-> A ) ) )
29 19 27 28 syl2anc 
 |-  ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` 1 ) = ( S _D ( x e. X |-> A ) ) )
30 1 2 3 dvmptconst 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> 0 ) )
31 29 30 eqtrd 
 |-  ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` 1 ) = ( x e. X |-> 0 ) )
32 simp3 
 |-  ( ( m e. NN /\ ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) /\ ph ) -> ph )
33 simp1 
 |-  ( ( m e. NN /\ ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) /\ ph ) -> m e. NN )
34 simpr 
 |-  ( ( ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) /\ ph ) -> ph )
35 simpl 
 |-  ( ( ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) /\ ph ) -> ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) )
36 pm3.35 
 |-  ( ( ph /\ ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) )
37 34 35 36 syl2anc 
 |-  ( ( ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) )
38 37 3adant1 
 |-  ( ( m e. NN /\ ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) )
39 19 3ad2ant1 
 |-  ( ( ph /\ m e. NN /\ ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) -> S C_ CC )
40 27 3ad2ant1 
 |-  ( ( ph /\ m e. NN /\ ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) -> ( x e. X |-> A ) e. ( CC ^pm S ) )
41 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
42 41 3ad2ant2 
 |-  ( ( ph /\ m e. NN /\ ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) -> m e. NN0 )
43 dvnp1 
 |-  ( ( S C_ CC /\ ( x e. X |-> A ) e. ( CC ^pm S ) /\ m e. NN0 ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( m + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> A ) ) ` m ) ) )
44 39 40 42 43 syl3anc 
 |-  ( ( ph /\ m e. NN /\ ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( m + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> A ) ) ` m ) ) )
45 oveq2 
 |-  ( ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) -> ( S _D ( ( S Dn ( x e. X |-> A ) ) ` m ) ) = ( S _D ( x e. X |-> 0 ) ) )
46 45 3ad2ant3 
 |-  ( ( ph /\ m e. NN /\ ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) -> ( S _D ( ( S Dn ( x e. X |-> A ) ) ` m ) ) = ( S _D ( x e. X |-> 0 ) ) )
47 0cnd 
 |-  ( ph -> 0 e. CC )
48 1 2 47 dvmptconst 
 |-  ( ph -> ( S _D ( x e. X |-> 0 ) ) = ( x e. X |-> 0 ) )
49 48 3ad2ant1 
 |-  ( ( ph /\ m e. NN /\ ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) -> ( S _D ( x e. X |-> 0 ) ) = ( x e. X |-> 0 ) )
50 44 46 49 3eqtrd 
 |-  ( ( ph /\ m e. NN /\ ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( m + 1 ) ) = ( x e. X |-> 0 ) )
51 32 33 38 50 syl3anc 
 |-  ( ( m e. NN /\ ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( m + 1 ) ) = ( x e. X |-> 0 ) )
52 51 3exp 
 |-  ( m e. NN -> ( ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` m ) = ( x e. X |-> 0 ) ) -> ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` ( m + 1 ) ) = ( x e. X |-> 0 ) ) ) )
53 8 11 14 17 31 52 nnind 
 |-  ( N e. NN -> ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` N ) = ( x e. X |-> 0 ) ) )
54 4 5 53 sylc 
 |-  ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` N ) = ( x e. X |-> 0 ) )