Step |
Hyp |
Ref |
Expression |
1 |
|
negex |
|- -u 1 e. _V |
2 |
1
|
prid1 |
|- -u 1 e. { -u 1 , 1 } |
3 |
|
neg1ne0 |
|- -u 1 =/= 0 |
4 |
|
neg1cn |
|- -u 1 e. CC |
5 |
|
ax-1cn |
|- 1 e. CC |
6 |
|
prssi |
|- ( ( -u 1 e. CC /\ 1 e. CC ) -> { -u 1 , 1 } C_ CC ) |
7 |
4 5 6
|
mp2an |
|- { -u 1 , 1 } C_ CC |
8 |
|
elpri |
|- ( x e. { -u 1 , 1 } -> ( x = -u 1 \/ x = 1 ) ) |
9 |
7
|
sseli |
|- ( y e. { -u 1 , 1 } -> y e. CC ) |
10 |
9
|
mulm1d |
|- ( y e. { -u 1 , 1 } -> ( -u 1 x. y ) = -u y ) |
11 |
|
elpri |
|- ( y e. { -u 1 , 1 } -> ( y = -u 1 \/ y = 1 ) ) |
12 |
|
negeq |
|- ( y = -u 1 -> -u y = -u -u 1 ) |
13 |
|
negneg1e1 |
|- -u -u 1 = 1 |
14 |
|
1ex |
|- 1 e. _V |
15 |
14
|
prid2 |
|- 1 e. { -u 1 , 1 } |
16 |
13 15
|
eqeltri |
|- -u -u 1 e. { -u 1 , 1 } |
17 |
12 16
|
eqeltrdi |
|- ( y = -u 1 -> -u y e. { -u 1 , 1 } ) |
18 |
|
negeq |
|- ( y = 1 -> -u y = -u 1 ) |
19 |
18 2
|
eqeltrdi |
|- ( y = 1 -> -u y e. { -u 1 , 1 } ) |
20 |
17 19
|
jaoi |
|- ( ( y = -u 1 \/ y = 1 ) -> -u y e. { -u 1 , 1 } ) |
21 |
11 20
|
syl |
|- ( y e. { -u 1 , 1 } -> -u y e. { -u 1 , 1 } ) |
22 |
10 21
|
eqeltrd |
|- ( y e. { -u 1 , 1 } -> ( -u 1 x. y ) e. { -u 1 , 1 } ) |
23 |
|
oveq1 |
|- ( x = -u 1 -> ( x x. y ) = ( -u 1 x. y ) ) |
24 |
23
|
eleq1d |
|- ( x = -u 1 -> ( ( x x. y ) e. { -u 1 , 1 } <-> ( -u 1 x. y ) e. { -u 1 , 1 } ) ) |
25 |
22 24
|
syl5ibr |
|- ( x = -u 1 -> ( y e. { -u 1 , 1 } -> ( x x. y ) e. { -u 1 , 1 } ) ) |
26 |
9
|
mulid2d |
|- ( y e. { -u 1 , 1 } -> ( 1 x. y ) = y ) |
27 |
|
id |
|- ( y e. { -u 1 , 1 } -> y e. { -u 1 , 1 } ) |
28 |
26 27
|
eqeltrd |
|- ( y e. { -u 1 , 1 } -> ( 1 x. y ) e. { -u 1 , 1 } ) |
29 |
|
oveq1 |
|- ( x = 1 -> ( x x. y ) = ( 1 x. y ) ) |
30 |
29
|
eleq1d |
|- ( x = 1 -> ( ( x x. y ) e. { -u 1 , 1 } <-> ( 1 x. y ) e. { -u 1 , 1 } ) ) |
31 |
28 30
|
syl5ibr |
|- ( x = 1 -> ( y e. { -u 1 , 1 } -> ( x x. y ) e. { -u 1 , 1 } ) ) |
32 |
25 31
|
jaoi |
|- ( ( x = -u 1 \/ x = 1 ) -> ( y e. { -u 1 , 1 } -> ( x x. y ) e. { -u 1 , 1 } ) ) |
33 |
8 32
|
syl |
|- ( x e. { -u 1 , 1 } -> ( y e. { -u 1 , 1 } -> ( x x. y ) e. { -u 1 , 1 } ) ) |
34 |
33
|
imp |
|- ( ( x e. { -u 1 , 1 } /\ y e. { -u 1 , 1 } ) -> ( x x. y ) e. { -u 1 , 1 } ) |
35 |
|
oveq2 |
|- ( x = -u 1 -> ( 1 / x ) = ( 1 / -u 1 ) ) |
36 |
|
ax-1ne0 |
|- 1 =/= 0 |
37 |
|
divneg2 |
|- ( ( 1 e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) ) |
38 |
5 5 36 37
|
mp3an |
|- -u ( 1 / 1 ) = ( 1 / -u 1 ) |
39 |
|
1div1e1 |
|- ( 1 / 1 ) = 1 |
40 |
39
|
negeqi |
|- -u ( 1 / 1 ) = -u 1 |
41 |
38 40
|
eqtr3i |
|- ( 1 / -u 1 ) = -u 1 |
42 |
41 2
|
eqeltri |
|- ( 1 / -u 1 ) e. { -u 1 , 1 } |
43 |
35 42
|
eqeltrdi |
|- ( x = -u 1 -> ( 1 / x ) e. { -u 1 , 1 } ) |
44 |
|
oveq2 |
|- ( x = 1 -> ( 1 / x ) = ( 1 / 1 ) ) |
45 |
39 15
|
eqeltri |
|- ( 1 / 1 ) e. { -u 1 , 1 } |
46 |
44 45
|
eqeltrdi |
|- ( x = 1 -> ( 1 / x ) e. { -u 1 , 1 } ) |
47 |
43 46
|
jaoi |
|- ( ( x = -u 1 \/ x = 1 ) -> ( 1 / x ) e. { -u 1 , 1 } ) |
48 |
8 47
|
syl |
|- ( x e. { -u 1 , 1 } -> ( 1 / x ) e. { -u 1 , 1 } ) |
49 |
48
|
adantr |
|- ( ( x e. { -u 1 , 1 } /\ x =/= 0 ) -> ( 1 / x ) e. { -u 1 , 1 } ) |
50 |
7 34 15 49
|
expcl2lem |
|- ( ( -u 1 e. { -u 1 , 1 } /\ -u 1 =/= 0 /\ N e. ZZ ) -> ( -u 1 ^ N ) e. { -u 1 , 1 } ) |
51 |
2 3 50
|
mp3an12 |
|- ( N e. ZZ -> ( -u 1 ^ N ) e. { -u 1 , 1 } ) |