Step | Hyp | Ref
| Expression |
1 | | 2re 12251 |
. . . . . 6
โข 2 โ
โ |
2 | | remulcl 11160 |
. . . . . 6
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
3 | 1, 2 | mpan 688 |
. . . . 5
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
4 | | 1re 11179 |
. . . . 5
โข 1 โ
โ |
5 | | resubcl 11489 |
. . . . 5
โข (((2
ยท ๐) โ โ
โง 1 โ โ) โ ((2 ยท ๐) โ 1) โ
โ) |
6 | 3, 4, 5 | sylancl 586 |
. . . 4
โข (๐ โ โ โ ((2
ยท ๐) โ 1)
โ โ) |
7 | 6 | 3ad2ant1 1133 |
. . 3
โข ((๐ โ โ โง (1 / 2)
โค ๐ โง ๐ โค 1) โ ((2 ยท
๐) โ 1) โ
โ) |
8 | | subge0 11692 |
. . . . . . 7
โข (((2
ยท ๐) โ โ
โง 1 โ โ) โ (0 โค ((2 ยท ๐) โ 1) โ 1 โค (2 ยท ๐))) |
9 | 3, 4, 8 | sylancl 586 |
. . . . . 6
โข (๐ โ โ โ (0 โค
((2 ยท ๐) โ 1)
โ 1 โค (2 ยท ๐))) |
10 | | 2pos 12280 |
. . . . . . . 8
โข 0 <
2 |
11 | 1, 10 | pm3.2i 471 |
. . . . . . 7
โข (2 โ
โ โง 0 < 2) |
12 | | ledivmul 12055 |
. . . . . . 7
โข ((1
โ โ โง ๐
โ โ โง (2 โ โ โง 0 < 2)) โ ((1 / 2) โค
๐ โ 1 โค (2 ยท
๐))) |
13 | 4, 11, 12 | mp3an13 1452 |
. . . . . 6
โข (๐ โ โ โ ((1 / 2)
โค ๐ โ 1 โค (2
ยท ๐))) |
14 | 9, 13 | bitr4d 281 |
. . . . 5
โข (๐ โ โ โ (0 โค
((2 ยท ๐) โ 1)
โ (1 / 2) โค ๐)) |
15 | 14 | biimpar 478 |
. . . 4
โข ((๐ โ โ โง (1 / 2)
โค ๐) โ 0 โค ((2
ยท ๐) โ
1)) |
16 | 15 | 3adant3 1132 |
. . 3
โข ((๐ โ โ โง (1 / 2)
โค ๐ โง ๐ โค 1) โ 0 โค ((2
ยท ๐) โ
1)) |
17 | | ax-1cn 11133 |
. . . . . . . . 9
โข 1 โ
โ |
18 | 17 | 2timesi 12315 |
. . . . . . . 8
โข (2
ยท 1) = (1 + 1) |
19 | 18 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ (2
ยท 1) = (1 + 1)) |
20 | 19 | breq2d 5137 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท ๐) โค (2
ยท 1) โ (2 ยท ๐) โค (1 + 1))) |
21 | | lemul2 12032 |
. . . . . . 7
โข ((๐ โ โ โง 1 โ
โ โง (2 โ โ โง 0 < 2)) โ (๐ โค 1 โ (2 ยท ๐) โค (2 ยท 1))) |
22 | 4, 11, 21 | mp3an23 1453 |
. . . . . 6
โข (๐ โ โ โ (๐ โค 1 โ (2 ยท ๐) โค (2 ยท
1))) |
23 | | lesubadd 11651 |
. . . . . . . 8
โข (((2
ยท ๐) โ โ
โง 1 โ โ โง 1 โ โ) โ (((2 ยท ๐) โ 1) โค 1 โ (2
ยท ๐) โค (1 +
1))) |
24 | 4, 4, 23 | mp3an23 1453 |
. . . . . . 7
โข ((2
ยท ๐) โ โ
โ (((2 ยท ๐)
โ 1) โค 1 โ (2 ยท ๐) โค (1 + 1))) |
25 | 3, 24 | syl 17 |
. . . . . 6
โข (๐ โ โ โ (((2
ยท ๐) โ 1) โค
1 โ (2 ยท ๐)
โค (1 + 1))) |
26 | 20, 22, 25 | 3bitr4d 310 |
. . . . 5
โข (๐ โ โ โ (๐ โค 1 โ ((2 ยท
๐) โ 1) โค
1)) |
27 | 26 | biimpa 477 |
. . . 4
โข ((๐ โ โ โง ๐ โค 1) โ ((2 ยท
๐) โ 1) โค
1) |
28 | 27 | 3adant2 1131 |
. . 3
โข ((๐ โ โ โง (1 / 2)
โค ๐ โง ๐ โค 1) โ ((2 ยท
๐) โ 1) โค
1) |
29 | 7, 16, 28 | 3jca 1128 |
. 2
โข ((๐ โ โ โง (1 / 2)
โค ๐ โง ๐ โค 1) โ (((2 ยท
๐) โ 1) โ
โ โง 0 โค ((2 ยท ๐) โ 1) โง ((2 ยท ๐) โ 1) โค
1)) |
30 | | halfre 12391 |
. . 3
โข (1 / 2)
โ โ |
31 | 30, 4 | elicc2i 13355 |
. 2
โข (๐ โ ((1 / 2)[,]1) โ
(๐ โ โ โง (1
/ 2) โค ๐ โง ๐ โค 1)) |
32 | | elicc01 13408 |
. 2
โข (((2
ยท ๐) โ 1)
โ (0[,]1) โ (((2 ยท ๐) โ 1) โ โ โง 0 โค ((2
ยท ๐) โ 1)
โง ((2 ยท ๐)
โ 1) โค 1)) |
33 | 29, 31, 32 | 3imtr4i 291 |
1
โข (๐ โ ((1 / 2)[,]1) โ ((2
ยท ๐) โ 1)
โ (0[,]1)) |