Theorem plypow

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

	Ref	Expression
Assertion	plypow	⊢ ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑁 ) ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑧 ∈ ℂ → 𝑧 ∈ ℂ )
2		simp3	⊢ ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
3		expcl	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑁 ) ∈ ℂ )
4	1 2 3	syl2anr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ↑ 𝑁 ) ∈ ℂ )
5	4	mullidd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( 1 · ( 𝑧 ↑ 𝑁 ) ) = ( 𝑧 ↑ 𝑁 ) )
6	5	mpteq2dva	⊢ ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 𝑁 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑁 ) ) )
7		eqid	⊢ ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 𝑁 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 𝑁 ) ) )
8	7	ply1term	⊢ ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 𝑁 ) ) ) ∈ ( Poly ‘ 𝑆 ) )
9	6 8	eqeltrrd	⊢ ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑁 ) ) ∈ ( Poly ‘ 𝑆 ) )