Step |
Hyp |
Ref |
Expression |
1 |
|
neg1cn |
|- -u 1 e. CC |
2 |
1
|
a1i |
|- ( N e. NN -> -u 1 e. CC ) |
3 |
|
2re |
|- 2 e. RR |
4 |
|
nndivre |
|- ( ( 2 e. RR /\ N e. NN ) -> ( 2 / N ) e. RR ) |
5 |
3 4
|
mpan |
|- ( N e. NN -> ( 2 / N ) e. RR ) |
6 |
5
|
recnd |
|- ( N e. NN -> ( 2 / N ) e. CC ) |
7 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
8 |
2 6 7
|
cxpmul2d |
|- ( N e. NN -> ( -u 1 ^c ( ( 2 / N ) x. N ) ) = ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ) |
9 |
|
2cnd |
|- ( N e. NN -> 2 e. CC ) |
10 |
|
nncn |
|- ( N e. NN -> N e. CC ) |
11 |
|
nnne0 |
|- ( N e. NN -> N =/= 0 ) |
12 |
9 10 11
|
divcan1d |
|- ( N e. NN -> ( ( 2 / N ) x. N ) = 2 ) |
13 |
12
|
oveq2d |
|- ( N e. NN -> ( -u 1 ^c ( ( 2 / N ) x. N ) ) = ( -u 1 ^c 2 ) ) |
14 |
|
2nn0 |
|- 2 e. NN0 |
15 |
|
cxpexp |
|- ( ( -u 1 e. CC /\ 2 e. NN0 ) -> ( -u 1 ^c 2 ) = ( -u 1 ^ 2 ) ) |
16 |
1 14 15
|
mp2an |
|- ( -u 1 ^c 2 ) = ( -u 1 ^ 2 ) |
17 |
|
ax-1cn |
|- 1 e. CC |
18 |
|
sqneg |
|- ( 1 e. CC -> ( -u 1 ^ 2 ) = ( 1 ^ 2 ) ) |
19 |
17 18
|
ax-mp |
|- ( -u 1 ^ 2 ) = ( 1 ^ 2 ) |
20 |
|
sq1 |
|- ( 1 ^ 2 ) = 1 |
21 |
16 19 20
|
3eqtri |
|- ( -u 1 ^c 2 ) = 1 |
22 |
13 21
|
eqtrdi |
|- ( N e. NN -> ( -u 1 ^c ( ( 2 / N ) x. N ) ) = 1 ) |
23 |
8 22
|
eqtr3d |
|- ( N e. NN -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 ) |