Step | Hyp | Ref
| Expression |
1 | | 2z 12466 |
. . . . . 6
โข 2 โ
โค |
2 | | divides 16073 |
. . . . . 6
โข ((2
โ โค โง ๐
โ โค) โ (2 โฅ ๐ โ โ๐ โ โค (๐ ยท 2) = ๐)) |
3 | 1, 2 | mpan 689 |
. . . . 5
โข (๐ โ โค โ (2
โฅ ๐ โ
โ๐ โ โค
(๐ ยท 2) = ๐)) |
4 | | oveq2 7358 |
. . . . . . . 8
โข (๐ = (๐ ยท 2) โ (-1โ๐) = (-1โ(๐ ยท 2))) |
5 | 4 | eqcoms 2746 |
. . . . . . 7
โข ((๐ ยท 2) = ๐ โ (-1โ๐) = (-1โ(๐ ยท 2))) |
6 | | zcn 12438 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
7 | | 2cnd 12165 |
. . . . . . . . . 10
โข (๐ โ โค โ 2 โ
โ) |
8 | 6, 7 | mulcomd 11110 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ ยท 2) = (2 ยท ๐)) |
9 | 8 | oveq2d 7366 |
. . . . . . . 8
โข (๐ โ โค โ
(-1โ(๐ ยท 2)) =
(-1โ(2 ยท ๐))) |
10 | | m1expeven 13944 |
. . . . . . . 8
โข (๐ โ โค โ
(-1โ(2 ยท ๐)) =
1) |
11 | 9, 10 | eqtrd 2778 |
. . . . . . 7
โข (๐ โ โค โ
(-1โ(๐ ยท 2)) =
1) |
12 | 5, 11 | sylan9eqr 2800 |
. . . . . 6
โข ((๐ โ โค โง (๐ ยท 2) = ๐) โ (-1โ๐) = 1) |
13 | 12 | rexlimiva 3143 |
. . . . 5
โข
(โ๐ โ
โค (๐ ยท 2) =
๐ โ (-1โ๐) = 1) |
14 | 3, 13 | syl6bi 253 |
. . . 4
โข (๐ โ โค โ (2
โฅ ๐ โ
(-1โ๐) =
1)) |
15 | 14 | impcom 409 |
. . 3
โข ((2
โฅ ๐ โง ๐ โ โค) โ
(-1โ๐) =
1) |
16 | | simpl 484 |
. . 3
โข ((2
โฅ ๐ โง ๐ โ โค) โ 2
โฅ ๐) |
17 | 15, 16 | 2thd 265 |
. 2
โข ((2
โฅ ๐ โง ๐ โ โค) โ
((-1โ๐) = 1 โ 2
โฅ ๐)) |
18 | | ax-1ne0 11054 |
. . . . 5
โข 1 โ
0 |
19 | | eqcom 2745 |
. . . . . 6
โข (-1 = 1
โ 1 = -1) |
20 | | ax-1cn 11043 |
. . . . . . 7
โข 1 โ
โ |
21 | 20 | eqnegi 11818 |
. . . . . 6
โข (1 = -1
โ 1 = 0) |
22 | 19, 21 | bitri 275 |
. . . . 5
โข (-1 = 1
โ 1 = 0) |
23 | 18, 22 | nemtbir 3039 |
. . . 4
โข ยฌ -1
= 1 |
24 | | odd2np1 16158 |
. . . . . . 7
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
25 | | oveq2 7358 |
. . . . . . . . . 10
โข (๐ = ((2 ยท ๐) + 1) โ (-1โ๐) = (-1โ((2 ยท ๐) + 1))) |
26 | 25 | eqcoms 2746 |
. . . . . . . . 9
โข (((2
ยท ๐) + 1) = ๐ โ (-1โ๐) = (-1โ((2 ยท ๐) + 1))) |
27 | | neg1cn 12201 |
. . . . . . . . . . . 12
โข -1 โ
โ |
28 | 27 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โค โ -1 โ
โ) |
29 | | neg1ne0 12203 |
. . . . . . . . . . . 12
โข -1 โ
0 |
30 | 29 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โค โ -1 โ
0) |
31 | 1 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โค โ 2 โ
โค) |
32 | | id 22 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โค) |
33 | 31, 32 | zmulcld 12546 |
. . . . . . . . . . 11
โข (๐ โ โค โ (2
ยท ๐) โ
โค) |
34 | 28, 30, 33 | expp1zd 13987 |
. . . . . . . . . 10
โข (๐ โ โค โ
(-1โ((2 ยท ๐) +
1)) = ((-1โ(2 ยท ๐)) ยท -1)) |
35 | 10 | oveq1d 7365 |
. . . . . . . . . . 11
โข (๐ โ โค โ
((-1โ(2 ยท ๐))
ยท -1) = (1 ยท -1)) |
36 | 27 | mulid2i 11094 |
. . . . . . . . . . 11
โข (1
ยท -1) = -1 |
37 | 35, 36 | eqtrdi 2794 |
. . . . . . . . . 10
โข (๐ โ โค โ
((-1โ(2 ยท ๐))
ยท -1) = -1) |
38 | 34, 37 | eqtrd 2778 |
. . . . . . . . 9
โข (๐ โ โค โ
(-1โ((2 ยท ๐) +
1)) = -1) |
39 | 26, 38 | sylan9eqr 2800 |
. . . . . . . 8
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐) โ (-1โ๐) = -1) |
40 | 39 | rexlimiva 3143 |
. . . . . . 7
โข
(โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โ
(-1โ๐) =
-1) |
41 | 24, 40 | syl6bi 253 |
. . . . . 6
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
(-1โ๐) =
-1)) |
42 | 41 | impcom 409 |
. . . . 5
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โค) โ
(-1โ๐) =
-1) |
43 | 42 | eqeq1d 2740 |
. . . 4
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โค) โ
((-1โ๐) = 1 โ -1
= 1)) |
44 | 23, 43 | mtbiri 327 |
. . 3
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โค) โ ยฌ
(-1โ๐) =
1) |
45 | | simpl 484 |
. . 3
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โค) โ ยฌ 2
โฅ ๐) |
46 | 44, 45 | 2falsed 377 |
. 2
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โค) โ
((-1โ๐) = 1 โ 2
โฅ ๐)) |
47 | 17, 46 | pm2.61ian 811 |
1
โข (๐ โ โค โ
((-1โ๐) = 1 โ 2
โฅ ๐)) |