Step | Hyp | Ref
| Expression |
1 | | odd2np1 16158 |
. . 3
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
2 | | 0xr 11136 |
. . . . . . . . . . . 12
โข 0 โ
โ* |
3 | | 1xr 11148 |
. . . . . . . . . . . 12
โข 1 โ
โ* |
4 | | halfre 12301 |
. . . . . . . . . . . . 13
โข (1 / 2)
โ โ |
5 | 4 | rexri 11147 |
. . . . . . . . . . . 12
โข (1 / 2)
โ โ* |
6 | 2, 3, 5 | 3pm3.2i 1340 |
. . . . . . . . . . 11
โข (0 โ
โ* โง 1 โ โ* โง (1 / 2) โ
โ*) |
7 | | halfgt0 12303 |
. . . . . . . . . . . 12
โข 0 < (1
/ 2) |
8 | | halflt1 12305 |
. . . . . . . . . . . 12
โข (1 / 2)
< 1 |
9 | 7, 8 | pm3.2i 472 |
. . . . . . . . . . 11
โข (0 <
(1 / 2) โง (1 / 2) < 1) |
10 | | elioo3g 13222 |
. . . . . . . . . . 11
โข ((1 / 2)
โ (0(,)1) โ ((0 โ โ* โง 1 โ
โ* โง (1 / 2) โ โ*) โง (0 < (1
/ 2) โง (1 / 2) < 1))) |
11 | 6, 9, 10 | mpbir2an 710 |
. . . . . . . . . 10
โข (1 / 2)
โ (0(,)1) |
12 | | zltaddlt1le 13351 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง (1 / 2)
โ (0(,)1)) โ ((๐
+ (1 / 2)) < ๐ โ
(๐ + (1 / 2)) โค ๐)) |
13 | 11, 12 | mp3an3 1451 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ + (1 / 2)) < ๐ โ (๐ + (1 / 2)) โค ๐)) |
14 | | zcn 12438 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
15 | 14 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
16 | | 1cnd 11084 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ 1 โ
โ) |
17 | | 2cnne0 12297 |
. . . . . . . . . . . 12
โข (2 โ
โ โง 2 โ 0) |
18 | 17 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (2
โ โ โง 2 โ 0)) |
19 | | muldivdir 11782 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 1 โ
โ โง (2 โ โ โง 2 โ 0)) โ (((2 ยท ๐) + 1) / 2) = (๐ + (1 / 2))) |
20 | 15, 16, 18, 19 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) / 2) =
(๐ + (1 /
2))) |
21 | 20 | breq1d 5114 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ ((((2
ยท ๐) + 1) / 2) <
๐ โ (๐ + (1 / 2)) < ๐)) |
22 | 20 | breq1d 5114 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ ((((2
ยท ๐) + 1) / 2) โค
๐ โ (๐ + (1 / 2)) โค ๐)) |
23 | 13, 21, 22 | 3bitr4rd 312 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ ((((2
ยท ๐) + 1) / 2) โค
๐ โ (((2 ยท
๐) + 1) / 2) < ๐)) |
24 | | oveq1 7357 |
. . . . . . . . . 10
โข (((2
ยท ๐) + 1) = ๐ โ (((2 ยท ๐) + 1) / 2) = (๐ / 2)) |
25 | 24 | breq1d 5114 |
. . . . . . . . 9
โข (((2
ยท ๐) + 1) = ๐ โ ((((2 ยท ๐) + 1) / 2) โค ๐ โ (๐ / 2) โค ๐)) |
26 | 24 | breq1d 5114 |
. . . . . . . . 9
โข (((2
ยท ๐) + 1) = ๐ โ ((((2 ยท ๐) + 1) / 2) < ๐ โ (๐ / 2) < ๐)) |
27 | 25, 26 | bibi12d 346 |
. . . . . . . 8
โข (((2
ยท ๐) + 1) = ๐ โ (((((2 ยท ๐) + 1) / 2) โค ๐ โ (((2 ยท ๐) + 1) / 2) < ๐) โ ((๐ / 2) โค ๐ โ (๐ / 2) < ๐))) |
28 | 23, 27 | syl5ibcom 245 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) = ๐ โ ((๐ / 2) โค ๐ โ (๐ / 2) < ๐))) |
29 | 28 | ex 414 |
. . . . . 6
โข (๐ โ โค โ (๐ โ โค โ (((2
ยท ๐) + 1) = ๐ โ ((๐ / 2) โค ๐ โ (๐ / 2) < ๐)))) |
30 | 29 | adantl 483 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ โค โ (((2
ยท ๐) + 1) = ๐ โ ((๐ / 2) โค ๐ โ (๐ / 2) < ๐)))) |
31 | 30 | com23 86 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) = ๐ โ (๐ โ โค โ ((๐ / 2) โค ๐ โ (๐ / 2) < ๐)))) |
32 | 31 | rexlimdva 3151 |
. . 3
โข (๐ โ โค โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐ โ (๐ โ โค โ ((๐ / 2) โค ๐ โ (๐ / 2) < ๐)))) |
33 | 1, 32 | sylbid 239 |
. 2
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ (๐ โ โค โ ((๐ / 2) โค ๐ โ (๐ / 2) < ๐)))) |
34 | 33 | 3imp 1112 |
1
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐ โ โค) โ ((๐ / 2) โค ๐ โ (๐ / 2) < ๐)) |