Step | Hyp | Ref
| Expression |
1 | | odd2np1 11877 |
. . 3
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
2 | | halfre 9131 |
. . . . . . . . . . . . . . . 16
โข (1 / 2)
โ โ |
3 | 2 | a1i 9 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (1 / 2)
โ โ) |
4 | | 1red 7971 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ 1 โ
โ) |
5 | | zre 9256 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ ๐ โ
โ) |
6 | 3, 4, 5 | 3jca 1177 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ((1 / 2)
โ โ โง 1 โ โ โง ๐ โ โ)) |
7 | 6 | adantr 276 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ ((1 / 2)
โ โ โง 1 โ โ โง ๐ โ โ)) |
8 | | halflt1 9135 |
. . . . . . . . . . . . 13
โข (1 / 2)
< 1 |
9 | | axltadd 8026 |
. . . . . . . . . . . . 13
โข (((1 / 2)
โ โ โง 1 โ โ โง ๐ โ โ) โ ((1 / 2) < 1
โ (๐ + (1 / 2)) <
(๐ + 1))) |
10 | 7, 8, 9 | mpisyl 1446 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + (1 / 2)) < (๐ + 1)) |
11 | | zre 9256 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
12 | 11 | adantl 277 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
13 | 5, 3 | readdcld 7986 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ + (1 / 2)) โ
โ) |
14 | 13 | adantr 276 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + (1 / 2)) โ
โ) |
15 | | peano2z 9288 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (๐ + 1) โ
โค) |
16 | 15 | zred 9374 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ + 1) โ
โ) |
17 | 16 | adantr 276 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + 1) โ
โ) |
18 | | lttr 8030 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ + (1 / 2)) โ โ โง
(๐ + 1) โ โ)
โ ((๐ < (๐ + (1 / 2)) โง (๐ + (1 / 2)) < (๐ + 1)) โ ๐ < (๐ + 1))) |
19 | 12, 14, 17, 18 | syl3anc 1238 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ < (๐ + (1 / 2)) โง (๐ + (1 / 2)) < (๐ + 1)) โ ๐ < (๐ + 1))) |
20 | 10, 19 | mpan2d 428 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (๐ + (1 / 2)) โ ๐ < (๐ + 1))) |
21 | | zleltp1 9307 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
22 | 21 | ancoms 268 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
23 | 20, 22 | sylibrd 169 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (๐ + (1 / 2)) โ ๐ โค ๐)) |
24 | | halfgt0 9133 |
. . . . . . . . . . . 12
โข 0 < (1
/ 2) |
25 | 3, 5 | jca 306 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ((1 / 2)
โ โ โง ๐
โ โ)) |
26 | 25 | adantr 276 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ ((1 / 2)
โ โ โง ๐
โ โ)) |
27 | | ltaddpos 8408 |
. . . . . . . . . . . . 13
โข (((1 / 2)
โ โ โง ๐
โ โ) โ (0 < (1 / 2) โ ๐ < (๐ + (1 / 2)))) |
28 | 26, 27 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (0 <
(1 / 2) โ ๐ <
(๐ + (1 /
2)))) |
29 | 24, 28 | mpbii 148 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ๐ < (๐ + (1 / 2))) |
30 | 5 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
31 | | lelttr 8045 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ โง (๐ + (1 / 2)) โ โ)
โ ((๐ โค ๐ โง ๐ < (๐ + (1 / 2))) โ ๐ < (๐ + (1 / 2)))) |
32 | 12, 30, 14, 31 | syl3anc 1238 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ โค ๐ โง ๐ < (๐ + (1 / 2))) โ ๐ < (๐ + (1 / 2)))) |
33 | 29, 32 | mpan2d 428 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ ๐ < (๐ + (1 / 2)))) |
34 | 23, 33 | impbid 129 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (๐ + (1 / 2)) โ ๐ โค ๐)) |
35 | | zcn 9257 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
36 | | 1cnd 7972 |
. . . . . . . . . . . 12
โข (๐ โ โค โ 1 โ
โ) |
37 | | 2cn 8989 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
38 | | 2ap0 9011 |
. . . . . . . . . . . . . 14
โข 2 #
0 |
39 | 37, 38 | pm3.2i 272 |
. . . . . . . . . . . . 13
โข (2 โ
โ โง 2 # 0) |
40 | 39 | a1i 9 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (2 โ
โ โง 2 # 0)) |
41 | | muldivdirap 8663 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 1 โ
โ โง (2 โ โ โง 2 # 0)) โ (((2 ยท ๐) + 1) / 2) = (๐ + (1 / 2))) |
42 | 35, 36, 40, 41 | syl3anc 1238 |
. . . . . . . . . . 11
โข (๐ โ โค โ (((2
ยท ๐) + 1) / 2) =
(๐ + (1 /
2))) |
43 | 42 | breq2d 4015 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ < (((2 ยท ๐) + 1) / 2) โ ๐ < (๐ + (1 / 2)))) |
44 | 43 | adantr 276 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (((2 ยท ๐) + 1) / 2) โ ๐ < (๐ + (1 / 2)))) |
45 | | 2z 9280 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โค |
46 | 45 | a1i 9 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ 2 โ
โค) |
47 | | id 19 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ ๐ โ
โค) |
48 | 46, 47 | zmulcld 9380 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (2
ยท ๐) โ
โค) |
49 | 48 | zcnd 9375 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
50 | 49 | adantr 276 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (2
ยท ๐) โ
โ) |
51 | | pncan1 8333 |
. . . . . . . . . . . . 13
โข ((2
ยท ๐) โ โ
โ (((2 ยท ๐) +
1) โ 1) = (2 ยท ๐)) |
52 | 50, 51 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) โ 1)
= (2 ยท ๐)) |
53 | 52 | oveq1d 5889 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ((((2
ยท ๐) + 1) โ 1)
/ 2) = ((2 ยท ๐) /
2)) |
54 | | 2cnd 8991 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 โ
โ) |
55 | 38 | a1i 9 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 #
0) |
56 | 35, 54, 55 | divcanap3d 8751 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ((2
ยท ๐) / 2) = ๐) |
57 | 56 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ((2
ยท ๐) / 2) = ๐) |
58 | 53, 57 | eqtrd 2210 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ ((((2
ยท ๐) + 1) โ 1)
/ 2) = ๐) |
59 | 58 | breq2d 4015 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ((((2 ยท ๐) + 1) โ 1) / 2) โ
๐ โค ๐)) |
60 | 34, 44, 59 | 3bitr4d 220 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < (((2 ยท ๐) + 1) / 2) โ ๐ โค ((((2 ยท ๐) + 1) โ 1) /
2))) |
61 | | oveq1 5881 |
. . . . . . . . . 10
โข (((2
ยท ๐) + 1) = ๐ โ (((2 ยท ๐) + 1) / 2) = (๐ / 2)) |
62 | 61 | breq2d 4015 |
. . . . . . . . 9
โข (((2
ยท ๐) + 1) = ๐ โ (๐ < (((2 ยท ๐) + 1) / 2) โ ๐ < (๐ / 2))) |
63 | | oveq1 5881 |
. . . . . . . . . . 11
โข (((2
ยท ๐) + 1) = ๐ โ (((2 ยท ๐) + 1) โ 1) = (๐ โ 1)) |
64 | 63 | oveq1d 5889 |
. . . . . . . . . 10
โข (((2
ยท ๐) + 1) = ๐ โ ((((2 ยท ๐) + 1) โ 1) / 2) = ((๐ โ 1) /
2)) |
65 | 64 | breq2d 4015 |
. . . . . . . . 9
โข (((2
ยท ๐) + 1) = ๐ โ (๐ โค ((((2 ยท ๐) + 1) โ 1) / 2) โ ๐ โค ((๐ โ 1) / 2))) |
66 | 62, 65 | bibi12d 235 |
. . . . . . . 8
โข (((2
ยท ๐) + 1) = ๐ โ ((๐ < (((2 ยท ๐) + 1) / 2) โ ๐ โค ((((2 ยท ๐) + 1) โ 1) / 2)) โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2)))) |
67 | 60, 66 | syl5ibcom 155 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) = ๐ โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2)))) |
68 | 67 | ex 115 |
. . . . . 6
โข (๐ โ โค โ (๐ โ โค โ (((2
ยท ๐) + 1) = ๐ โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
69 | 68 | adantl 277 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ โค โ (((2
ยท ๐) + 1) = ๐ โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
70 | 69 | com23 78 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) = ๐ โ (๐ โ โค โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
71 | 70 | rexlimdva 2594 |
. . 3
โข (๐ โ โค โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐ โ (๐ โ โค โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
72 | 1, 71 | sylbid 150 |
. 2
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ (๐ โ โค โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))))) |
73 | 72 | 3imp 1193 |
1
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐ โ โค) โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))) |