Theorem expm1t

Description: Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005)

	Ref	Expression
Assertion	expm1t	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
2		ax-1cn	⊢ 1 ∈ ℂ
3		npcan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
4	1 2 3	sylancl	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
5	4	oveq2d	⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝐴 ↑ 𝑁 ) )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝐴 ↑ 𝑁 ) )
7		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
8		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 𝐴 ) )
9	7 8	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 𝐴 ) )
10	6 9	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 𝐴 ) )