Step | Hyp | Ref
| Expression |
1 | | halfnz 12586 |
. . . . . . . . . . 11
โข ยฌ (1
/ 2) โ โค |
2 | | eleq1 2822 |
. . . . . . . . . . 11
โข ((1 / 2)
= -๐ฅ โ ((1 / 2) โ
โค โ -๐ฅ โ
โค)) |
3 | 1, 2 | mtbii 326 |
. . . . . . . . . 10
โข ((1 / 2)
= -๐ฅ โ ยฌ -๐ฅ โ
โค) |
4 | | znegcl 12543 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ -๐ฅ โ
โค) |
5 | 3, 4 | nsyl3 138 |
. . . . . . . . 9
โข (๐ฅ โ โค โ ยฌ (1
/ 2) = -๐ฅ) |
6 | | eqcom 2740 |
. . . . . . . . 9
โข (-๐ฅ = (1 / 2) โ (1 / 2) =
-๐ฅ) |
7 | 5, 6 | sylnibr 329 |
. . . . . . . 8
โข (๐ฅ โ โค โ ยฌ
-๐ฅ = (1 /
2)) |
8 | | ax-1cn 11114 |
. . . . . . . . . . . 12
โข 1 โ
โ |
9 | | 2cn 12233 |
. . . . . . . . . . . 12
โข 2 โ
โ |
10 | | 2ne0 12262 |
. . . . . . . . . . . 12
โข 2 โ
0 |
11 | | divneg 11852 |
. . . . . . . . . . . . 13
โข ((1
โ โ โง 2 โ โ โง 2 โ 0) โ -(1 / 2) = (-1 /
2)) |
12 | 11 | eqcomd 2739 |
. . . . . . . . . . . 12
โข ((1
โ โ โง 2 โ โ โง 2 โ 0) โ (-1 / 2) = -(1 /
2)) |
13 | 8, 9, 10, 12 | mp3an 1462 |
. . . . . . . . . . 11
โข (-1 / 2)
= -(1 / 2) |
14 | 13 | a1i 11 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ (-1 / 2)
= -(1 / 2)) |
15 | 14 | eqeq1d 2735 |
. . . . . . . . 9
โข (๐ฅ โ โค โ ((-1 / 2)
= ๐ฅ โ -(1 / 2) = ๐ฅ)) |
16 | | halfcn 12373 |
. . . . . . . . . . 11
โข (1 / 2)
โ โ |
17 | 16 | a1i 11 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ (1 / 2)
โ โ) |
18 | | zcn 12509 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
19 | 17, 18 | negcon1d 11511 |
. . . . . . . . 9
โข (๐ฅ โ โค โ (-(1 / 2)
= ๐ฅ โ -๐ฅ = (1 / 2))) |
20 | 15, 19 | bitrd 279 |
. . . . . . . 8
โข (๐ฅ โ โค โ ((-1 / 2)
= ๐ฅ โ -๐ฅ = (1 / 2))) |
21 | 7, 20 | mtbird 325 |
. . . . . . 7
โข (๐ฅ โ โค โ ยฌ (-1
/ 2) = ๐ฅ) |
22 | | neg1cn 12272 |
. . . . . . . . 9
โข -1 โ
โ |
23 | 22 | a1i 11 |
. . . . . . . 8
โข (๐ฅ โ โค โ -1 โ
โ) |
24 | | 2cnd 12236 |
. . . . . . . 8
โข (๐ฅ โ โค โ 2 โ
โ) |
25 | 10 | a1i 11 |
. . . . . . . 8
โข (๐ฅ โ โค โ 2 โ
0) |
26 | 23, 18, 24, 25 | divmul2d 11969 |
. . . . . . 7
โข (๐ฅ โ โค โ ((-1 / 2)
= ๐ฅ โ -1 = (2 ยท
๐ฅ))) |
27 | 21, 26 | mtbid 324 |
. . . . . 6
โข (๐ฅ โ โค โ ยฌ -1
= (2 ยท ๐ฅ)) |
28 | | eqcom 2740 |
. . . . . . . 8
โข (0 = ((2
ยท ๐ฅ) + 1) โ ((2
ยท ๐ฅ) + 1) =
0) |
29 | 28 | a1i 11 |
. . . . . . 7
โข (๐ฅ โ โค โ (0 = ((2
ยท ๐ฅ) + 1) โ ((2
ยท ๐ฅ) + 1) =
0)) |
30 | | 0cnd 11153 |
. . . . . . . 8
โข (๐ฅ โ โค โ 0 โ
โ) |
31 | | 1cnd 11155 |
. . . . . . . 8
โข (๐ฅ โ โค โ 1 โ
โ) |
32 | 24, 18 | mulcld 11180 |
. . . . . . . 8
โข (๐ฅ โ โค โ (2
ยท ๐ฅ) โ
โ) |
33 | | subadd2 11410 |
. . . . . . . . 9
โข ((0
โ โ โง 1 โ โ โง (2 ยท ๐ฅ) โ โ) โ ((0 โ 1) = (2
ยท ๐ฅ) โ ((2
ยท ๐ฅ) + 1) =
0)) |
34 | 33 | bicomd 222 |
. . . . . . . 8
โข ((0
โ โ โง 1 โ โ โง (2 ยท ๐ฅ) โ โ) โ (((2 ยท ๐ฅ) + 1) = 0 โ (0 โ 1)
= (2 ยท ๐ฅ))) |
35 | 30, 31, 32, 34 | syl3anc 1372 |
. . . . . . 7
โข (๐ฅ โ โค โ (((2
ยท ๐ฅ) + 1) = 0 โ
(0 โ 1) = (2 ยท ๐ฅ))) |
36 | | df-neg 11393 |
. . . . . . . . . 10
โข -1 = (0
โ 1) |
37 | 36 | eqcomi 2742 |
. . . . . . . . 9
โข (0
โ 1) = -1 |
38 | 37 | a1i 11 |
. . . . . . . 8
โข (๐ฅ โ โค โ (0
โ 1) = -1) |
39 | 38 | eqeq1d 2735 |
. . . . . . 7
โข (๐ฅ โ โค โ ((0
โ 1) = (2 ยท ๐ฅ)
โ -1 = (2 ยท ๐ฅ))) |
40 | 29, 35, 39 | 3bitrd 305 |
. . . . . 6
โข (๐ฅ โ โค โ (0 = ((2
ยท ๐ฅ) + 1) โ -1
= (2 ยท ๐ฅ))) |
41 | 27, 40 | mtbird 325 |
. . . . 5
โข (๐ฅ โ โค โ ยฌ 0 =
((2 ยท ๐ฅ) +
1)) |
42 | 41 | nrex 3074 |
. . . 4
โข ยฌ
โ๐ฅ โ โค 0 =
((2 ยท ๐ฅ) +
1) |
43 | 42 | intnan 488 |
. . 3
โข ยฌ (0
โ โค โง โ๐ฅ โ โค 0 = ((2 ยท ๐ฅ) + 1)) |
44 | | eqeq1 2737 |
. . . . 5
โข (๐ง = 0 โ (๐ง = ((2 ยท ๐ฅ) + 1) โ 0 = ((2 ยท ๐ฅ) + 1))) |
45 | 44 | rexbidv 3172 |
. . . 4
โข (๐ง = 0 โ (โ๐ฅ โ โค ๐ง = ((2 ยท ๐ฅ) + 1) โ โ๐ฅ โ โค 0 = ((2 ยท
๐ฅ) + 1))) |
46 | | oddinmgm.e |
. . . 4
โข ๐ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = ((2 ยท ๐ฅ) + 1)} |
47 | 45, 46 | elrab2 3649 |
. . 3
โข (0 โ
๐ โ (0 โ โค
โง โ๐ฅ โ
โค 0 = ((2 ยท ๐ฅ)
+ 1))) |
48 | 43, 47 | mtbir 323 |
. 2
โข ยฌ 0
โ ๐ |
49 | 48 | nelir 3049 |
1
โข 0 โ
๐ |