Step | Hyp | Ref
| Expression |
1 | | 2z 9281 |
. . . . . . 7
โข 2 โ
โค |
2 | 1 | a1i 9 |
. . . . . 6
โข (๐ โ โค โ 2 โ
โค) |
3 | | id 19 |
. . . . . 6
โข (๐ โ โค โ ๐ โ
โค) |
4 | 2, 3 | zmulcld 9381 |
. . . . 5
โข (๐ โ โค โ (2
ยท ๐) โ
โค) |
5 | 4 | peano2zd 9378 |
. . . 4
โข (๐ โ โค โ ((2
ยท ๐) + 1) โ
โค) |
6 | 5 | zred 9375 |
. . 3
โข (๐ โ โค โ ((2
ยท ๐) + 1) โ
โ) |
7 | | 2re 8989 |
. . . 4
โข 2 โ
โ |
8 | 7 | a1i 9 |
. . 3
โข (๐ โ โค โ 2 โ
โ) |
9 | | 2pos 9010 |
. . . 4
โข 0 <
2 |
10 | 9 | a1i 9 |
. . 3
โข (๐ โ โค โ 0 <
2) |
11 | | ge0div 8828 |
. . 3
โข ((((2
ยท ๐) + 1) โ
โ โง 2 โ โ โง 0 < 2) โ (0 โค ((2 ยท
๐) + 1) โ 0 โค (((2
ยท ๐) + 1) /
2))) |
12 | 6, 8, 10, 11 | syl3anc 1238 |
. 2
โข (๐ โ โค โ (0 โค
((2 ยท ๐) + 1) โ
0 โค (((2 ยท ๐) +
1) / 2))) |
13 | 4 | zcnd 9376 |
. . . . 5
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
14 | | 1cnd 7973 |
. . . . 5
โข (๐ โ โค โ 1 โ
โ) |
15 | | 2cn 8990 |
. . . . . . 7
โข 2 โ
โ |
16 | | 2ap0 9012 |
. . . . . . 7
โข 2 #
0 |
17 | 15, 16 | pm3.2i 272 |
. . . . . 6
โข (2 โ
โ โง 2 # 0) |
18 | 17 | a1i 9 |
. . . . 5
โข (๐ โ โค โ (2 โ
โ โง 2 # 0)) |
19 | | divdirap 8654 |
. . . . 5
โข (((2
ยท ๐) โ โ
โง 1 โ โ โง (2 โ โ โง 2 # 0)) โ (((2
ยท ๐) + 1) / 2) =
(((2 ยท ๐) / 2) + (1
/ 2))) |
20 | 13, 14, 18, 19 | syl3anc 1238 |
. . . 4
โข (๐ โ โค โ (((2
ยท ๐) + 1) / 2) =
(((2 ยท ๐) / 2) + (1
/ 2))) |
21 | | zcn 9258 |
. . . . . 6
โข (๐ โ โค โ ๐ โ
โ) |
22 | | 2cnd 8992 |
. . . . . 6
โข (๐ โ โค โ 2 โ
โ) |
23 | 16 | a1i 9 |
. . . . . 6
โข (๐ โ โค โ 2 #
0) |
24 | 21, 22, 23 | divcanap3d 8752 |
. . . . 5
โข (๐ โ โค โ ((2
ยท ๐) / 2) = ๐) |
25 | 24 | oveq1d 5890 |
. . . 4
โข (๐ โ โค โ (((2
ยท ๐) / 2) + (1 / 2))
= (๐ + (1 /
2))) |
26 | 20, 25 | eqtrd 2210 |
. . 3
โข (๐ โ โค โ (((2
ยท ๐) + 1) / 2) =
(๐ + (1 /
2))) |
27 | 26 | breq2d 4016 |
. 2
โข (๐ โ โค โ (0 โค
(((2 ยท ๐) + 1) / 2)
โ 0 โค (๐ + (1 /
2)))) |
28 | | zre 9257 |
. . . 4
โข (๐ โ โค โ ๐ โ
โ) |
29 | | halfre 9132 |
. . . . 5
โข (1 / 2)
โ โ |
30 | 29 | a1i 9 |
. . . 4
โข (๐ โ โค โ (1 / 2)
โ โ) |
31 | 28, 30 | readdcld 7987 |
. . 3
โข (๐ โ โค โ (๐ + (1 / 2)) โ
โ) |
32 | | halfge0 9135 |
. . . 4
โข 0 โค (1
/ 2) |
33 | 28, 30 | addge01d 8490 |
. . . 4
โข (๐ โ โค โ (0 โค
(1 / 2) โ ๐ โค
(๐ + (1 /
2)))) |
34 | 32, 33 | mpbii 148 |
. . 3
โข (๐ โ โค โ ๐ โค (๐ + (1 / 2))) |
35 | | 1red 7972 |
. . . 4
โข (๐ โ โค โ 1 โ
โ) |
36 | | halflt1 9136 |
. . . . 5
โข (1 / 2)
< 1 |
37 | 36 | a1i 9 |
. . . 4
โข (๐ โ โค โ (1 / 2)
< 1) |
38 | 30, 35, 28, 37 | ltadd2dd 8379 |
. . 3
โข (๐ โ โค โ (๐ + (1 / 2)) < (๐ + 1)) |
39 | | btwnzge0 10300 |
. . 3
โข ((((๐ + (1 / 2)) โ โ โง
๐ โ โค) โง
(๐ โค (๐ + (1 / 2)) โง (๐ + (1 / 2)) < (๐ + 1))) โ (0 โค (๐ + (1 / 2)) โ 0 โค ๐)) |
40 | 31, 3, 34, 38, 39 | syl22anc 1239 |
. 2
โข (๐ โ โค โ (0 โค
(๐ + (1 / 2)) โ 0 โค
๐)) |
41 | 12, 27, 40 | 3bitrd 214 |
1
โข (๐ โ โค โ (0 โค
((2 ยท ๐) + 1) โ
0 โค ๐)) |