Metamath Proof Explorer


Theorem cjexp

Description: Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006)

Ref Expression
Assertion cjexp A N 0 A N = A N

Proof

Step Hyp Ref Expression
1 oveq2 j = 0 A j = A 0
2 1 fveq2d j = 0 A j = A 0
3 oveq2 j = 0 A j = A 0
4 2 3 eqeq12d j = 0 A j = A j A 0 = A 0
5 oveq2 j = k A j = A k
6 5 fveq2d j = k A j = A k
7 oveq2 j = k A j = A k
8 6 7 eqeq12d j = k A j = A j A k = A k
9 oveq2 j = k + 1 A j = A k + 1
10 9 fveq2d j = k + 1 A j = A k + 1
11 oveq2 j = k + 1 A j = A k + 1
12 10 11 eqeq12d j = k + 1 A j = A j A k + 1 = A k + 1
13 oveq2 j = N A j = A N
14 13 fveq2d j = N A j = A N
15 oveq2 j = N A j = A N
16 14 15 eqeq12d j = N A j = A j A N = A N
17 exp0 A A 0 = 1
18 17 fveq2d A A 0 = 1
19 cjcl A A
20 exp0 A A 0 = 1
21 1re 1
22 cjre 1 1 = 1
23 21 22 ax-mp 1 = 1
24 20 23 eqtr4di A A 0 = 1
25 19 24 syl A A 0 = 1
26 18 25 eqtr4d A A 0 = A 0
27 expp1 A k 0 A k + 1 = A k A
28 27 fveq2d A k 0 A k + 1 = A k A
29 expcl A k 0 A k
30 simpl A k 0 A
31 cjmul A k A A k A = A k A
32 29 30 31 syl2anc A k 0 A k A = A k A
33 28 32 eqtrd A k 0 A k + 1 = A k A
34 33 adantr A k 0 A k = A k A k + 1 = A k A
35 oveq1 A k = A k A k A = A k A
36 expp1 A k 0 A k + 1 = A k A
37 19 36 sylan A k 0 A k + 1 = A k A
38 37 eqcomd A k 0 A k A = A k + 1
39 35 38 sylan9eqr A k 0 A k = A k A k A = A k + 1
40 34 39 eqtrd A k 0 A k = A k A k + 1 = A k + 1
41 4 8 12 16 26 40 nn0indd A N 0 A N = A N