Step | Hyp | Ref
| Expression |
1 | | bpos1.3 |
. . . . . 6
โข ๐ โ โ |
2 | | prmnn 16557 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
โข ๐ โ โ |
4 | 3 | nnzi 12534 |
. . . 4
โข ๐ โ โค |
5 | | eluzelz 12780 |
. . . 4
โข (๐ โ
(โคโฅโ๐ด) โ ๐ โ โค) |
6 | | eluz 12784 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ
(โคโฅโ๐) โ ๐ โค ๐)) |
7 | 4, 5, 6 | sylancr 588 |
. . 3
โข (๐ โ
(โคโฅโ๐ด) โ (๐ โ (โคโฅโ๐) โ ๐ โค ๐)) |
8 | | bpos1.2 |
. . 3
โข (๐ โ
(โคโฅโ๐) โ ๐) |
9 | 7, 8 | syl6bir 254 |
. 2
โข (๐ โ
(โคโฅโ๐ด) โ (๐ โค ๐ โ ๐)) |
10 | 3 | nnrei 12169 |
. . . . . . . 8
โข ๐ โ โ |
11 | 10 | a1i 11 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐ด) โ ๐ โ โ) |
12 | | bpos1.5 |
. . . . . . . . 9
โข (๐ด ยท 2) = ๐ต |
13 | | bpos1.4 |
. . . . . . . . . . 11
โข ๐ด โ
โ0 |
14 | 13 | nn0rei 12431 |
. . . . . . . . . 10
โข ๐ด โ โ |
15 | | 2re 12234 |
. . . . . . . . . 10
โข 2 โ
โ |
16 | 14, 15 | remulcli 11178 |
. . . . . . . . 9
โข (๐ด ยท 2) โ
โ |
17 | 12, 16 | eqeltrri 2835 |
. . . . . . . 8
โข ๐ต โ โ |
18 | 17 | a1i 11 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐ด) โ ๐ต โ โ) |
19 | | eluzelre 12781 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ๐ด) โ ๐ โ โ) |
20 | | remulcl 11143 |
. . . . . . . 8
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
21 | 15, 19, 20 | sylancr 588 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐ด) โ (2 ยท ๐) โ โ) |
22 | | bpos1.7 |
. . . . . . . . 9
โข (๐ < ๐ต โจ ๐ = ๐ต) |
23 | 10, 17 | leloei 11279 |
. . . . . . . . 9
โข (๐ โค ๐ต โ (๐ < ๐ต โจ ๐ = ๐ต)) |
24 | 22, 23 | mpbir 230 |
. . . . . . . 8
โข ๐ โค ๐ต |
25 | 24 | a1i 11 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐ด) โ ๐ โค ๐ต) |
26 | 13 | nn0cni 12432 |
. . . . . . . . 9
โข ๐ด โ โ |
27 | | 2cn 12235 |
. . . . . . . . 9
โข 2 โ
โ |
28 | 26, 27, 12 | mulcomli 11171 |
. . . . . . . 8
โข (2
ยท ๐ด) = ๐ต |
29 | | eluzle 12783 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ๐ด) โ ๐ด โค ๐) |
30 | | 2pos 12263 |
. . . . . . . . . . . 12
โข 0 <
2 |
31 | 15, 30 | pm3.2i 472 |
. . . . . . . . . . 11
โข (2 โ
โ โง 0 < 2) |
32 | | lemul2 12015 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ โง (2 โ
โ โง 0 < 2)) โ (๐ด โค ๐ โ (2 ยท ๐ด) โค (2 ยท ๐))) |
33 | 14, 31, 32 | mp3an13 1453 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ด โค ๐ โ (2 ยท ๐ด) โค (2 ยท ๐))) |
34 | 19, 33 | syl 17 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ๐ด) โ (๐ด โค ๐ โ (2 ยท ๐ด) โค (2 ยท ๐))) |
35 | 29, 34 | mpbid 231 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ๐ด) โ (2 ยท ๐ด) โค (2 ยท ๐)) |
36 | 28, 35 | eqbrtrrid 5146 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐ด) โ ๐ต โค (2 ยท ๐)) |
37 | 11, 18, 21, 25, 36 | letrd 11319 |
. . . . . 6
โข (๐ โ
(โคโฅโ๐ด) โ ๐ โค (2 ยท ๐)) |
38 | 37 | anim2i 618 |
. . . . 5
โข ((๐ < ๐ โง ๐ โ (โคโฅโ๐ด)) โ (๐ < ๐ โง ๐ โค (2 ยท ๐))) |
39 | | breq2 5114 |
. . . . . . 7
โข (๐ = ๐ โ (๐ < ๐ โ ๐ < ๐)) |
40 | | breq1 5113 |
. . . . . . 7
โข (๐ = ๐ โ (๐ โค (2 ยท ๐) โ ๐ โค (2 ยท ๐))) |
41 | 39, 40 | anbi12d 632 |
. . . . . 6
โข (๐ = ๐ โ ((๐ < ๐ โง ๐ โค (2 ยท ๐)) โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
42 | 41 | rspcev 3584 |
. . . . 5
โข ((๐ โ โ โง (๐ < ๐ โง ๐ โค (2 ยท ๐))) โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐))) |
43 | 1, 38, 42 | sylancr 588 |
. . . 4
โข ((๐ < ๐ โง ๐ โ (โคโฅโ๐ด)) โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐))) |
44 | | bpos1.1 |
. . . 4
โข
(โ๐ โ
โ (๐ < ๐ โง ๐ โค (2 ยท ๐)) โ ๐) |
45 | 43, 44 | syl 17 |
. . 3
โข ((๐ < ๐ โง ๐ โ (โคโฅโ๐ด)) โ ๐) |
46 | 45 | expcom 415 |
. 2
โข (๐ โ
(โคโฅโ๐ด) โ (๐ < ๐ โ ๐)) |
47 | | lelttric 11269 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โค ๐ โจ ๐ < ๐)) |
48 | 10, 19, 47 | sylancr 588 |
. 2
โข (๐ โ
(โคโฅโ๐ด) โ (๐ โค ๐ โจ ๐ < ๐)) |
49 | 9, 46, 48 | mpjaod 859 |
1
โข (๐ โ
(โคโฅโ๐ด) โ ๐) |