Step | Hyp | Ref
| Expression |
1 | | zre 12504 |
. . . . 5
โข (๐ โ โค โ ๐ โ
โ) |
2 | 1 | rehalfcld 12401 |
. . . 4
โข (๐ โ โค โ (๐ / 2) โ
โ) |
3 | 2 | adantr 482 |
. . 3
โข ((๐ โ โค โง ๐ผ โ โค) โ (๐ / 2) โ
โ) |
4 | | id 22 |
. . . . . 6
โข (๐ผ โ โค โ ๐ผ โ
โค) |
5 | | 2z 12536 |
. . . . . . 7
โข 2 โ
โค |
6 | 5 | a1i 11 |
. . . . . 6
โข (๐ผ โ โค โ 2 โ
โค) |
7 | 4, 6 | zmulcld 12614 |
. . . . 5
โข (๐ผ โ โค โ (๐ผ ยท 2) โ
โค) |
8 | 7 | zred 12608 |
. . . 4
โข (๐ผ โ โค โ (๐ผ ยท 2) โ
โ) |
9 | 8 | adantl 483 |
. . 3
โข ((๐ โ โค โง ๐ผ โ โค) โ (๐ผ ยท 2) โ
โ) |
10 | | 2re 12228 |
. . . . 5
โข 2 โ
โ |
11 | | 2pos 12257 |
. . . . 5
โข 0 <
2 |
12 | 10, 11 | pm3.2i 472 |
. . . 4
โข (2 โ
โ โง 0 < 2) |
13 | 12 | a1i 11 |
. . 3
โข ((๐ โ โค โง ๐ผ โ โค) โ (2
โ โ โง 0 < 2)) |
14 | | ltdiv1 12020 |
. . 3
โข (((๐ / 2) โ โ โง
(๐ผ ยท 2) โ
โ โง (2 โ โ โง 0 < 2)) โ ((๐ / 2) < (๐ผ ยท 2) โ ((๐ / 2) / 2) < ((๐ผ ยท 2) / 2))) |
15 | 3, 9, 13, 14 | syl3anc 1372 |
. 2
โข ((๐ โ โค โง ๐ผ โ โค) โ ((๐ / 2) < (๐ผ ยท 2) โ ((๐ / 2) / 2) < ((๐ผ ยท 2) / 2))) |
16 | | zcn 12505 |
. . . . . 6
โข (๐ โ โค โ ๐ โ
โ) |
17 | 16 | adantr 482 |
. . . . 5
โข ((๐ โ โค โง ๐ผ โ โค) โ ๐ โ
โ) |
18 | | 2cnne0 12364 |
. . . . . 6
โข (2 โ
โ โง 2 โ 0) |
19 | 18 | a1i 11 |
. . . . 5
โข ((๐ โ โค โง ๐ผ โ โค) โ (2
โ โ โง 2 โ 0)) |
20 | | divdiv1 11867 |
. . . . 5
โข ((๐ โ โ โง (2 โ
โ โง 2 โ 0) โง (2 โ โ โง 2 โ 0)) โ ((๐ / 2) / 2) = (๐ / (2 ยท 2))) |
21 | 17, 19, 19, 20 | syl3anc 1372 |
. . . 4
โข ((๐ โ โค โง ๐ผ โ โค) โ ((๐ / 2) / 2) = (๐ / (2 ยท 2))) |
22 | | 2t2e4 12318 |
. . . . 5
โข (2
ยท 2) = 4 |
23 | 22 | oveq2i 7369 |
. . . 4
โข (๐ / (2 ยท 2)) = (๐ / 4) |
24 | 21, 23 | eqtrdi 2793 |
. . 3
โข ((๐ โ โค โง ๐ผ โ โค) โ ((๐ / 2) / 2) = (๐ / 4)) |
25 | | zcn 12505 |
. . . . 5
โข (๐ผ โ โค โ ๐ผ โ
โ) |
26 | 25 | adantl 483 |
. . . 4
โข ((๐ โ โค โง ๐ผ โ โค) โ ๐ผ โ
โ) |
27 | | 2cnd 12232 |
. . . 4
โข ((๐ โ โค โง ๐ผ โ โค) โ 2 โ
โ) |
28 | | 2ne0 12258 |
. . . . 5
โข 2 โ
0 |
29 | 28 | a1i 11 |
. . . 4
โข ((๐ โ โค โง ๐ผ โ โค) โ 2 โ
0) |
30 | 26, 27, 29 | divcan4d 11938 |
. . 3
โข ((๐ โ โค โง ๐ผ โ โค) โ ((๐ผ ยท 2) / 2) = ๐ผ) |
31 | 24, 30 | breq12d 5119 |
. 2
โข ((๐ โ โค โง ๐ผ โ โค) โ (((๐ / 2) / 2) < ((๐ผ ยท 2) / 2) โ (๐ / 4) < ๐ผ)) |
32 | | 4re 12238 |
. . . . 5
โข 4 โ
โ |
33 | 32 | a1i 11 |
. . . 4
โข (๐ โ โค โ 4 โ
โ) |
34 | | 4ne0 12262 |
. . . . 5
โข 4 โ
0 |
35 | 34 | a1i 11 |
. . . 4
โข (๐ โ โค โ 4 โ
0) |
36 | 1, 33, 35 | redivcld 11984 |
. . 3
โข (๐ โ โค โ (๐ / 4) โ
โ) |
37 | | fllt 13712 |
. . 3
โข (((๐ / 4) โ โ โง ๐ผ โ โค) โ ((๐ / 4) < ๐ผ โ (โโ(๐ / 4)) < ๐ผ)) |
38 | 36, 37 | sylan 581 |
. 2
โข ((๐ โ โค โง ๐ผ โ โค) โ ((๐ / 4) < ๐ผ โ (โโ(๐ / 4)) < ๐ผ)) |
39 | 15, 31, 38 | 3bitrrd 306 |
1
โข ((๐ โ โค โง ๐ผ โ โค) โ
((โโ(๐ / 4))
< ๐ผ โ (๐ / 2) < (๐ผ ยท 2))) |