Step |
Hyp |
Ref |
Expression |
1 |
|
zcn |
|- ( N e. ZZ -> N e. CC ) |
2 |
1
|
2timesd |
|- ( N e. ZZ -> ( 2 x. N ) = ( N + N ) ) |
3 |
2
|
oveq2d |
|- ( N e. ZZ -> ( -u 1 ^ ( 2 x. N ) ) = ( -u 1 ^ ( N + N ) ) ) |
4 |
|
neg1cn |
|- -u 1 e. CC |
5 |
|
neg1ne0 |
|- -u 1 =/= 0 |
6 |
|
expaddz |
|- ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( N e. ZZ /\ N e. ZZ ) ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) ) |
7 |
4 5 6
|
mpanl12 |
|- ( ( N e. ZZ /\ N e. ZZ ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) ) |
8 |
7
|
anidms |
|- ( N e. ZZ -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) ) |
9 |
|
m1expcl2 |
|- ( N e. ZZ -> ( -u 1 ^ N ) e. { -u 1 , 1 } ) |
10 |
|
ovex |
|- ( -u 1 ^ N ) e. _V |
11 |
10
|
elpr |
|- ( ( -u 1 ^ N ) e. { -u 1 , 1 } <-> ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) ) |
12 |
|
oveq12 |
|- ( ( ( -u 1 ^ N ) = -u 1 /\ ( -u 1 ^ N ) = -u 1 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = ( -u 1 x. -u 1 ) ) |
13 |
12
|
anidms |
|- ( ( -u 1 ^ N ) = -u 1 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = ( -u 1 x. -u 1 ) ) |
14 |
|
neg1mulneg1e1 |
|- ( -u 1 x. -u 1 ) = 1 |
15 |
13 14
|
eqtrdi |
|- ( ( -u 1 ^ N ) = -u 1 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 ) |
16 |
|
oveq12 |
|- ( ( ( -u 1 ^ N ) = 1 /\ ( -u 1 ^ N ) = 1 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = ( 1 x. 1 ) ) |
17 |
16
|
anidms |
|- ( ( -u 1 ^ N ) = 1 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = ( 1 x. 1 ) ) |
18 |
|
1t1e1 |
|- ( 1 x. 1 ) = 1 |
19 |
17 18
|
eqtrdi |
|- ( ( -u 1 ^ N ) = 1 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 ) |
20 |
15 19
|
jaoi |
|- ( ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 ) |
21 |
11 20
|
sylbi |
|- ( ( -u 1 ^ N ) e. { -u 1 , 1 } -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 ) |
22 |
9 21
|
syl |
|- ( N e. ZZ -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 ) |
23 |
3 8 22
|
3eqtrd |
|- ( N e. ZZ -> ( -u 1 ^ ( 2 x. N ) ) = 1 ) |