Metamath Proof Explorer

Theorem dvnfre

Description: The N -th derivative of a real function is real. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion dvnfre 
|- ( ( F : A --> RR /\ A C_ RR /\ N e. NN0 ) -> ( ( RR Dn F ) ` N ) : dom ( ( RR Dn F ) ` N ) --> RR )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = 0 -> ( ( RR Dn F ) ` x ) = ( ( RR Dn F ) ` 0 ) )
2 1 dmeqd 
 |-  ( x = 0 -> dom ( ( RR Dn F ) ` x ) = dom ( ( RR Dn F ) ` 0 ) )
3 1 2 feq12d 
 |-  ( x = 0 -> ( ( ( RR Dn F ) ` x ) : dom ( ( RR Dn F ) ` x ) --> RR <-> ( ( RR Dn F ) ` 0 ) : dom ( ( RR Dn F ) ` 0 ) --> RR ) )
4 3 imbi2d 
 |-  ( x = 0 -> ( ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` x ) : dom ( ( RR Dn F ) ` x ) --> RR ) <-> ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` 0 ) : dom ( ( RR Dn F ) ` 0 ) --> RR ) ) )
5 fveq2 
 |-  ( x = n -> ( ( RR Dn F ) ` x ) = ( ( RR Dn F ) ` n ) )
6 5 dmeqd 
 |-  ( x = n -> dom ( ( RR Dn F ) ` x ) = dom ( ( RR Dn F ) ` n ) )
7 5 6 feq12d 
 |-  ( x = n -> ( ( ( RR Dn F ) ` x ) : dom ( ( RR Dn F ) ` x ) --> RR <-> ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) )
8 7 imbi2d 
 |-  ( x = n -> ( ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` x ) : dom ( ( RR Dn F ) ` x ) --> RR ) <-> ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) )
9 fveq2 
 |-  ( x = ( n + 1 ) -> ( ( RR Dn F ) ` x ) = ( ( RR Dn F ) ` ( n + 1 ) ) )
10 9 dmeqd 
 |-  ( x = ( n + 1 ) -> dom ( ( RR Dn F ) ` x ) = dom ( ( RR Dn F ) ` ( n + 1 ) ) )
11 9 10 feq12d 
 |-  ( x = ( n + 1 ) -> ( ( ( RR Dn F ) ` x ) : dom ( ( RR Dn F ) ` x ) --> RR <-> ( ( RR Dn F ) ` ( n + 1 ) ) : dom ( ( RR Dn F ) ` ( n + 1 ) ) --> RR ) )
12 11 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` x ) : dom ( ( RR Dn F ) ` x ) --> RR ) <-> ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` ( n + 1 ) ) : dom ( ( RR Dn F ) ` ( n + 1 ) ) --> RR ) ) )
13 fveq2 
 |-  ( x = N -> ( ( RR Dn F ) ` x ) = ( ( RR Dn F ) ` N ) )
14 13 dmeqd 
 |-  ( x = N -> dom ( ( RR Dn F ) ` x ) = dom ( ( RR Dn F ) ` N ) )
15 13 14 feq12d 
 |-  ( x = N -> ( ( ( RR Dn F ) ` x ) : dom ( ( RR Dn F ) ` x ) --> RR <-> ( ( RR Dn F ) ` N ) : dom ( ( RR Dn F ) ` N ) --> RR ) )
16 15 imbi2d 
 |-  ( x = N -> ( ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` x ) : dom ( ( RR Dn F ) ` x ) --> RR ) <-> ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` N ) : dom ( ( RR Dn F ) ` N ) --> RR ) ) )
17 simpl 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> F : A --> RR )
18 ax-resscn 
 |-  RR C_ CC
19 fss 
 |-  ( ( F : A --> RR /\ RR C_ CC ) -> F : A --> CC )
20 18 19 mpan2 
 |-  ( F : A --> RR -> F : A --> CC )
21 cnex 
 |-  CC e. _V
22 reex 
 |-  RR e. _V
