Step | Hyp | Ref
| Expression |
1 | | eleq1 2822 |
. . . . . . . 8
โข (((2
ยท ๐) + 1) = ๐ โ (((2 ยท ๐) + 1) โ
(โคโฅโ2) โ ๐ โ
(โคโฅโ2))) |
2 | | nn0z 12529 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โค) |
3 | 2 | adantl 483 |
. . . . . . . . . 10
โข ((((2
ยท ๐) + 1) โ
(โคโฅโ2) โง ๐ โ โ0) โ ๐ โ
โค) |
4 | | eluz2 12774 |
. . . . . . . . . . . 12
โข (((2
ยท ๐) + 1) โ
(โคโฅโ2) โ (2 โ โค โง ((2 ยท
๐) + 1) โ โค
โง 2 โค ((2 ยท ๐) + 1))) |
5 | | 2re 12232 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
6 | 5 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ 2 โ โ) |
7 | | 1red 11161 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ 1 โ โ) |
8 | | 2nn0 12435 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ0 |
9 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ 2 โ โ0) |
10 | | id 22 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ ๐ โ
โ0) |
11 | 9, 10 | nn0mulcld 12483 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ (2 ยท ๐)
โ โ0) |
12 | 11 | nn0red 12479 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ (2 ยท ๐)
โ โ) |
13 | 6, 7, 12 | lesubaddd 11757 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ ((2 โ 1) โค (2 ยท ๐) โ 2 โค ((2 ยท ๐) + 1))) |
14 | | 2m1e1 12284 |
. . . . . . . . . . . . . . . . 17
โข (2
โ 1) = 1 |
15 | 14 | breq1i 5113 |
. . . . . . . . . . . . . . . 16
โข ((2
โ 1) โค (2 ยท ๐) โ 1 โค (2 ยท ๐)) |
16 | | nn0re 12427 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ ๐ โ
โ) |
17 | | 2rp 12925 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ+ |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ 2 โ โ+) |
19 | 7, 16, 18 | ledivmuld 13015 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ ((1 / 2) โค ๐
โ 1 โค (2 ยท ๐))) |
20 | | halfgt0 12374 |
. . . . . . . . . . . . . . . . . 18
โข 0 < (1
/ 2) |
21 | | 0red 11163 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ 0 โ โ) |
22 | | halfre 12372 |
. . . . . . . . . . . . . . . . . . . 20
โข (1 / 2)
โ โ |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ (1 / 2) โ โ) |
24 | | ltletr 11252 |
. . . . . . . . . . . . . . . . . . 19
โข ((0
โ โ โง (1 / 2) โ โ โง ๐ โ โ) โ ((0 < (1 / 2)
โง (1 / 2) โค ๐)
โ 0 < ๐)) |
25 | 21, 23, 16, 24 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ ((0 < (1 / 2) โง (1 / 2) โค ๐) โ 0 < ๐)) |
26 | 20, 25 | mpani 695 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ ((1 / 2) โค ๐
โ 0 < ๐)) |
27 | 19, 26 | sylbird 260 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ (1 โค (2 ยท ๐) โ 0 < ๐)) |
28 | 15, 27 | biimtrid 241 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ ((2 โ 1) โค (2 ยท ๐) โ 0 < ๐)) |
29 | 13, 28 | sylbird 260 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (2 โค ((2 ยท ๐) + 1) โ 0 < ๐)) |
30 | 29 | com12 32 |
. . . . . . . . . . . . 13
โข (2 โค
((2 ยท ๐) + 1) โ
(๐ โ
โ0 โ 0 < ๐)) |
31 | 30 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
โข ((2
โ โค โง ((2 ยท ๐) + 1) โ โค โง 2 โค ((2
ยท ๐) + 1)) โ
(๐ โ
โ0 โ 0 < ๐)) |
32 | 4, 31 | sylbi 216 |
. . . . . . . . . . 11
โข (((2
ยท ๐) + 1) โ
(โคโฅโ2) โ (๐ โ โ0 โ 0 <
๐)) |
33 | 32 | imp 408 |
. . . . . . . . . 10
โข ((((2
ยท ๐) + 1) โ
(โคโฅโ2) โง ๐ โ โ0) โ 0 <
๐) |
34 | | elnnz 12514 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ โ โค โง 0 <
๐)) |
35 | 3, 33, 34 | sylanbrc 584 |
. . . . . . . . 9
โข ((((2
ยท ๐) + 1) โ
(โคโฅโ2) โง ๐ โ โ0) โ ๐ โ
โ) |
36 | 35 | ex 414 |
. . . . . . . 8
โข (((2
ยท ๐) + 1) โ
(โคโฅโ2) โ (๐ โ โ0 โ ๐ โ
โ)) |
37 | 1, 36 | syl6bir 254 |
. . . . . . 7
โข (((2
ยท ๐) + 1) = ๐ โ (๐ โ (โคโฅโ2)
โ (๐ โ
โ0 โ ๐ โ โ))) |
38 | 37 | com13 88 |
. . . . . 6
โข (๐ โ โ0
โ (๐ โ
(โคโฅโ2) โ (((2 ยท ๐) + 1) = ๐ โ ๐ โ โ))) |
39 | 38 | impcom 409 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (((2
ยท ๐) + 1) = ๐ โ ๐ โ โ)) |
40 | 39 | pm4.71rd 564 |
. . . 4
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (((2
ยท ๐) + 1) = ๐ โ (๐ โ โ โง ((2 ยท ๐) + 1) = ๐))) |
41 | 40 | bicomd 222 |
. . 3
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ ((๐ โ โ โง ((2
ยท ๐) + 1) = ๐) โ ((2 ยท ๐) + 1) = ๐)) |
42 | 41 | rexbidva 3170 |
. 2
โข (๐ โ
(โคโฅโ2) โ (โ๐ โ โ0 (๐ โ โ โง ((2
ยท ๐) + 1) = ๐) โ โ๐ โ โ0 ((2
ยท ๐) + 1) = ๐)) |
43 | | nnssnn0 12421 |
. . 3
โข โ
โ โ0 |
44 | | rexss 4016 |
. . 3
โข (โ
โ โ0 โ (โ๐ โ โ ((2 ยท ๐) + 1) = ๐ โ โ๐ โ โ0 (๐ โ โ โง ((2
ยท ๐) + 1) = ๐))) |
45 | 43, 44 | mp1i 13 |
. 2
โข (๐ โ
(โคโฅโ2) โ (โ๐ โ โ ((2 ยท ๐) + 1) = ๐ โ โ๐ โ โ0 (๐ โ โ โง ((2
ยท ๐) + 1) = ๐))) |
46 | | eluzge2nn0 12817 |
. . 3
โข (๐ โ
(โคโฅโ2) โ ๐ โ
โ0) |
47 | | oddnn02np1 16235 |
. . 3
โข (๐ โ โ0
โ (ยฌ 2 โฅ ๐
โ โ๐ โ
โ0 ((2 ยท ๐) + 1) = ๐)) |
48 | 46, 47 | syl 17 |
. 2
โข (๐ โ
(โคโฅโ2) โ (ยฌ 2 โฅ ๐ โ โ๐ โ โ0 ((2 ยท
๐) + 1) = ๐)) |
49 | 42, 45, 48 | 3bitr4rd 312 |
1
โข (๐ โ
(โคโฅโ2) โ (ยฌ 2 โฅ ๐ โ โ๐ โ โ ((2 ยท ๐) + 1) = ๐)) |