Step | Hyp | Ref
| Expression |
1 | | negex 11407 |
. . 3
โข -1 โ
V |
2 | 1 | prid1 4727 |
. 2
โข -1 โ
{-1, 1} |
3 | | neg1ne0 12277 |
. 2
โข -1 โ
0 |
4 | | neg1cn 12275 |
. . . 4
โข -1 โ
โ |
5 | | ax-1cn 11117 |
. . . 4
โข 1 โ
โ |
6 | | prssi 4785 |
. . . 4
โข ((-1
โ โ โง 1 โ โ) โ {-1, 1} โ
โ) |
7 | 4, 5, 6 | mp2an 691 |
. . 3
โข {-1, 1}
โ โ |
8 | | elpri 4612 |
. . . . 5
โข (๐ฅ โ {-1, 1} โ (๐ฅ = -1 โจ ๐ฅ = 1)) |
9 | 7 | sseli 3944 |
. . . . . . . . 9
โข (๐ฆ โ {-1, 1} โ ๐ฆ โ
โ) |
10 | 9 | mulm1d 11615 |
. . . . . . . 8
โข (๐ฆ โ {-1, 1} โ (-1
ยท ๐ฆ) = -๐ฆ) |
11 | | elpri 4612 |
. . . . . . . . 9
โข (๐ฆ โ {-1, 1} โ (๐ฆ = -1 โจ ๐ฆ = 1)) |
12 | | negeq 11401 |
. . . . . . . . . . 11
โข (๐ฆ = -1 โ -๐ฆ = --1) |
13 | | negneg1e1 12279 |
. . . . . . . . . . . 12
โข --1 =
1 |
14 | | 1ex 11159 |
. . . . . . . . . . . . 13
โข 1 โ
V |
15 | 14 | prid2 4728 |
. . . . . . . . . . . 12
โข 1 โ
{-1, 1} |
16 | 13, 15 | eqeltri 2830 |
. . . . . . . . . . 11
โข --1
โ {-1, 1} |
17 | 12, 16 | eqeltrdi 2842 |
. . . . . . . . . 10
โข (๐ฆ = -1 โ -๐ฆ โ {-1, 1}) |
18 | | negeq 11401 |
. . . . . . . . . . 11
โข (๐ฆ = 1 โ -๐ฆ = -1) |
19 | 18, 2 | eqeltrdi 2842 |
. . . . . . . . . 10
โข (๐ฆ = 1 โ -๐ฆ โ {-1, 1}) |
20 | 17, 19 | jaoi 856 |
. . . . . . . . 9
โข ((๐ฆ = -1 โจ ๐ฆ = 1) โ -๐ฆ โ {-1, 1}) |
21 | 11, 20 | syl 17 |
. . . . . . . 8
โข (๐ฆ โ {-1, 1} โ -๐ฆ โ {-1,
1}) |
22 | 10, 21 | eqeltrd 2834 |
. . . . . . 7
โข (๐ฆ โ {-1, 1} โ (-1
ยท ๐ฆ) โ {-1,
1}) |
23 | | oveq1 7368 |
. . . . . . . 8
โข (๐ฅ = -1 โ (๐ฅ ยท ๐ฆ) = (-1 ยท ๐ฆ)) |
24 | 23 | eleq1d 2819 |
. . . . . . 7
โข (๐ฅ = -1 โ ((๐ฅ ยท ๐ฆ) โ {-1, 1} โ (-1 ยท ๐ฆ) โ {-1,
1})) |
25 | 22, 24 | imbitrrid 245 |
. . . . . 6
โข (๐ฅ = -1 โ (๐ฆ โ {-1, 1} โ (๐ฅ ยท ๐ฆ) โ {-1, 1})) |
26 | 9 | mullidd 11181 |
. . . . . . . 8
โข (๐ฆ โ {-1, 1} โ (1
ยท ๐ฆ) = ๐ฆ) |
27 | | id 22 |
. . . . . . . 8
โข (๐ฆ โ {-1, 1} โ ๐ฆ โ {-1,
1}) |
28 | 26, 27 | eqeltrd 2834 |
. . . . . . 7
โข (๐ฆ โ {-1, 1} โ (1
ยท ๐ฆ) โ {-1,
1}) |
29 | | oveq1 7368 |
. . . . . . . 8
โข (๐ฅ = 1 โ (๐ฅ ยท ๐ฆ) = (1 ยท ๐ฆ)) |
30 | 29 | eleq1d 2819 |
. . . . . . 7
โข (๐ฅ = 1 โ ((๐ฅ ยท ๐ฆ) โ {-1, 1} โ (1 ยท ๐ฆ) โ {-1,
1})) |
31 | 28, 30 | imbitrrid 245 |
. . . . . 6
โข (๐ฅ = 1 โ (๐ฆ โ {-1, 1} โ (๐ฅ ยท ๐ฆ) โ {-1, 1})) |
32 | 25, 31 | jaoi 856 |
. . . . 5
โข ((๐ฅ = -1 โจ ๐ฅ = 1) โ (๐ฆ โ {-1, 1} โ (๐ฅ ยท ๐ฆ) โ {-1, 1})) |
33 | 8, 32 | syl 17 |
. . . 4
โข (๐ฅ โ {-1, 1} โ (๐ฆ โ {-1, 1} โ (๐ฅ ยท ๐ฆ) โ {-1, 1})) |
34 | 33 | imp 408 |
. . 3
โข ((๐ฅ โ {-1, 1} โง ๐ฆ โ {-1, 1}) โ (๐ฅ ยท ๐ฆ) โ {-1, 1}) |
35 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = -1 โ (1 / ๐ฅ) = (1 / -1)) |
36 | | ax-1ne0 11128 |
. . . . . . . . . 10
โข 1 โ
0 |
37 | | divneg2 11887 |
. . . . . . . . . 10
โข ((1
โ โ โง 1 โ โ โง 1 โ 0) โ -(1 / 1) = (1 /
-1)) |
38 | 5, 5, 36, 37 | mp3an 1462 |
. . . . . . . . 9
โข -(1 / 1)
= (1 / -1) |
39 | | 1div1e1 11853 |
. . . . . . . . . 10
โข (1 / 1) =
1 |
40 | 39 | negeqi 11402 |
. . . . . . . . 9
โข -(1 / 1)
= -1 |
41 | 38, 40 | eqtr3i 2763 |
. . . . . . . 8
โข (1 / -1)
= -1 |
42 | 41, 2 | eqeltri 2830 |
. . . . . . 7
โข (1 / -1)
โ {-1, 1} |
43 | 35, 42 | eqeltrdi 2842 |
. . . . . 6
โข (๐ฅ = -1 โ (1 / ๐ฅ) โ {-1,
1}) |
44 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = 1 โ (1 / ๐ฅ) = (1 / 1)) |
45 | 39, 15 | eqeltri 2830 |
. . . . . . 7
โข (1 / 1)
โ {-1, 1} |
46 | 44, 45 | eqeltrdi 2842 |
. . . . . 6
โข (๐ฅ = 1 โ (1 / ๐ฅ) โ {-1,
1}) |
47 | 43, 46 | jaoi 856 |
. . . . 5
โข ((๐ฅ = -1 โจ ๐ฅ = 1) โ (1 / ๐ฅ) โ {-1, 1}) |
48 | 8, 47 | syl 17 |
. . . 4
โข (๐ฅ โ {-1, 1} โ (1 /
๐ฅ) โ {-1,
1}) |
49 | 48 | adantr 482 |
. . 3
โข ((๐ฅ โ {-1, 1} โง ๐ฅ โ 0) โ (1 / ๐ฅ) โ {-1,
1}) |
50 | 7, 34, 15, 49 | expcl2lem 13988 |
. 2
โข ((-1
โ {-1, 1} โง -1 โ 0 โง ๐ โ โค) โ (-1โ๐) โ {-1,
1}) |
51 | 2, 3, 50 | mp3an12 1452 |
1
โข (๐ โ โค โ
(-1โ๐) โ {-1,
1}) |