Step | Hyp | Ref
| Expression |
1 | | peano2z 9289 |
. . . . . . 7
โข (๐ โ โค โ (๐ + 1) โ
โค) |
2 | | 2nn 9080 |
. . . . . . 7
โข 2 โ
โ |
3 | | znq 9624 |
. . . . . . 7
โข (((๐ + 1) โ โค โง 2
โ โ) โ ((๐
+ 1) / 2) โ โ) |
4 | 1, 2, 3 | sylancl 413 |
. . . . . 6
โข (๐ โ โค โ ((๐ + 1) / 2) โ
โ) |
5 | | flqltp1 10279 |
. . . . . 6
โข (((๐ + 1) / 2) โ โ โ
((๐ + 1) / 2) <
((โโ((๐ + 1) /
2)) + 1)) |
6 | 4, 5 | syl 14 |
. . . . 5
โข (๐ โ โค โ ((๐ + 1) / 2) <
((โโ((๐ + 1) /
2)) + 1)) |
7 | | zre 9257 |
. . . . . . 7
โข (๐ โ โค โ ๐ โ
โ) |
8 | | peano2re 8093 |
. . . . . . 7
โข (๐ โ โ โ (๐ + 1) โ
โ) |
9 | 7, 8 | syl 14 |
. . . . . 6
โข (๐ โ โค โ (๐ + 1) โ
โ) |
10 | 4 | flqcld 10277 |
. . . . . . . 8
โข (๐ โ โค โ
(โโ((๐ + 1) /
2)) โ โค) |
11 | 10 | zred 9375 |
. . . . . . 7
โข (๐ โ โค โ
(โโ((๐ + 1) /
2)) โ โ) |
12 | | 1red 7972 |
. . . . . . 7
โข (๐ โ โค โ 1 โ
โ) |
13 | 11, 12 | readdcld 7987 |
. . . . . 6
โข (๐ โ โค โ
((โโ((๐ + 1) /
2)) + 1) โ โ) |
14 | | 2rp 9658 |
. . . . . . 7
โข 2 โ
โ+ |
15 | 14 | a1i 9 |
. . . . . 6
โข (๐ โ โค โ 2 โ
โ+) |
16 | 9, 13, 15 | ltdivmuld 9748 |
. . . . 5
โข (๐ โ โค โ (((๐ + 1) / 2) <
((โโ((๐ + 1) /
2)) + 1) โ (๐ + 1)
< (2 ยท ((โโ((๐ + 1) / 2)) + 1)))) |
17 | 6, 16 | mpbid 147 |
. . . 4
โข (๐ โ โค โ (๐ + 1) < (2 ยท
((โโ((๐ + 1) /
2)) + 1))) |
18 | 12 | recnd 7986 |
. . . . . . 7
โข (๐ โ โค โ 1 โ
โ) |
19 | 18 | 2timesd 9161 |
. . . . . 6
โข (๐ โ โค โ (2
ยท 1) = (1 + 1)) |
20 | 19 | oveq2d 5891 |
. . . . 5
โข (๐ โ โค โ ((2
ยท (โโ((๐
+ 1) / 2))) + (2 ยท 1)) = ((2 ยท (โโ((๐ + 1) / 2))) + (1 + 1))) |
21 | | 2cnd 8992 |
. . . . . 6
โข (๐ โ โค โ 2 โ
โ) |
22 | 11 | recnd 7986 |
. . . . . 6
โข (๐ โ โค โ
(โโ((๐ + 1) /
2)) โ โ) |
23 | 21, 22, 18 | adddid 7982 |
. . . . 5
โข (๐ โ โค โ (2
ยท ((โโ((๐ + 1) / 2)) + 1)) = ((2 ยท
(โโ((๐ + 1) /
2))) + (2 ยท 1))) |
24 | | 2re 8989 |
. . . . . . . . 9
โข 2 โ
โ |
25 | 24 | a1i 9 |
. . . . . . . 8
โข (๐ โ โค โ 2 โ
โ) |
26 | 25, 11 | remulcld 7988 |
. . . . . . 7
โข (๐ โ โค โ (2
ยท (โโ((๐
+ 1) / 2))) โ โ) |
27 | 26 | recnd 7986 |
. . . . . 6
โข (๐ โ โค โ (2
ยท (โโ((๐
+ 1) / 2))) โ โ) |
28 | 27, 18, 18 | addassd 7980 |
. . . . 5
โข (๐ โ โค โ (((2
ยท (โโ((๐
+ 1) / 2))) + 1) + 1) = ((2 ยท (โโ((๐ + 1) / 2))) + (1 + 1))) |
29 | 20, 23, 28 | 3eqtr4d 2220 |
. . . 4
โข (๐ โ โค โ (2
ยท ((โโ((๐ + 1) / 2)) + 1)) = (((2 ยท
(โโ((๐ + 1) /
2))) + 1) + 1)) |
30 | 17, 29 | breqtrd 4030 |
. . 3
โข (๐ โ โค โ (๐ + 1) < (((2 ยท
(โโ((๐ + 1) /
2))) + 1) + 1)) |
31 | 26, 12 | readdcld 7987 |
. . . 4
โข (๐ โ โค โ ((2
ยท (โโ((๐
+ 1) / 2))) + 1) โ โ) |
32 | 7, 31, 12 | ltadd1d 8495 |
. . 3
โข (๐ โ โค โ (๐ < ((2 ยท
(โโ((๐ + 1) /
2))) + 1) โ (๐ + 1)
< (((2 ยท (โโ((๐ + 1) / 2))) + 1) + 1))) |
33 | 30, 32 | mpbird 167 |
. 2
โข (๐ โ โค โ ๐ < ((2 ยท
(โโ((๐ + 1) /
2))) + 1)) |
34 | | 2z 9281 |
. . . . 5
โข 2 โ
โค |
35 | 34 | a1i 9 |
. . . 4
โข (๐ โ โค โ 2 โ
โค) |
36 | 35, 10 | zmulcld 9381 |
. . 3
โข (๐ โ โค โ (2
ยท (โโ((๐
+ 1) / 2))) โ โค) |
37 | | zleltp1 9308 |
. . 3
โข ((๐ โ โค โง (2
ยท (โโ((๐
+ 1) / 2))) โ โค) โ (๐ โค (2 ยท (โโ((๐ + 1) / 2))) โ ๐ < ((2 ยท
(โโ((๐ + 1) /
2))) + 1))) |
38 | 36, 37 | mpdan 421 |
. 2
โข (๐ โ โค โ (๐ โค (2 ยท
(โโ((๐ + 1) /
2))) โ ๐ < ((2
ยท (โโ((๐
+ 1) / 2))) + 1))) |
39 | 33, 38 | mpbird 167 |
1
โข (๐ โ โค โ ๐ โค (2 ยท
(โโ((๐ + 1) /
2)))) |