Step | Hyp | Ref
| Expression |
1 | | odd2np1 16158 |
. . 3
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
2 | | halfre 12301 |
. . . . . . . . . . . . . . . 16
โข (1 / 2)
โ โ |
3 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (1 / 2)
โ โ) |
4 | | 1red 11090 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ 1 โ
โ) |
5 | | zre 12437 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ ๐ โ
โ) |
6 | 3, 4, 5 | 3jca 1129 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ((1 / 2)
โ โ โง 1 โ โ โง ๐ โ โ)) |
7 | 6 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ ((1 / 2)
โ โ โง 1 โ โ โง ๐ โ โ)) |
8 | | halflt1 12305 |
. . . . . . . . . . . . 13
โข (1 / 2)
< 1 |
9 | | axltadd 11162 |
. . . . . . . . . . . . 13
โข (((1 / 2)
โ โ โง 1 โ โ โง ๐ โ โ) โ ((1 / 2) < 1
โ (๐ + (1 / 2)) <
(๐ + 1))) |
10 | 7, 8, 9 | mpisyl 21 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + (1 / 2)) < (๐ + 1)) |
11 | | zre 12437 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
12 | 11 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
13 | 5, 3 | readdcld 11118 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ + (1 / 2)) โ
โ) |
14 | 13 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + (1 / 2)) โ
โ) |
15 | | peano2z 12475 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (๐ + 1) โ
โค) |
16 | 15 | zred 12540 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ + 1) โ
โ) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + 1) โ
โ) |
18 | | lttr 11165 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ + (1 / 2)) โ โ โง
(๐ + 1) โ โ)
โ ((๐ < (๐ + (1 / 2)) โง (๐ + (1 / 2)) < (๐ + 1)) โ ๐ < (๐ + 1))) |
19 | 12, 14, 17, 18 | syl3anc 1372 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ < (๐ + (1 / 2)) โง (๐ + (1 / 2)) < (๐ + 1)) โ ๐ < (๐ + 1))) |
20 | 10, 19 | mpan2d 693 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (๐ + (1 / 2)) โ ๐ < (๐ + 1))) |
21 | | zleltp1 12485 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
22 | 21 | ancoms 460 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
23 | 20, 22 | sylibrd 259 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (๐ + (1 / 2)) โ ๐ โค ๐)) |
24 | | halfgt0 12303 |
. . . . . . . . . . . 12
โข 0 < (1
/ 2) |
25 | 3, 5 | jca 513 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ((1 / 2)
โ โ โง ๐
โ โ)) |
26 | 25 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ ((1 / 2)
โ โ โง ๐
โ โ)) |
27 | | ltaddpos 11579 |
. . . . . . . . . . . . 13
โข (((1 / 2)
โ โ โง ๐
โ โ) โ (0 < (1 / 2) โ ๐ < (๐ + (1 / 2)))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (0 <
(1 / 2) โ ๐ <
(๐ + (1 /
2)))) |
29 | 24, 28 | mpbii 232 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ๐ < (๐ + (1 / 2))) |
30 | 5 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
31 | | lelttr 11179 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ โง (๐ + (1 / 2)) โ โ)
โ ((๐ โค ๐ โง ๐ < (๐ + (1 / 2))) โ ๐ < (๐ + (1 / 2)))) |
32 | 12, 30, 14, 31 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ โค ๐ โง ๐ < (๐ + (1 / 2))) โ ๐ < (๐ + (1 / 2)))) |
33 | 29, 32 | mpan2d 693 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ ๐ < (๐ + (1 / 2)))) |
34 | 23, 33 | impbid 211 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (๐ + (1 / 2)) โ ๐ โค ๐)) |
35 | | zcn 12438 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
36 | | 1cnd 11084 |
. . . . . . . . . . . 12
โข (๐ โ โค โ 1 โ
โ) |
37 | | 2cnne0 12297 |
. . . . . . . . . . . . 13
โข (2 โ
โ โง 2 โ 0) |
38 | 37 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (2 โ
โ โง 2 โ 0)) |
39 | | muldivdir 11782 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 1 โ
โ โง (2 โ โ โง 2 โ 0)) โ (((2 ยท ๐) + 1) / 2) = (๐ + (1 / 2))) |
40 | 35, 36, 38, 39 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ โค โ (((2
ยท ๐) + 1) / 2) =
(๐ + (1 /
2))) |
41 | 40 | breq2d 5116 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ < (((2 ยท ๐) + 1) / 2) โ ๐ < (๐ + (1 / 2)))) |
42 | 41 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (((2 ยท ๐) + 1) / 2) โ ๐ < (๐ + (1 / 2)))) |
43 | | 2z 12466 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โค |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ 2 โ
โค) |
45 | | id 22 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ ๐ โ
โค) |
46 | 44, 45 | zmulcld 12546 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (2
ยท ๐) โ
โค) |
47 | 46 | zcnd 12541 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (2
ยท ๐) โ
โ) |
49 | | pncan1 11513 |
. . . . . . . . . . . . 13
โข ((2
ยท ๐) โ โ
โ (((2 ยท ๐) +
1) โ 1) = (2 ยท ๐)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) โ 1)
= (2 ยท ๐)) |
51 | 50 | oveq1d 7365 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ((((2
ยท ๐) + 1) โ 1)
/ 2) = ((2 ยท ๐) /
2)) |
52 | | 2cnd 12165 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 โ
โ) |
53 | | 2ne0 12191 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 โ
0) |
55 | 35, 52, 54 | divcan3d 11870 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ((2
ยท ๐) / 2) = ๐) |
56 | 55 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ((2
ยท ๐) / 2) = ๐) |
57 | 51, 56 | eqtrd 2778 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ ((((2
ยท ๐) + 1) โ 1)
/ 2) = ๐) |
58 | 57 | breq2d 5116 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ((((2 ยท ๐) + 1) โ 1) / 2) โ
๐ โค ๐)) |
59 | 34, 42, 58 | 3bitr4d 311 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (((2 ยท ๐) + 1) / 2) โ ๐ โค ((((2 ยท ๐) + 1) โ 1) /
2))) |
60 | | oveq1 7357 |
. . . . . . . . . 10
โข (((2
ยท ๐) + 1) = ๐ โ (((2 ยท ๐) + 1) / 2) = (๐ / 2)) |
61 | 60 | breq2d 5116 |
. . . . . . . . 9
โข (((2
ยท ๐) + 1) = ๐ โ (๐ < (((2 ยท ๐) + 1) / 2) โ ๐ < (๐ / 2))) |
62 | | oveq1 7357 |
. . . . . . . . . . 11
โข (((2
ยท ๐) + 1) = ๐ โ (((2 ยท ๐) + 1) โ 1) = (๐ โ 1)) |
63 | 62 | oveq1d 7365 |
. . . . . . . . . 10
โข (((2
ยท ๐) + 1) = ๐ โ ((((2 ยท ๐) + 1) โ 1) / 2) = ((๐ โ 1) /
2)) |
64 | 63 | breq2d 5116 |
. . . . . . . . 9
โข (((2
ยท ๐) + 1) = ๐ โ (๐ โค ((((2 ยท ๐) + 1) โ 1) / 2) โ ๐ โค ((๐ โ 1) / 2))) |
65 | 61, 64 | bibi12d 346 |
. . . . . . . 8
โข (((2
ยท ๐) + 1) = ๐ โ ((๐ < (((2 ยท ๐) + 1) / 2) โ ๐ โค ((((2 ยท ๐) + 1) โ 1) / 2)) โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2)))) |
66 | 59, 65 | syl5ibcom 245 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) = ๐ โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2)))) |
67 | 66 | ex 414 |
. . . . . 6
โข (๐ โ โค โ (๐ โ โค โ (((2
ยท ๐) + 1) = ๐ โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
68 | 67 | adantl 483 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ โค โ (((2
ยท ๐) + 1) = ๐ โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
69 | 68 | com23 86 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) = ๐ โ (๐ โ โค โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
70 | 69 | rexlimdva 3151 |
. . 3
โข (๐ โ โค โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐ โ (๐ โ โค โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
71 | 1, 70 | sylbid 239 |
. 2
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ (๐ โ โค โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
72 | 71 | 3imp 1112 |
1
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐ โ โค) โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))) |