This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℂ ⟼ A z^{N})$
	Assertion	dgr1term	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℕ_{0}) \to \deg (F) = N$

Step	Hyp	Ref	Expression
1		coe1term.1	$⊢ F = (z \in ℂ ⟼ A z^{N})$
2	1	coe1termlem	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (coeff (F) = (n \in ℕ_{0} ⟼ if (n = N, A, 0)) \land (A \neq 0 \to \deg (F) = N))$
3	2	simprd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (A \neq 0 \to \deg (F) = N)$
4	3	3impia	$⊢ (A \in ℂ \land N \in ℕ_{0} \land A \neq 0) \to \deg (F) = N$
5	4	3com23	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℕ_{0}) \to \deg (F) = N$