Step | Hyp | Ref
| Expression |
1 | | 2nn0 12437 |
. . . 4
โข 2 โ
โ0 |
2 | | simpll 766 |
. . . 4
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐ โ
(โคโฅโ๐พ)) โ ๐ โ
โ0) |
3 | | nn0mulcl 12456 |
. . . 4
โข ((2
โ โ0 โง ๐ โ โ0) โ (2
ยท ๐) โ
โ0) |
4 | 1, 2, 3 | sylancr 588 |
. . 3
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐ โ
(โคโฅโ๐พ)) โ (2 ยท ๐) โ
โ0) |
5 | | simpr 486 |
. . 3
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐ โ
(โคโฅโ๐พ)) โ ๐ โ (โคโฅโ๐พ)) |
6 | | nn0re 12429 |
. . . . . 6
โข (๐ โ โ0
โ ๐ โ
โ) |
7 | 6 | leidd 11728 |
. . . . 5
โข (๐ โ โ0
โ ๐ โค ๐) |
8 | | nn0cn 12430 |
. . . . . 6
โข (๐ โ โ0
โ ๐ โ
โ) |
9 | | 2cn 12235 |
. . . . . . 7
โข 2 โ
โ |
10 | | 2ne0 12264 |
. . . . . . 7
โข 2 โ
0 |
11 | | divcan3 11846 |
. . . . . . 7
โข ((๐ โ โ โง 2 โ
โ โง 2 โ 0) โ ((2 ยท ๐) / 2) = ๐) |
12 | 9, 10, 11 | mp3an23 1454 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท ๐) / 2) = ๐) |
13 | 8, 12 | syl 17 |
. . . . 5
โข (๐ โ โ0
โ ((2 ยท ๐) / 2)
= ๐) |
14 | 7, 13 | breqtrrd 5138 |
. . . 4
โข (๐ โ โ0
โ ๐ โค ((2 ยท
๐) / 2)) |
15 | 2, 14 | syl 17 |
. . 3
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐ โ
(โคโฅโ๐พ)) โ ๐ โค ((2 ยท ๐) / 2)) |
16 | | bcmono 26641 |
. . 3
โข (((2
ยท ๐) โ
โ0 โง ๐
โ (โคโฅโ๐พ) โง ๐ โค ((2 ยท ๐) / 2)) โ ((2 ยท ๐)C๐พ) โค ((2 ยท ๐)C๐)) |
17 | 4, 5, 15, 16 | syl3anc 1372 |
. 2
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐ โ
(โคโฅโ๐พ)) โ ((2 ยท ๐)C๐พ) โค ((2 ยท ๐)C๐)) |
18 | | simpll 766 |
. . . . 5
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ๐ โ
โ0) |
19 | 1, 18, 3 | sylancr 588 |
. . . 4
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ (2 ยท ๐) โ
โ0) |
20 | | simplr 768 |
. . . 4
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ๐พ โ โค) |
21 | | bccmpl 14216 |
. . . 4
โข (((2
ยท ๐) โ
โ0 โง ๐พ
โ โค) โ ((2 ยท ๐)C๐พ) = ((2 ยท ๐)C((2 ยท ๐) โ ๐พ))) |
22 | 19, 20, 21 | syl2anc 585 |
. . 3
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ((2 ยท ๐)C๐พ) = ((2 ยท ๐)C((2 ยท ๐) โ ๐พ))) |
23 | 18 | nn0red 12481 |
. . . . . . . . 9
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ๐ โ โ) |
24 | 23 | recnd 11190 |
. . . . . . . 8
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ๐ โ โ) |
25 | 24 | 2timesd 12403 |
. . . . . . 7
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ (2 ยท ๐) = (๐ + ๐)) |
26 | 20 | zred 12614 |
. . . . . . . 8
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ๐พ โ โ) |
27 | | eluzle 12783 |
. . . . . . . . 9
โข (๐พ โ
(โคโฅโ๐) โ ๐ โค ๐พ) |
28 | 27 | adantl 483 |
. . . . . . . 8
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ๐ โค ๐พ) |
29 | 23, 26, 23, 28 | leadd2dd 11777 |
. . . . . . 7
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ (๐ + ๐) โค (๐ + ๐พ)) |
30 | 25, 29 | eqbrtrd 5132 |
. . . . . 6
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ (2 ยท ๐) โค (๐ + ๐พ)) |
31 | 19 | nn0red 12481 |
. . . . . . 7
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ (2 ยท ๐) โ โ) |
32 | 31, 26, 23 | lesubaddd 11759 |
. . . . . 6
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ (((2 ยท ๐) โ ๐พ) โค ๐ โ (2 ยท ๐) โค (๐ + ๐พ))) |
33 | 30, 32 | mpbird 257 |
. . . . 5
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ((2 ยท ๐) โ ๐พ) โค ๐) |
34 | 19 | nn0zd 12532 |
. . . . . . 7
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ (2 ยท ๐) โ โค) |
35 | 34, 20 | zsubcld 12619 |
. . . . . 6
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ((2 ยท ๐) โ ๐พ) โ โค) |
36 | 18 | nn0zd 12532 |
. . . . . 6
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ๐ โ โค) |
37 | | eluz 12784 |
. . . . . 6
โข ((((2
ยท ๐) โ ๐พ) โ โค โง ๐ โ โค) โ (๐ โ
(โคโฅโ((2 ยท ๐) โ ๐พ)) โ ((2 ยท ๐) โ ๐พ) โค ๐)) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . 5
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ (๐ โ (โคโฅโ((2
ยท ๐) โ ๐พ)) โ ((2 ยท ๐) โ ๐พ) โค ๐)) |
39 | 33, 38 | mpbird 257 |
. . . 4
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ๐ โ (โคโฅโ((2
ยท ๐) โ ๐พ))) |
40 | 18, 14 | syl 17 |
. . . 4
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ๐ โค ((2 ยท ๐) / 2)) |
41 | | bcmono 26641 |
. . . 4
โข (((2
ยท ๐) โ
โ0 โง ๐
โ (โคโฅโ((2 ยท ๐) โ ๐พ)) โง ๐ โค ((2 ยท ๐) / 2)) โ ((2 ยท ๐)C((2 ยท ๐) โ ๐พ)) โค ((2 ยท ๐)C๐)) |
42 | 19, 39, 40, 41 | syl3anc 1372 |
. . 3
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ((2 ยท ๐)C((2 ยท ๐) โ ๐พ)) โค ((2 ยท ๐)C๐)) |
43 | 22, 42 | eqbrtrd 5132 |
. 2
โข (((๐ โ โ0
โง ๐พ โ โค)
โง ๐พ โ
(โคโฅโ๐)) โ ((2 ยท ๐)C๐พ) โค ((2 ยท ๐)C๐)) |
44 | | simpr 486 |
. . 3
โข ((๐ โ โ0
โง ๐พ โ โค)
โ ๐พ โ
โค) |
45 | | nn0z 12531 |
. . . 4
โข (๐ โ โ0
โ ๐ โ
โค) |
46 | 45 | adantr 482 |
. . 3
โข ((๐ โ โ0
โง ๐พ โ โค)
โ ๐ โ
โค) |
47 | | uztric 12794 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค) โ (๐ โ
(โคโฅโ๐พ) โจ ๐พ โ (โคโฅโ๐))) |
48 | 44, 46, 47 | syl2anc 585 |
. 2
โข ((๐ โ โ0
โง ๐พ โ โค)
โ (๐ โ
(โคโฅโ๐พ) โจ ๐พ โ (โคโฅโ๐))) |
49 | 17, 43, 48 | mpjaodan 958 |
1
โข ((๐ โ โ0
โง ๐พ โ โค)
โ ((2 ยท ๐)C๐พ) โค ((2 ยท ๐)C๐)) |