Step | Hyp | Ref
| Expression |
1 | | zeo 12520 |
. . . 4
โข (๐ โ โค โ ((๐ / 2) โ โค โจ
((๐ + 1) / 2) โ
โค)) |
2 | | zre 12437 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
3 | | 2rp 12849 |
. . . . . . . . 9
โข 2 โ
โ+ |
4 | | mod0 13710 |
. . . . . . . . 9
โข ((๐ โ โ โง 2 โ
โ+) โ ((๐ mod 2) = 0 โ (๐ / 2) โ โค)) |
5 | 2, 3, 4 | sylancl 587 |
. . . . . . . 8
โข (๐ โ โค โ ((๐ mod 2) = 0 โ (๐ / 2) โ
โค)) |
6 | 5 | biimpar 479 |
. . . . . . 7
โข ((๐ โ โค โง (๐ / 2) โ โค) โ
(๐ mod 2) =
0) |
7 | | eqeq1 2742 |
. . . . . . . 8
โข ((๐ mod 2) = 0 โ ((๐ mod 2) = 1 โ 0 =
1)) |
8 | | 0ne1 12158 |
. . . . . . . . 9
โข 0 โ
1 |
9 | | eqneqall 2953 |
. . . . . . . . 9
โข (0 = 1
โ (0 โ 1 โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) |
10 | 8, 9 | mpi 20 |
. . . . . . . 8
โข (0 = 1
โ โ๐ โ
โค ((2 ยท ๐) +
1) = ๐) |
11 | 7, 10 | syl6bi 253 |
. . . . . . 7
โข ((๐ mod 2) = 0 โ ((๐ mod 2) = 1 โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
12 | 6, 11 | syl 17 |
. . . . . 6
โข ((๐ โ โค โง (๐ / 2) โ โค) โ
((๐ mod 2) = 1 โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
13 | 12 | expcom 415 |
. . . . 5
โข ((๐ / 2) โ โค โ
(๐ โ โค โ
((๐ mod 2) = 1 โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐))) |
14 | | peano2zm 12477 |
. . . . . . . . 9
โข (((๐ + 1) / 2) โ โค โ
(((๐ + 1) / 2) โ 1)
โ โค) |
15 | | zcn 12438 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
16 | | xp1d2m1eqxm1d2 12341 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((๐ + 1) / 2) โ 1) = ((๐ โ 1) /
2)) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โค โ (((๐ + 1) / 2) โ 1) = ((๐ โ 1) /
2)) |
18 | 17 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ โ โค โ ((((๐ + 1) / 2) โ 1) โ
โค โ ((๐ โ
1) / 2) โ โค)) |
19 | 18 | biimpd 228 |
. . . . . . . . 9
โข (๐ โ โค โ ((((๐ + 1) / 2) โ 1) โ
โค โ ((๐ โ
1) / 2) โ โค)) |
20 | 14, 19 | mpan9 508 |
. . . . . . . 8
โข ((((๐ + 1) / 2) โ โค โง
๐ โ โค) โ
((๐ โ 1) / 2) โ
โค) |
21 | | oveq2 7358 |
. . . . . . . . . . 11
โข (๐ = ((๐ โ 1) / 2) โ (2 ยท ๐) = (2 ยท ((๐ โ 1) /
2))) |
22 | 21 | adantl 483 |
. . . . . . . . . 10
โข
(((((๐ + 1) / 2)
โ โค โง ๐
โ โค) โง ๐ =
((๐ โ 1) / 2)) โ
(2 ยท ๐) = (2
ยท ((๐ โ 1) /
2))) |
23 | 22 | oveq1d 7365 |
. . . . . . . . 9
โข
(((((๐ + 1) / 2)
โ โค โง ๐
โ โค) โง ๐ =
((๐ โ 1) / 2)) โ
((2 ยท ๐) + 1) = ((2
ยท ((๐ โ 1) /
2)) + 1)) |
24 | | peano2zm 12477 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
25 | 24 | zcnd 12541 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (๐ โ 1) โ
โ) |
26 | | 2cnd 12165 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 โ
โ) |
27 | | 2ne0 12191 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
28 | 27 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 โ
0) |
29 | 25, 26, 28 | divcan2d 11867 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (2
ยท ((๐ โ 1) /
2)) = (๐ โ
1)) |
30 | 29 | oveq1d 7365 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((2
ยท ((๐ โ 1) /
2)) + 1) = ((๐ โ 1) +
1)) |
31 | | npcan1 11514 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
32 | 15, 31 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((๐ โ 1) + 1) = ๐) |
33 | 30, 32 | eqtrd 2778 |
. . . . . . . . . 10
โข (๐ โ โค โ ((2
ยท ((๐ โ 1) /
2)) + 1) = ๐) |
34 | 33 | ad2antlr 726 |
. . . . . . . . 9
โข
(((((๐ + 1) / 2)
โ โค โง ๐
โ โค) โง ๐ =
((๐ โ 1) / 2)) โ
((2 ยท ((๐ โ 1)
/ 2)) + 1) = ๐) |
35 | 23, 34 | eqtrd 2778 |
. . . . . . . 8
โข
(((((๐ + 1) / 2)
โ โค โง ๐
โ โค) โง ๐ =
((๐ โ 1) / 2)) โ
((2 ยท ๐) + 1) =
๐) |
36 | 20, 35 | rspcedeq1vd 3585 |
. . . . . . 7
โข ((((๐ + 1) / 2) โ โค โง
๐ โ โค) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐) |
37 | 36 | a1d 25 |
. . . . . 6
โข ((((๐ + 1) / 2) โ โค โง
๐ โ โค) โ
((๐ mod 2) = 1 โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
38 | 37 | ex 414 |
. . . . 5
โข (((๐ + 1) / 2) โ โค โ
(๐ โ โค โ
((๐ mod 2) = 1 โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐))) |
39 | 13, 38 | jaoi 856 |
. . . 4
โข (((๐ / 2) โ โค โจ
((๐ + 1) / 2) โ
โค) โ (๐ โ
โค โ ((๐ mod 2) =
1 โ โ๐ โ
โค ((2 ยท ๐) +
1) = ๐))) |
40 | 1, 39 | mpcom 38 |
. . 3
โข (๐ โ โค โ ((๐ mod 2) = 1 โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
41 | | oveq1 7357 |
. . . . . 6
โข (๐ = ((2 ยท ๐) + 1) โ (๐ mod 2) = (((2 ยท ๐) + 1) mod 2)) |
42 | 41 | eqcoms 2746 |
. . . . 5
โข (((2
ยท ๐) + 1) = ๐ โ (๐ mod 2) = (((2 ยท ๐) + 1) mod 2)) |
43 | | 2cnd 12165 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 โ
โ) |
44 | | zcn 12438 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
45 | 43, 44 | mulcomd 11110 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (2
ยท ๐) = (๐ ยท 2)) |
46 | 45 | oveq1d 7365 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((2
ยท ๐) mod 2) =
((๐ ยท 2) mod
2)) |
47 | | mulmod0 13711 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง 2 โ
โ+) โ ((๐ ยท 2) mod 2) = 0) |
48 | 3, 47 | mpan2 690 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((๐ ยท 2) mod 2) =
0) |
49 | 46, 48 | eqtrd 2778 |
. . . . . . . . . 10
โข (๐ โ โค โ ((2
ยท ๐) mod 2) =
0) |
50 | 49 | oveq1d 7365 |
. . . . . . . . 9
โข (๐ โ โค โ (((2
ยท ๐) mod 2) + 1) =
(0 + 1)) |
51 | | 0p1e1 12209 |
. . . . . . . . 9
โข (0 + 1) =
1 |
52 | 50, 51 | eqtrdi 2794 |
. . . . . . . 8
โข (๐ โ โค โ (((2
ยท ๐) mod 2) + 1) =
1) |
53 | 52 | oveq1d 7365 |
. . . . . . 7
โข (๐ โ โค โ ((((2
ยท ๐) mod 2) + 1) mod
2) = (1 mod 2)) |
54 | | 2z 12466 |
. . . . . . . . . . 11
โข 2 โ
โค |
55 | 54 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โค โ 2 โ
โค) |
56 | | id 22 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โค) |
57 | 55, 56 | zmulcld 12546 |
. . . . . . . . 9
โข (๐ โ โค โ (2
ยท ๐) โ
โค) |
58 | 57 | zred 12540 |
. . . . . . . 8
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
59 | | 1red 11090 |
. . . . . . . 8
โข (๐ โ โค โ 1 โ
โ) |
60 | 3 | a1i 11 |
. . . . . . . 8
โข (๐ โ โค โ 2 โ
โ+) |
61 | | modaddmod 13744 |
. . . . . . . 8
โข (((2
ยท ๐) โ โ
โง 1 โ โ โง 2 โ โ+) โ ((((2
ยท ๐) mod 2) + 1) mod
2) = (((2 ยท ๐) + 1)
mod 2)) |
62 | 58, 59, 60, 61 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ โค โ ((((2
ยท ๐) mod 2) + 1) mod
2) = (((2 ยท ๐) + 1)
mod 2)) |
63 | | 2re 12161 |
. . . . . . . . 9
โข 2 โ
โ |
64 | | 1lt2 12258 |
. . . . . . . . 9
โข 1 <
2 |
65 | 63, 64 | pm3.2i 472 |
. . . . . . . 8
โข (2 โ
โ โง 1 < 2) |
66 | | 1mod 13737 |
. . . . . . . 8
โข ((2
โ โ โง 1 < 2) โ (1 mod 2) = 1) |
67 | 65, 66 | mp1i 13 |
. . . . . . 7
โข (๐ โ โค โ (1 mod 2)
= 1) |
68 | 53, 62, 67 | 3eqtr3d 2786 |
. . . . . 6
โข (๐ โ โค โ (((2
ยท ๐) + 1) mod 2) =
1) |
69 | 68 | adantl 483 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) mod 2) =
1) |
70 | 42, 69 | sylan9eqr 2800 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ((2
ยท ๐) + 1) = ๐) โ (๐ mod 2) = 1) |
71 | 70 | rexlimdva2 3153 |
. . 3
โข (๐ โ โค โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐ โ (๐ mod 2) = 1)) |
72 | 40, 71 | impbid 211 |
. 2
โข (๐ โ โค โ ((๐ mod 2) = 1 โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
73 | | odd2np1 16158 |
. 2
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
74 | 72, 73 | bitr4d 282 |
1
โข (๐ โ โค โ ((๐ mod 2) = 1 โ ยฌ 2
โฅ ๐)) |