Metamath Proof Explorer

Theorem expp1

Description: Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of Gleason p. 134. When A is nonzero, this holds for all integers N , see expneg . (Contributed by NM, 20-May-2005) (Revised by Mario Carneiro, 2-Jul-2013)

Ref Expression
Assertion expp1 ⊢ A ∈ ℂ ∧ N ∈ ℕ 0 → A N + 1 = A N ⁢ A

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
2 seqp1 ⊢ N ∈ ℤ ≥ 1 → seq 1 × ℕ × A ⁡ N + 1 = seq 1 × ℕ × A ⁡ N ⁢ ℕ × A ⁡ N + 1
3 nnuz ⊢ ℕ = ℤ ≥ 1
4 2 3 eleq2s ⊢ N ∈ ℕ → seq 1 × ℕ × A ⁡ N + 1 = seq 1 × ℕ × A ⁡ N ⁢ ℕ × A ⁡ N + 1
5 4 adantl ⊢ A ∈ ℂ ∧ N ∈ ℕ → seq 1 × ℕ × A ⁡ N + 1 = seq 1 × ℕ × A ⁡ N ⁢ ℕ × A ⁡ N + 1
6 peano2nn ⊢ N ∈ ℕ → N + 1 ∈ ℕ
7 fvconst2g ⊢ A ∈ ℂ ∧ N + 1 ∈ ℕ → ℕ × A ⁡ N + 1 = A
8 6 7 sylan2 ⊢ A ∈ ℂ ∧ N ∈ ℕ → ℕ × A ⁡ N + 1 = A
9 8 oveq2d ⊢ A ∈ ℂ ∧ N ∈ ℕ → seq 1 × ℕ × A ⁡ N ⁢ ℕ × A ⁡ N + 1 = seq 1 × ℕ × A ⁡ N ⁢ A
10 5 9 eqtrd ⊢ A ∈ ℂ ∧ N ∈ ℕ → seq 1 × ℕ × A ⁡ N + 1 = seq 1 × ℕ × A ⁡ N ⁢ A
11 expnnval ⊢ A ∈ ℂ ∧ N + 1 ∈ ℕ → A N + 1 = seq 1 × ℕ × A ⁡ N + 1
12 6 11 sylan2 ⊢ A ∈ ℂ ∧ N ∈ ℕ → A N + 1 = seq 1 × ℕ × A ⁡ N + 1
13 expnnval ⊢ A ∈ ℂ ∧ N ∈ ℕ → A N = seq 1 × ℕ × A ⁡ N
14 13 oveq1d ⊢ A ∈ ℂ ∧ N ∈ ℕ → A N ⁢ A = seq 1 × ℕ × A ⁡ N ⁢ A
15 10 12 14 3eqtr4d ⊢ A ∈ ℂ ∧ N ∈ ℕ → A N + 1 = A N ⁢ A
16 exp1 ⊢ A ∈ ℂ → A 1 = A
17 mullid ⊢ A ∈ ℂ → 1 ⁢ A = A
18 16 17 eqtr4d ⊢ A ∈ ℂ → A 1 = 1 ⁢ A
19 18 adantr ⊢ A ∈ ℂ ∧ N = 0 → A 1 = 1 ⁢ A
20 simpr ⊢ A ∈ ℂ ∧ N = 0 → N = 0
21 20 oveq1d ⊢ A ∈ ℂ ∧ N = 0 → N + 1 = 0 + 1
22 0p1e1 ⊢ 0 + 1 = 1
23 21 22 eqtrdi ⊢ A ∈ ℂ ∧ N = 0 → N + 1 = 1
24 23 oveq2d ⊢ A ∈ ℂ ∧ N = 0 → A N + 1 = A 1
25 oveq2 ⊢ N = 0 → A N = A 0
26 exp0 ⊢ A ∈ ℂ → A 0 = 1
27 25 26 sylan9eqr ⊢ A ∈ ℂ ∧ N = 0 → A N = 1
28 27 oveq1d ⊢ A ∈ ℂ ∧ N = 0 → A N ⁢ A = 1 ⁢ A
29 19 24 28 3eqtr4d ⊢ A ∈ ℂ ∧ N = 0 → A N + 1 = A N ⁢ A
30 15 29 jaodan ⊢ A ∈ ℂ ∧ N ∈ ℕ ∨ N = 0 → A N + 1 = A N ⁢ A
31 1 30 sylan2b ⊢ A ∈ ℂ ∧ N ∈ ℕ 0 → A N + 1 = A N ⁢ A