plypow

Description: A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

		Ref	Expression
	Assertion	plypow	$⊢ (S \subseteq ℂ \land 1 \in S \land N \in ℕ_{0}) \to (z \in ℂ ⟼ z^{N}) \in Poly (S)$

Step	Hyp	Ref	Expression
1		id	$⊢ z \in ℂ \to z \in ℂ$
2		simp3	$⊢ (S \subseteq ℂ \land 1 \in S \land N \in ℕ_{0}) \to N \in ℕ_{0}$
3		expcl	$⊢ (z \in ℂ \land N \in ℕ_{0}) \to z^{N} \in ℂ$
4	1 2 3	syl2anr	$⊢ ((S \subseteq ℂ \land 1 \in S \land N \in ℕ_{0}) \land z \in ℂ) \to z^{N} \in ℂ$
5	4	mullidd	$⊢ ((S \subseteq ℂ \land 1 \in S \land N \in ℕ_{0}) \land z \in ℂ) \to 1 z^{N} = z^{N}$
6	5	mpteq2dva	$⊢ (S \subseteq ℂ \land 1 \in S \land N \in ℕ_{0}) \to (z \in ℂ ⟼ 1 z^{N}) = (z \in ℂ ⟼ z^{N})$
7		eqid	$⊢ (z \in ℂ ⟼ 1 z^{N}) = (z \in ℂ ⟼ 1 z^{N})$
8	7	ply1term	$⊢ (S \subseteq ℂ \land 1 \in S \land N \in ℕ_{0}) \to (z \in ℂ ⟼ 1 z^{N}) \in Poly (S)$
9	6 8	eqeltrrd	$⊢ (S \subseteq ℂ \land 1 \in S \land N \in ℕ_{0}) \to (z \in ℂ ⟼ z^{N}) \in Poly (S)$

Metamath Proof Explorer