Step | Hyp | Ref
| Expression |
1 | | nnex 8927 |
. . 3
โข โ
โ V |
2 | 1 | rabex 4149 |
. 2
โข {๐ง โ โ โฃ 2
โฅ ๐ง} โ
V |
3 | | breq2 4009 |
. . . 4
โข (๐ง = ๐ฅ โ (2 โฅ ๐ง โ 2 โฅ ๐ฅ)) |
4 | 3 | elrab 2895 |
. . 3
โข (๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โ (๐ฅ โ โ โง 2 โฅ ๐ฅ)) |
5 | | nnehalf 11911 |
. . 3
โข ((๐ฅ โ โ โง 2 โฅ
๐ฅ) โ (๐ฅ / 2) โ
โ) |
6 | 4, 5 | sylbi 121 |
. 2
โข (๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โ (๐ฅ / 2) โ โ) |
7 | | 2nn 9082 |
. . . . 5
โข 2 โ
โ |
8 | 7 | a1i 9 |
. . . 4
โข (๐ฆ โ โ โ 2 โ
โ) |
9 | | id 19 |
. . . 4
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
10 | 8, 9 | nnmulcld 8970 |
. . 3
โข (๐ฆ โ โ โ (2
ยท ๐ฆ) โ
โ) |
11 | | 2z 9283 |
. . . 4
โข 2 โ
โค |
12 | | nnz 9274 |
. . . 4
โข (๐ฆ โ โ โ ๐ฆ โ
โค) |
13 | | dvdsmul1 11822 |
. . . 4
โข ((2
โ โค โง ๐ฆ
โ โค) โ 2 โฅ (2 ยท ๐ฆ)) |
14 | 11, 12, 13 | sylancr 414 |
. . 3
โข (๐ฆ โ โ โ 2 โฅ
(2 ยท ๐ฆ)) |
15 | | breq2 4009 |
. . . 4
โข (๐ง = (2 ยท ๐ฆ) โ (2 โฅ ๐ง โ 2 โฅ (2 ยท
๐ฆ))) |
16 | 15 | elrab 2895 |
. . 3
โข ((2
ยท ๐ฆ) โ {๐ง โ โ โฃ 2
โฅ ๐ง} โ ((2
ยท ๐ฆ) โ โ
โง 2 โฅ (2 ยท ๐ฆ))) |
17 | 10, 14, 16 | sylanbrc 417 |
. 2
โข (๐ฆ โ โ โ (2
ยท ๐ฆ) โ {๐ง โ โ โฃ 2
โฅ ๐ง}) |
18 | | elrabi 2892 |
. . . . . 6
โข (๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โ ๐ฅ โ โ) |
19 | 18 | adantr 276 |
. . . . 5
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ๐ฅ โ โ) |
20 | 19 | nncnd 8935 |
. . . 4
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ๐ฅ โ โ) |
21 | | simpr 110 |
. . . . 5
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ๐ฆ โ โ) |
22 | 21 | nncnd 8935 |
. . . 4
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ๐ฆ โ โ) |
23 | | 2cnd 8994 |
. . . 4
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ 2 โ
โ) |
24 | | 2ap0 9014 |
. . . . 5
โข 2 #
0 |
25 | 24 | a1i 9 |
. . . 4
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ 2 #
0) |
26 | 20, 22, 23, 25 | divmulap3d 8784 |
. . 3
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ((๐ฅ / 2) = ๐ฆ โ ๐ฅ = (๐ฆ ยท 2))) |
27 | | eqcom 2179 |
. . . 4
โข ((๐ฅ / 2) = ๐ฆ โ ๐ฆ = (๐ฅ / 2)) |
28 | 27 | a1i 9 |
. . 3
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ((๐ฅ / 2) = ๐ฆ โ ๐ฆ = (๐ฅ / 2))) |
29 | 22, 23 | mulcomd 7981 |
. . . 4
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ (๐ฆ ยท 2) = (2 ยท ๐ฆ)) |
30 | 29 | eqeq2d 2189 |
. . 3
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ (๐ฅ = (๐ฆ ยท 2) โ ๐ฅ = (2 ยท ๐ฆ))) |
31 | 26, 28, 30 | 3bitr3rd 219 |
. 2
โข ((๐ฅ โ {๐ง โ โ โฃ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ (๐ฅ = (2 ยท ๐ฆ) โ ๐ฆ = (๐ฅ / 2))) |
32 | 2, 1, 6, 17, 31 | en3i 6773 |
1
โข {๐ง โ โ โฃ 2
โฅ ๐ง} โ
โ |