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

Metamath Proof Explorer

Theorem expm1t

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

Ref Expression
Assertion expm1t ⊢ A ∈ ℂ ∧ N ∈ ℕ → A N = A N − 1 ⁢ A

Proof

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