Step |
Hyp |
Ref |
Expression |
1 |
|
negex |
โข - 1 โ V |
2 |
1
|
prid1 |
โข - 1 โ { - 1 , 1 } |
3 |
|
neg1ne0 |
โข - 1 โ 0 |
4 |
|
neg1cn |
โข - 1 โ โ |
5 |
|
ax-1cn |
โข 1 โ โ |
6 |
|
prssi |
โข ( ( - 1 โ โ โง 1 โ โ ) โ { - 1 , 1 } โ โ ) |
7 |
4 5 6
|
mp2an |
โข { - 1 , 1 } โ โ |
8 |
|
elpri |
โข ( ๐ฅ โ { - 1 , 1 } โ ( ๐ฅ = - 1 โจ ๐ฅ = 1 ) ) |
9 |
7
|
sseli |
โข ( ๐ฆ โ { - 1 , 1 } โ ๐ฆ โ โ ) |
10 |
9
|
mulm1d |
โข ( ๐ฆ โ { - 1 , 1 } โ ( - 1 ยท ๐ฆ ) = - ๐ฆ ) |
11 |
|
elpri |
โข ( ๐ฆ โ { - 1 , 1 } โ ( ๐ฆ = - 1 โจ ๐ฆ = 1 ) ) |
12 |
|
negeq |
โข ( ๐ฆ = - 1 โ - ๐ฆ = - - 1 ) |
13 |
|
negneg1e1 |
โข - - 1 = 1 |
14 |
|
1ex |
โข 1 โ V |
15 |
14
|
prid2 |
โข 1 โ { - 1 , 1 } |
16 |
13 15
|
eqeltri |
โข - - 1 โ { - 1 , 1 } |
17 |
12 16
|
eqeltrdi |
โข ( ๐ฆ = - 1 โ - ๐ฆ โ { - 1 , 1 } ) |
18 |
|
negeq |
โข ( ๐ฆ = 1 โ - ๐ฆ = - 1 ) |
19 |
18 2
|
eqeltrdi |
โข ( ๐ฆ = 1 โ - ๐ฆ โ { - 1 , 1 } ) |
20 |
17 19
|
jaoi |
โข ( ( ๐ฆ = - 1 โจ ๐ฆ = 1 ) โ - ๐ฆ โ { - 1 , 1 } ) |
21 |
11 20
|
syl |
โข ( ๐ฆ โ { - 1 , 1 } โ - ๐ฆ โ { - 1 , 1 } ) |
22 |
10 21
|
eqeltrd |
โข ( ๐ฆ โ { - 1 , 1 } โ ( - 1 ยท ๐ฆ ) โ { - 1 , 1 } ) |
23 |
|
oveq1 |
โข ( ๐ฅ = - 1 โ ( ๐ฅ ยท ๐ฆ ) = ( - 1 ยท ๐ฆ ) ) |
24 |
23
|
eleq1d |
โข ( ๐ฅ = - 1 โ ( ( ๐ฅ ยท ๐ฆ ) โ { - 1 , 1 } โ ( - 1 ยท ๐ฆ ) โ { - 1 , 1 } ) ) |
25 |
22 24
|
imbitrrid |
โข ( ๐ฅ = - 1 โ ( ๐ฆ โ { - 1 , 1 } โ ( ๐ฅ ยท ๐ฆ ) โ { - 1 , 1 } ) ) |
26 |
9
|
mullidd |
โข ( ๐ฆ โ { - 1 , 1 } โ ( 1 ยท ๐ฆ ) = ๐ฆ ) |
27 |
|
id |
โข ( ๐ฆ โ { - 1 , 1 } โ ๐ฆ โ { - 1 , 1 } ) |
28 |
26 27
|
eqeltrd |
โข ( ๐ฆ โ { - 1 , 1 } โ ( 1 ยท ๐ฆ ) โ { - 1 , 1 } ) |
29 |
|
oveq1 |
โข ( ๐ฅ = 1 โ ( ๐ฅ ยท ๐ฆ ) = ( 1 ยท ๐ฆ ) ) |
30 |
29
|
eleq1d |
โข ( ๐ฅ = 1 โ ( ( ๐ฅ ยท ๐ฆ ) โ { - 1 , 1 } โ ( 1 ยท ๐ฆ ) โ { - 1 , 1 } ) ) |
31 |
28 30
|
imbitrrid |
โข ( ๐ฅ = 1 โ ( ๐ฆ โ { - 1 , 1 } โ ( ๐ฅ ยท ๐ฆ ) โ { - 1 , 1 } ) ) |
32 |
25 31
|
jaoi |
โข ( ( ๐ฅ = - 1 โจ ๐ฅ = 1 ) โ ( ๐ฆ โ { - 1 , 1 } โ ( ๐ฅ ยท ๐ฆ ) โ { - 1 , 1 } ) ) |
33 |
8 32
|
syl |
โข ( ๐ฅ โ { - 1 , 1 } โ ( ๐ฆ โ { - 1 , 1 } โ ( ๐ฅ ยท ๐ฆ ) โ { - 1 , 1 } ) ) |
34 |
33
|
imp |
โข ( ( ๐ฅ โ { - 1 , 1 } โง ๐ฆ โ { - 1 , 1 } ) โ ( ๐ฅ ยท ๐ฆ ) โ { - 1 , 1 } ) |
35 |
|
oveq2 |
โข ( ๐ฅ = - 1 โ ( 1 / ๐ฅ ) = ( 1 / - 1 ) ) |
36 |
|
ax-1ne0 |
โข 1 โ 0 |
37 |
|
divneg2 |
โข ( ( 1 โ โ โง 1 โ โ โง 1 โ 0 ) โ - ( 1 / 1 ) = ( 1 / - 1 ) ) |
38 |
5 5 36 37
|
mp3an |
โข - ( 1 / 1 ) = ( 1 / - 1 ) |
39 |
|
1div1e1 |
โข ( 1 / 1 ) = 1 |
40 |
39
|
negeqi |
โข - ( 1 / 1 ) = - 1 |
41 |
38 40
|
eqtr3i |
โข ( 1 / - 1 ) = - 1 |
42 |
41 2
|
eqeltri |
โข ( 1 / - 1 ) โ { - 1 , 1 } |
43 |
35 42
|
eqeltrdi |
โข ( ๐ฅ = - 1 โ ( 1 / ๐ฅ ) โ { - 1 , 1 } ) |
44 |
|
oveq2 |
โข ( ๐ฅ = 1 โ ( 1 / ๐ฅ ) = ( 1 / 1 ) ) |
45 |
39 15
|
eqeltri |
โข ( 1 / 1 ) โ { - 1 , 1 } |
46 |
44 45
|
eqeltrdi |
โข ( ๐ฅ = 1 โ ( 1 / ๐ฅ ) โ { - 1 , 1 } ) |
47 |
43 46
|
jaoi |
โข ( ( ๐ฅ = - 1 โจ ๐ฅ = 1 ) โ ( 1 / ๐ฅ ) โ { - 1 , 1 } ) |
48 |
8 47
|
syl |
โข ( ๐ฅ โ { - 1 , 1 } โ ( 1 / ๐ฅ ) โ { - 1 , 1 } ) |
49 |
48
|
adantr |
โข ( ( ๐ฅ โ { - 1 , 1 } โง ๐ฅ โ 0 ) โ ( 1 / ๐ฅ ) โ { - 1 , 1 } ) |
50 |
7 34 15 49
|
expcl2lem |
โข ( ( - 1 โ { - 1 , 1 } โง - 1 โ 0 โง ๐ โ โค ) โ ( - 1 โ ๐ ) โ { - 1 , 1 } ) |
51 |
2 3 50
|
mp3an12 |
โข ( ๐ โ โค โ ( - 1 โ ๐ ) โ { - 1 , 1 } ) |