Step | Hyp | Ref
| Expression |
1 | | zre 12508 |
. . . . . . . 8
โข (๐ โ โค โ ๐ โ
โ) |
2 | | peano2re 11333 |
. . . . . . . 8
โข (๐ โ โ โ (๐ + 1) โ
โ) |
3 | 1, 2 | syl 17 |
. . . . . . 7
โข (๐ โ โค โ (๐ + 1) โ
โ) |
4 | 3 | rehalfcld 12405 |
. . . . . 6
โข (๐ โ โค โ ((๐ + 1) / 2) โ
โ) |
5 | | flltp1 13711 |
. . . . . 6
โข (((๐ + 1) / 2) โ โ โ
((๐ + 1) / 2) <
((โโ((๐ + 1) /
2)) + 1)) |
6 | 4, 5 | syl 17 |
. . . . 5
โข (๐ โ โค โ ((๐ + 1) / 2) <
((โโ((๐ + 1) /
2)) + 1)) |
7 | 4 | flcld 13709 |
. . . . . . . 8
โข (๐ โ โค โ
(โโ((๐ + 1) /
2)) โ โค) |
8 | 7 | zred 12612 |
. . . . . . 7
โข (๐ โ โค โ
(โโ((๐ + 1) /
2)) โ โ) |
9 | | 1red 11161 |
. . . . . . 7
โข (๐ โ โค โ 1 โ
โ) |
10 | 8, 9 | readdcld 11189 |
. . . . . 6
โข (๐ โ โค โ
((โโ((๐ + 1) /
2)) + 1) โ โ) |
11 | | 2rp 12925 |
. . . . . . 7
โข 2 โ
โ+ |
12 | 11 | a1i 11 |
. . . . . 6
โข (๐ โ โค โ 2 โ
โ+) |
13 | 3, 10, 12 | ltdivmuld 13013 |
. . . . 5
โข (๐ โ โค โ (((๐ + 1) / 2) <
((โโ((๐ + 1) /
2)) + 1) โ (๐ + 1)
< (2 ยท ((โโ((๐ + 1) / 2)) + 1)))) |
14 | 6, 13 | mpbid 231 |
. . . 4
โข (๐ โ โค โ (๐ + 1) < (2 ยท
((โโ((๐ + 1) /
2)) + 1))) |
15 | 9 | recnd 11188 |
. . . . . . 7
โข (๐ โ โค โ 1 โ
โ) |
16 | 15 | 2timesd 12401 |
. . . . . 6
โข (๐ โ โค โ (2
ยท 1) = (1 + 1)) |
17 | 16 | oveq2d 7374 |
. . . . 5
โข (๐ โ โค โ ((2
ยท (โโ((๐
+ 1) / 2))) + (2 ยท 1)) = ((2 ยท (โโ((๐ + 1) / 2))) + (1 + 1))) |
18 | | 2cnd 12236 |
. . . . . 6
โข (๐ โ โค โ 2 โ
โ) |
19 | 8 | recnd 11188 |
. . . . . 6
โข (๐ โ โค โ
(โโ((๐ + 1) /
2)) โ โ) |
20 | 18, 19, 15 | adddid 11184 |
. . . . 5
โข (๐ โ โค โ (2
ยท ((โโ((๐ + 1) / 2)) + 1)) = ((2 ยท
(โโ((๐ + 1) /
2))) + (2 ยท 1))) |
21 | | 2re 12232 |
. . . . . . . . 9
โข 2 โ
โ |
22 | 21 | a1i 11 |
. . . . . . . 8
โข (๐ โ โค โ 2 โ
โ) |
23 | 22, 8 | remulcld 11190 |
. . . . . . 7
โข (๐ โ โค โ (2
ยท (โโ((๐
+ 1) / 2))) โ โ) |
24 | 23 | recnd 11188 |
. . . . . 6
โข (๐ โ โค โ (2
ยท (โโ((๐
+ 1) / 2))) โ โ) |
25 | 24, 15, 15 | addassd 11182 |
. . . . 5
โข (๐ โ โค โ (((2
ยท (โโ((๐
+ 1) / 2))) + 1) + 1) = ((2 ยท (โโ((๐ + 1) / 2))) + (1 + 1))) |
26 | 17, 20, 25 | 3eqtr4d 2783 |
. . . 4
โข (๐ โ โค โ (2
ยท ((โโ((๐ + 1) / 2)) + 1)) = (((2 ยท
(โโ((๐ + 1) /
2))) + 1) + 1)) |
27 | 14, 26 | breqtrd 5132 |
. . 3
โข (๐ โ โค โ (๐ + 1) < (((2 ยท
(โโ((๐ + 1) /
2))) + 1) + 1)) |
28 | 23, 9 | readdcld 11189 |
. . . 4
โข (๐ โ โค โ ((2
ยท (โโ((๐
+ 1) / 2))) + 1) โ โ) |
29 | 1, 28, 9 | ltadd1d 11753 |
. . 3
โข (๐ โ โค โ (๐ < ((2 ยท
(โโ((๐ + 1) /
2))) + 1) โ (๐ + 1)
< (((2 ยท (โโ((๐ + 1) / 2))) + 1) + 1))) |
30 | 27, 29 | mpbird 257 |
. 2
โข (๐ โ โค โ ๐ < ((2 ยท
(โโ((๐ + 1) /
2))) + 1)) |
31 | | 2z 12540 |
. . . . 5
โข 2 โ
โค |
32 | 31 | a1i 11 |
. . . 4
โข (๐ โ โค โ 2 โ
โค) |
33 | 32, 7 | zmulcld 12618 |
. . 3
โข (๐ โ โค โ (2
ยท (โโ((๐
+ 1) / 2))) โ โค) |
34 | | zleltp1 12559 |
. . 3
โข ((๐ โ โค โง (2
ยท (โโ((๐
+ 1) / 2))) โ โค) โ (๐ โค (2 ยท (โโ((๐ + 1) / 2))) โ ๐ < ((2 ยท
(โโ((๐ + 1) /
2))) + 1))) |
35 | 33, 34 | mpdan 686 |
. 2
โข (๐ โ โค โ (๐ โค (2 ยท
(โโ((๐ + 1) /
2))) โ ๐ < ((2
ยท (โโ((๐
+ 1) / 2))) + 1))) |
36 | 30, 35 | mpbird 257 |
1
โข (๐ โ โค โ ๐ โค (2 ยท
(โโ((๐ + 1) /
2)))) |