23 elpm2r 
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) )
24 21 22 23 mpanl12 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> F e. ( CC ^pm RR ) )
25 20 24 sylan 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> F e. ( CC ^pm RR ) )
26 dvn0 
 |-  ( ( RR C_ CC /\ F e. ( CC ^pm RR ) ) -> ( ( RR Dn F ) ` 0 ) = F )
27 18 25 26 sylancr 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` 0 ) = F )
28 27 dmeqd 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> dom ( ( RR Dn F ) ` 0 ) = dom F )
29 fdm 
 |-  ( F : A --> RR -> dom F = A )
30 29 adantr 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> dom F = A )
31 28 30 eqtrd 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> dom ( ( RR Dn F ) ` 0 ) = A )
32 27 31 feq12d 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( ( ( RR Dn F ) ` 0 ) : dom ( ( RR Dn F ) ` 0 ) --> RR <-> F : A --> RR ) )
33 17 32 mpbird 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` 0 ) : dom ( ( RR Dn F ) ` 0 ) --> RR )
34 simprr 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR )
35 22 prid1 
 |-  RR e. { RR , CC }
36 simprl 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> n e. NN0 )
37 dvnbss 
 |-  ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ n e. NN0 ) -> dom ( ( RR Dn F ) ` n ) C_ dom F )
38 35 25 36 37 mp3an2ani 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> dom ( ( RR Dn F ) ` n ) C_ dom F )
39 30 adantr 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> dom F = A )
40 38 39 sseqtrd 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> dom ( ( RR Dn F ) ` n ) C_ A )
41 simplr 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> A C_ RR )
42 40 41 sstrd 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> dom ( ( RR Dn F ) ` n ) C_ RR )
43 dvfre 
 |-  ( ( ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR /\ dom ( ( RR Dn F ) ` n ) C_ RR ) -> ( RR _D ( ( RR Dn F ) ` n ) ) : dom ( RR _D ( ( RR Dn F ) ` n ) ) --> RR )
44 34 42 43 syl2anc 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> ( RR _D ( ( RR Dn F ) ` n ) ) : dom ( RR _D ( ( RR Dn F ) ` n ) ) --> RR )
45 dvnp1 
 |-  ( ( RR C_ CC /\ F e. ( CC ^pm RR ) /\ n e. NN0 ) -> ( ( RR Dn F ) ` ( n + 1 ) ) = ( RR _D ( ( RR Dn F ) ` n ) ) )
46 18 25 36 45 mp3an2ani 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> ( ( RR Dn F ) ` ( n + 1 ) ) = ( RR _D ( ( RR Dn F ) ` n ) ) )
47 46 dmeqd 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> dom ( ( RR Dn F ) ` ( n + 1 ) ) = dom ( RR _D ( ( RR Dn F ) ` n ) ) )
48 46 47 feq12d 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> ( ( ( RR Dn F ) ` ( n + 1 ) ) : dom ( ( RR Dn F ) ` ( n + 1 ) ) --> RR <-> ( RR _D ( ( RR Dn F ) ` n ) ) : dom ( RR _D ( ( RR Dn F ) ` n ) ) --> RR ) )
49 44 48 mpbird 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ ( n e. NN0 /\ ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) ) -> ( ( RR Dn F ) ` ( n + 1 ) ) : dom ( ( RR Dn F ) ` ( n + 1 ) ) --> RR )
50 49 expr 
 |-  ( ( ( F : A --> RR /\ A C_ RR ) /\ n e. NN0 ) -> ( ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR -> ( ( RR Dn F ) ` ( n + 1 ) ) : dom ( ( RR Dn F ) ` ( n + 1 ) ) --> RR ) )
51 50 expcom 
 |-  ( n e. NN0 -> ( ( F : A --> RR /\ A C_ RR ) -> ( ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR -> ( ( RR Dn F ) ` ( n + 1 ) ) : dom ( ( RR Dn F ) ` ( n + 1 ) ) --> RR ) ) )
52 51 a2d 
 |-  ( n e. NN0 -> ( ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` n ) : dom ( ( RR Dn F ) ` n ) --> RR ) -> ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` ( n + 1 ) ) : dom ( ( RR Dn F ) ` ( n + 1 ) ) --> RR ) ) )
53 4 8 12 16 33 52 nn0ind 
 |-  ( N e. NN0 -> ( ( F : A --> RR /\ A C_ RR ) -> ( ( RR Dn F ) ` N ) : dom ( ( RR Dn F ) ` N ) --> RR ) )
54 53 com12 
 |-  ( ( F : A --> RR /\ A C_ RR ) -> ( N e. NN0 -> ( ( RR Dn F ) ` N ) : dom ( ( RR Dn F ) ` N ) --> RR ) )
55 54 3impia 
 |-  ( ( F : A --> RR /\ A C_ RR /\ N e. NN0 ) -> ( ( RR Dn F ) ` N ) : dom ( ( RR Dn F ) ` N ) --> RR )