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. (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 mulid2 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