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

Metamath Proof Explorer

Theorem expp1d

Description: Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of Gleason p. 134. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	expcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	expcld.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
Assertion	expp1d	⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		expcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		expcld.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
3		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ₀ ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) )