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

Metamath Proof Explorer

Theorem coef

Description: The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014)

		Ref	Expression
	Hypothesis	dgrval.1	$⊢ A = coeff (F)$
	Assertion	coef	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ S \cup \{0\}$

Step	Hyp	Ref	Expression
1		dgrval.1	$⊢ A = coeff (F)$
2	1	dgrlem	$⊢ F \in Poly (S) \to (A : ℕ_{0} ⟶ S \cup \{0\} \land \exists n \in ℤ \forall x \in A^{-1} [ℂ ∖ \{0\}] x \leq n)$
3	2	simpld	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ S \cup \{0\}$