Metamath Proof Explorer

Theorem dgr1term

Description: The degree of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis coe1term.1 
|- F = ( z e. CC |-> ( A x. ( z ^ N ) ) )
Assertion dgr1term 
|- ( ( A e. CC /\ A =/= 0 /\ N e. NN0 ) -> ( deg ` F ) = N )

Proof

Step Hyp Ref Expression
1 coe1term.1 
 |-  F = ( z e. CC |-> ( A x. ( z ^ N ) ) )
2 1 coe1termlem 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( coeff ` F ) = ( n e. NN0 |-> if ( n = N , A , 0 ) ) /\ ( A =/= 0 -> ( deg ` F ) = N ) ) )
3 2 simprd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A =/= 0 -> ( deg ` F ) = N ) )
4 3 3impia 
 |-  ( ( A e. CC /\ N e. NN0 /\ A =/= 0 ) -> ( deg ` F ) = N )
5 4 3com23 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. NN0 ) -> ( deg ` F ) = N )