Step |
Hyp |
Ref |
Expression |
1 |
|
0p1e1 |
|- ( 0 + 1 ) = 1 |
2 |
1
|
fveq2i |
|- ( ( S Dn F ) ` ( 0 + 1 ) ) = ( ( S Dn F ) ` 1 ) |
3 |
|
0nn0 |
|- 0 e. NN0 |
4 |
|
dvnp1 |
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ 0 e. NN0 ) -> ( ( S Dn F ) ` ( 0 + 1 ) ) = ( S _D ( ( S Dn F ) ` 0 ) ) ) |
5 |
3 4
|
mp3an3 |
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` ( 0 + 1 ) ) = ( S _D ( ( S Dn F ) ` 0 ) ) ) |
6 |
|
dvn0 |
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F ) |
7 |
6
|
oveq2d |
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( S _D ( ( S Dn F ) ` 0 ) ) = ( S _D F ) ) |
8 |
5 7
|
eqtrd |
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` ( 0 + 1 ) ) = ( S _D F ) ) |
9 |
2 8
|
syl5eqr |
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 1 ) = ( S _D F ) ) |