Step | Hyp | Ref
| Expression |
1 | | prmnn 16551 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ) |
2 | | nnnn0 12421 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ0) |
3 | | oddnn02np1 16231 |
. . . 4
โข (๐ โ โ0
โ (ยฌ 2 โฅ ๐
โ โ๐ โ
โ0 ((2 ยท ๐) + 1) = ๐)) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
โข (๐ โ โ โ (ยฌ 2
โฅ ๐ โ
โ๐ โ
โ0 ((2 ยท ๐) + 1) = ๐)) |
5 | | iftrue 4493 |
. . . . . . . . 9
โข (2
โฅ ๐ โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (๐ / 2)) |
6 | 5 | adantr 482 |
. . . . . . . 8
โข ((2
โฅ ๐ โง ๐ โ โ0)
โ if(2 โฅ ๐,
(๐ / 2), ((๐ โ 1) / 2)) = (๐ / 2)) |
7 | | 2nn 12227 |
. . . . . . . . . 10
โข 2 โ
โ |
8 | | nn0ledivnn 13029 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง 2 โ โ) โ (๐ / 2) โค ๐) |
9 | 7, 8 | mpan2 690 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ / 2) โค ๐) |
10 | 9 | adantl 483 |
. . . . . . . 8
โข ((2
โฅ ๐ โง ๐ โ โ0)
โ (๐ / 2) โค ๐) |
11 | 6, 10 | eqbrtrd 5128 |
. . . . . . 7
โข ((2
โฅ ๐ โง ๐ โ โ0)
โ if(2 โฅ ๐,
(๐ / 2), ((๐ โ 1) / 2)) โค ๐) |
12 | | iffalse 4496 |
. . . . . . . . 9
โข (ยฌ 2
โฅ ๐ โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = ((๐ โ 1) / 2)) |
13 | 12 | adantr 482 |
. . . . . . . 8
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โ0)
โ if(2 โฅ ๐,
(๐ / 2), ((๐ โ 1) / 2)) = ((๐ โ 1) /
2)) |
14 | | nn0re 12423 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โ) |
15 | | peano2rem 11469 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
16 | 15 | rehalfcld 12401 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((๐ โ 1) / 2) โ
โ) |
17 | 14, 16 | syl 17 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((๐ โ 1) / 2)
โ โ) |
18 | 14 | rehalfcld 12401 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ / 2) โ
โ) |
19 | 14 | lem1d 12089 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (๐ โ 1) โค
๐) |
20 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (๐ โ 1) โ
โ) |
21 | | 2re 12228 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
22 | | 2pos 12257 |
. . . . . . . . . . . . . 14
โข 0 <
2 |
23 | 21, 22 | pm3.2i 472 |
. . . . . . . . . . . . 13
โข (2 โ
โ โง 0 < 2) |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (2 โ โ โง 0 < 2)) |
25 | | lediv1 12021 |
. . . . . . . . . . . 12
โข (((๐ โ 1) โ โ โง
๐ โ โ โง (2
โ โ โง 0 < 2)) โ ((๐ โ 1) โค ๐ โ ((๐ โ 1) / 2) โค (๐ / 2))) |
26 | 20, 14, 24, 25 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ((๐ โ 1) โค
๐ โ ((๐ โ 1) / 2) โค (๐ / 2))) |
27 | 19, 26 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((๐ โ 1) / 2)
โค (๐ /
2)) |
28 | 17, 18, 14, 27, 9 | letrd 11313 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((๐ โ 1) / 2)
โค ๐) |
29 | 28 | adantl 483 |
. . . . . . . 8
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โ0)
โ ((๐ โ 1) / 2)
โค ๐) |
30 | 13, 29 | eqbrtrd 5128 |
. . . . . . 7
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โ0)
โ if(2 โฅ ๐,
(๐ / 2), ((๐ โ 1) / 2)) โค ๐) |
31 | 11, 30 | pm2.61ian 811 |
. . . . . 6
โข (๐ โ โ0
โ if(2 โฅ ๐,
(๐ / 2), ((๐ โ 1) / 2)) โค ๐) |
32 | 31 | ad2antlr 726 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ0)
โง ((2 ยท ๐) + 1)
= ๐) โ if(2 โฅ
๐, (๐ / 2), ((๐ โ 1) / 2)) โค ๐) |
33 | | nn0z 12525 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โค) |
34 | 33 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โค) |
35 | | eqcom 2744 |
. . . . . . 7
โข (((2
ยท ๐) + 1) = ๐ โ ๐ = ((2 ยท ๐) + 1)) |
36 | 35 | biimpi 215 |
. . . . . 6
โข (((2
ยท ๐) + 1) = ๐ โ ๐ = ((2 ยท ๐) + 1)) |
37 | | flodddiv4 16296 |
. . . . . 6
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ
(โโ(๐ / 4)) =
if(2 โฅ ๐, (๐ / 2), ((๐ โ 1) / 2))) |
38 | 34, 36, 37 | syl2an 597 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ0)
โง ((2 ยท ๐) + 1)
= ๐) โ
(โโ(๐ / 4)) =
if(2 โฅ ๐, (๐ / 2), ((๐ โ 1) / 2))) |
39 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ((2 ยท ๐) + 1) โ (๐ โ 1) = (((2 ยท ๐) + 1) โ
1)) |
40 | 39 | eqcoms 2745 |
. . . . . . . . 9
โข (((2
ยท ๐) + 1) = ๐ โ (๐ โ 1) = (((2 ยท ๐) + 1) โ
1)) |
41 | 40 | adantl 483 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ0)
โง ((2 ยท ๐) + 1)
= ๐) โ (๐ โ 1) = (((2 ยท
๐) + 1) โ
1)) |
42 | | 2nn0 12431 |
. . . . . . . . . . . . 13
โข 2 โ
โ0 |
43 | 42 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ 2 โ โ0) |
44 | | id 22 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โ0) |
45 | 43, 44 | nn0mulcld 12479 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (2 ยท ๐)
โ โ0) |
46 | 45 | nn0cnd 12476 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (2 ยท ๐)
โ โ) |
47 | | pncan1 11580 |
. . . . . . . . . 10
โข ((2
ยท ๐) โ โ
โ (((2 ยท ๐) +
1) โ 1) = (2 ยท ๐)) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) โ 1) = (2 ยท ๐)) |
49 | 48 | ad2antlr 726 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ0)
โง ((2 ยท ๐) + 1)
= ๐) โ (((2 ยท
๐) + 1) โ 1) = (2
ยท ๐)) |
50 | 41, 49 | eqtrd 2777 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ0)
โง ((2 ยท ๐) + 1)
= ๐) โ (๐ โ 1) = (2 ยท ๐)) |
51 | 50 | oveq1d 7373 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ0)
โง ((2 ยท ๐) + 1)
= ๐) โ ((๐ โ 1) / 2) = ((2 ยท
๐) / 2)) |
52 | | nn0cn 12424 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
53 | | 2cnd 12232 |
. . . . . . . 8
โข (๐ โ โ0
โ 2 โ โ) |
54 | | 2ne0 12258 |
. . . . . . . . 9
โข 2 โ
0 |
55 | 54 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ0
โ 2 โ 0) |
56 | 52, 53, 55 | divcan3d 11937 |
. . . . . . 7
โข (๐ โ โ0
โ ((2 ยท ๐) / 2)
= ๐) |
57 | 56 | ad2antlr 726 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ0)
โง ((2 ยท ๐) + 1)
= ๐) โ ((2 ยท
๐) / 2) = ๐) |
58 | 51, 57 | eqtrd 2777 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ0)
โง ((2 ยท ๐) + 1)
= ๐) โ ((๐ โ 1) / 2) = ๐) |
59 | 32, 38, 58 | 3brtr4d 5138 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ0)
โง ((2 ยท ๐) + 1)
= ๐) โ
(โโ(๐ / 4))
โค ((๐ โ 1) /
2)) |
60 | 59 | rexlimdva2 3155 |
. . 3
โข (๐ โ โ โ
(โ๐ โ
โ0 ((2 ยท ๐) + 1) = ๐ โ (โโ(๐ / 4)) โค ((๐ โ 1) / 2))) |
61 | 4, 60 | sylbid 239 |
. 2
โข (๐ โ โ โ (ยฌ 2
โฅ ๐ โ
(โโ(๐ / 4))
โค ((๐ โ 1) /
2))) |
62 | 61 | imp 408 |
1
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(โโ(๐ / 4))
โค ((๐ โ 1) /
2)) |