Step | Hyp | Ref
| Expression |
1 | | eluzelz 12706 |
. . 3
โข (๐ โ
(โคโฅโ2) โ ๐ โ โค) |
2 | | zre 12437 |
. . . 4
โข (๐ โ โค โ ๐ โ
โ) |
3 | | id 22 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
4 | | 4re 12171 |
. . . . . 6
โข 4 โ
โ |
5 | 4 | a1i 11 |
. . . . 5
โข (๐ โ โ โ 4 โ
โ) |
6 | | 4ne0 12195 |
. . . . . 6
โข 4 โ
0 |
7 | 6 | a1i 11 |
. . . . 5
โข (๐ โ โ โ 4 โ
0) |
8 | 3, 5, 7 | redivcld 11917 |
. . . 4
โข (๐ โ โ โ (๐ / 4) โ
โ) |
9 | 2, 8 | syl 17 |
. . 3
โข (๐ โ โค โ (๐ / 4) โ
โ) |
10 | | flle 13633 |
. . 3
โข ((๐ / 4) โ โ โ
(โโ(๐ / 4))
โค (๐ /
4)) |
11 | 1, 9, 10 | 3syl 18 |
. 2
โข (๐ โ
(โคโฅโ2) โ (โโ(๐ / 4)) โค (๐ / 4)) |
12 | | 1red 11090 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ 1 โ โ) |
13 | | eluzelre 12707 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
14 | | rehalfcl 12313 |
. . . . 5
โข (๐ โ โ โ (๐ / 2) โ
โ) |
15 | 1, 2, 14 | 3syl 18 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ (๐ / 2) โ โ) |
16 | | 2rp 12849 |
. . . . . . 7
โข 2 โ
โ+ |
17 | 16 | a1i 11 |
. . . . . 6
โข (๐ โ
(โคโฅโ2) โ 2 โ
โ+) |
18 | | eluzle 12709 |
. . . . . 6
โข (๐ โ
(โคโฅโ2) โ 2 โค ๐) |
19 | | divge1 12912 |
. . . . . 6
โข ((2
โ โ+ โง ๐ โ โ โง 2 โค ๐) โ 1 โค (๐ / 2)) |
20 | 17, 13, 18, 19 | syl3anc 1372 |
. . . . 5
โข (๐ โ
(โคโฅโ2) โ 1 โค (๐ / 2)) |
21 | | eluzelcn 12708 |
. . . . . 6
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
22 | | subhalfhalf 12321 |
. . . . . 6
โข (๐ โ โ โ (๐ โ (๐ / 2)) = (๐ / 2)) |
23 | 21, 22 | syl 17 |
. . . . 5
โข (๐ โ
(โคโฅโ2) โ (๐ โ (๐ / 2)) = (๐ / 2)) |
24 | 20, 23 | breqtrrd 5132 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ 1 โค (๐ โ (๐ / 2))) |
25 | 12, 13, 15, 24 | lesubd 11693 |
. . 3
โข (๐ โ
(โคโฅโ2) โ (๐ / 2) โค (๐ โ 1)) |
26 | | 2t2e4 12251 |
. . . . . . . . 9
โข (2
ยท 2) = 4 |
27 | 26 | eqcomi 2747 |
. . . . . . . 8
โข 4 = (2
ยท 2) |
28 | 27 | a1i 11 |
. . . . . . 7
โข (๐ โ
(โคโฅโ2) โ 4 = (2 ยท 2)) |
29 | 28 | oveq2d 7366 |
. . . . . 6
โข (๐ โ
(โคโฅโ2) โ (๐ / 4) = (๐ / (2 ยท 2))) |
30 | | 2cnne0 12297 |
. . . . . . . 8
โข (2 โ
โ โง 2 โ 0) |
31 | 30 | a1i 11 |
. . . . . . 7
โข (๐ โ
(โคโฅโ2) โ (2 โ โ โง 2 โ
0)) |
32 | | divdiv1 11800 |
. . . . . . 7
โข ((๐ โ โ โง (2 โ
โ โง 2 โ 0) โง (2 โ โ โง 2 โ 0)) โ ((๐ / 2) / 2) = (๐ / (2 ยท 2))) |
33 | 21, 31, 31, 32 | syl3anc 1372 |
. . . . . 6
โข (๐ โ
(โคโฅโ2) โ ((๐ / 2) / 2) = (๐ / (2 ยท 2))) |
34 | 29, 33 | eqtr4d 2781 |
. . . . 5
โข (๐ โ
(โคโฅโ2) โ (๐ / 4) = ((๐ / 2) / 2)) |
35 | 34 | breq1d 5114 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ ((๐ / 4) โค ((๐ โ 1) / 2) โ ((๐ / 2) / 2) โค ((๐ โ 1) / 2))) |
36 | | peano2rem 11402 |
. . . . . 6
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
37 | 13, 36 | syl 17 |
. . . . 5
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
38 | 15, 37, 17 | lediv1d 12932 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ ((๐ / 2) โค (๐ โ 1) โ ((๐ / 2) / 2) โค ((๐ โ 1) / 2))) |
39 | 35, 38 | bitr4d 282 |
. . 3
โข (๐ โ
(โคโฅโ2) โ ((๐ / 4) โค ((๐ โ 1) / 2) โ (๐ / 2) โค (๐ โ 1))) |
40 | 25, 39 | mpbird 257 |
. 2
โข (๐ โ
(โคโฅโ2) โ (๐ / 4) โค ((๐ โ 1) / 2)) |
41 | 8 | flcld 13632 |
. . . . . 6
โข (๐ โ โ โ
(โโ(๐ / 4))
โ โค) |
42 | 41 | zred 12540 |
. . . . 5
โข (๐ โ โ โ
(โโ(๐ / 4))
โ โ) |
43 | 36 | rehalfcld 12334 |
. . . . 5
โข (๐ โ โ โ ((๐ โ 1) / 2) โ
โ) |
44 | 42, 8, 43 | 3jca 1129 |
. . . 4
โข (๐ โ โ โ
((โโ(๐ / 4))
โ โ โง (๐ /
4) โ โ โง ((๐
โ 1) / 2) โ โ)) |
45 | 1, 2, 44 | 3syl 18 |
. . 3
โข (๐ โ
(โคโฅโ2) โ ((โโ(๐ / 4)) โ โ โง (๐ / 4) โ โ โง
((๐ โ 1) / 2) โ
โ)) |
46 | | letr 11183 |
. . 3
โข
(((โโ(๐
/ 4)) โ โ โง (๐ / 4) โ โ โง ((๐ โ 1) / 2) โ โ)
โ (((โโ(๐
/ 4)) โค (๐ / 4) โง
(๐ / 4) โค ((๐ โ 1) / 2)) โ
(โโ(๐ / 4))
โค ((๐ โ 1) /
2))) |
47 | 45, 46 | syl 17 |
. 2
โข (๐ โ
(โคโฅโ2) โ (((โโ(๐ / 4)) โค (๐ / 4) โง (๐ / 4) โค ((๐ โ 1) / 2)) โ
(โโ(๐ / 4))
โค ((๐ โ 1) /
2))) |
48 | 11, 40, 47 | mp2and 698 |
1
โข (๐ โ
(โคโฅโ2) โ (โโ(๐ / 4)) โค ((๐ โ 1) / 2)) |