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

Metamath Proof Explorer

Theorem cxpp1

Description: Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpp1 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ → A B + 1 = A B ⁢ A

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 cxpadd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ 1 ∈ ℂ → A B + 1 = A B ⁢ A 1
3 1 2 mp3an3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ → A B + 1 = A B ⁢ A 1
4 3 3impa ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ → A B + 1 = A B ⁢ A 1
5 cxp1 ⊢ A ∈ ℂ → A 1 = A
6 5 3ad2ant1 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ → A 1 = A
7 6 oveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ → A B ⁢ A 1 = A B ⁢ A
8 4 7 eqtrd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ → A B + 1 = A B ⁢ A