Theorem dgr1term

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

	Ref	Expression
Hypothesis	coe1term.1	⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
Assertion	dgr1term	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℕ0 ) → ( deg ‘ 𝐹 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		coe1term.1	⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
2	1	coe1termlem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ∧ ( 𝐴 ≠ 0 → ( deg ‘ 𝐹 ) = 𝑁 ) ) )
3	2	simprd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ≠ 0 → ( deg ‘ 𝐹 ) = 𝑁 ) )
4	3	3impia	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ≠ 0 ) → ( deg ‘ 𝐹 ) = 𝑁 )
5	4	3com23	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℕ0 ) → ( deg ‘ 𝐹 ) = 𝑁 )