Step | Hyp | Ref
| Expression |
1 | | zeo 12519 |
. . . 4
โข (๐ โ โค โ ((๐ / 2) โ โค โจ
((๐ + 1) / 2) โ
โค)) |
2 | | zre 12436 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
3 | | 2rp 12848 |
. . . . . . . . 9
โข 2 โ
โ+ |
4 | | mod0 13709 |
. . . . . . . . 9
โข ((๐ โ โ โง 2 โ
โ+) โ ((๐ mod 2) = 0 โ (๐ / 2) โ โค)) |
5 | 2, 3, 4 | sylancl 586 |
. . . . . . . 8
โข (๐ โ โค โ ((๐ mod 2) = 0 โ (๐ / 2) โ
โค)) |
6 | 5 | biimpar 478 |
. . . . . . 7
โข ((๐ โ โค โง (๐ / 2) โ โค) โ
(๐ mod 2) =
0) |
7 | | eqeq1 2741 |
. . . . . . . 8
โข ((๐ mod 2) = 0 โ ((๐ mod 2) = 1 โ 0 =
1)) |
8 | | 0ne1 12157 |
. . . . . . . . 9
โข 0 โ
1 |
9 | | eqneqall 2952 |
. . . . . . . . 9
โข (0 = 1
โ (0 โ 1 โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) |
10 | 8, 9 | mpi 20 |
. . . . . . . 8
โข (0 = 1
โ โ๐ โ
โค ((2 ยท ๐) +
1) = ๐) |
11 | 7, 10 | syl6bi 252 |
. . . . . . 7
โข ((๐ mod 2) = 0 โ ((๐ mod 2) = 1 โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
12 | 6, 11 | syl 17 |
. . . . . 6
โข ((๐ โ โค โง (๐ / 2) โ โค) โ
((๐ mod 2) = 1 โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
13 | 12 | expcom 414 |
. . . . 5
โข ((๐ / 2) โ โค โ
(๐ โ โค โ
((๐ mod 2) = 1 โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐))) |
14 | | peano2zm 12476 |
. . . . . . . . 9
โข (((๐ + 1) / 2) โ โค โ
(((๐ + 1) / 2) โ 1)
โ โค) |
15 | | zcn 12437 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
16 | | xp1d2m1eqxm1d2 12340 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((๐ + 1) / 2) โ 1) = ((๐ โ 1) /
2)) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โค โ (((๐ + 1) / 2) โ 1) = ((๐ โ 1) /
2)) |
18 | 17 | eleq1d 2822 |
. . . . . . . . . 10
โข (๐ โ โค โ ((((๐ + 1) / 2) โ 1) โ
โค โ ((๐ โ
1) / 2) โ โค)) |
19 | 18 | biimpd 228 |
. . . . . . . . 9
โข (๐ โ โค โ ((((๐ + 1) / 2) โ 1) โ
โค โ ((๐ โ
1) / 2) โ โค)) |
20 | 14, 19 | mpan9 507 |
. . . . . . . 8
โข ((((๐ + 1) / 2) โ โค โง
๐ โ โค) โ
((๐ โ 1) / 2) โ
โค) |
21 | | oveq2 7357 |
. . . . . . . . . . 11
โข (๐ = ((๐ โ 1) / 2) โ (2 ยท ๐) = (2 ยท ((๐ โ 1) /
2))) |
22 | 21 | adantl 482 |
. . . . . . . . . 10
โข
(((((๐ + 1) / 2)
โ โค โง ๐
โ โค) โง ๐ =
((๐ โ 1) / 2)) โ
(2 ยท ๐) = (2
ยท ((๐ โ 1) /
2))) |
23 | 22 | oveq1d 7364 |
. . . . . . . . 9
โข
(((((๐ + 1) / 2)
โ โค โง ๐
โ โค) โง ๐ =
((๐ โ 1) / 2)) โ
((2 ยท ๐) + 1) = ((2
ยท ((๐ โ 1) /
2)) + 1)) |
24 | | peano2zm 12476 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
25 | 24 | zcnd 12540 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (๐ โ 1) โ
โ) |
26 | | 2cnd 12164 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 โ
โ) |
27 | | 2ne0 12190 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
28 | 27 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 โ
0) |
29 | 25, 26, 28 | divcan2d 11866 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (2
ยท ((๐ โ 1) /
2)) = (๐ โ
1)) |
30 | 29 | oveq1d 7364 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((2
ยท ((๐ โ 1) /
2)) + 1) = ((๐ โ 1) +
1)) |
31 | | npcan1 11513 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
32 | 15, 31 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((๐ โ 1) + 1) = ๐) |
33 | 30, 32 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ โค โ ((2
ยท ((๐ โ 1) /
2)) + 1) = ๐) |
34 | 33 | ad2antlr 725 |
. . . . . . . . 9
โข
(((((๐ + 1) / 2)
โ โค โง ๐
โ โค) โง ๐ =
((๐ โ 1) / 2)) โ
((2 ยท ((๐ โ 1)
/ 2)) + 1) = ๐) |
35 | 23, 34 | eqtrd 2777 |
. . . . . . . 8
โข
(((((๐ + 1) / 2)
โ โค โง ๐
โ โค) โง ๐ =
((๐ โ 1) / 2)) โ
((2 ยท ๐) + 1) =
๐) |
36 | 20, 35 | rspcedeq1vd 3584 |
. . . . . . 7
โข ((((๐ + 1) / 2) โ โค โง
๐ โ โค) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐) |
37 | 36 | a1d 25 |
. . . . . 6
โข ((((๐ + 1) / 2) โ โค โง
๐ โ โค) โ
((๐ mod 2) = 1 โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
38 | 37 | ex 413 |
. . . . 5
โข (((๐ + 1) / 2) โ โค โ
(๐ โ โค โ
((๐ mod 2) = 1 โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐))) |
39 | 13, 38 | jaoi 855 |
. . . 4
โข (((๐ / 2) โ โค โจ
((๐ + 1) / 2) โ
โค) โ (๐ โ
โค โ ((๐ mod 2) =
1 โ โ๐ โ
โค ((2 ยท ๐) +
1) = ๐))) |
40 | 1, 39 | mpcom 38 |
. . 3
โข (๐ โ โค โ ((๐ mod 2) = 1 โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
41 | | oveq1 7356 |
. . . . . 6
โข (๐ = ((2 ยท ๐) + 1) โ (๐ mod 2) = (((2 ยท ๐) + 1) mod 2)) |
42 | 41 | eqcoms 2745 |
. . . . 5
โข (((2
ยท ๐) + 1) = ๐ โ (๐ mod 2) = (((2 ยท ๐) + 1) mod 2)) |
43 | | 2cnd 12164 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 2 โ
โ) |
44 | | zcn 12437 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
45 | 43, 44 | mulcomd 11109 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (2
ยท ๐) = (๐ ยท 2)) |
46 | 45 | oveq1d 7364 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((2
ยท ๐) mod 2) =
((๐ ยท 2) mod
2)) |
47 | | mulmod0 13710 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง 2 โ
โ+) โ ((๐ ยท 2) mod 2) = 0) |
48 | 3, 47 | mpan2 689 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((๐ ยท 2) mod 2) =
0) |
49 | 46, 48 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ โค โ ((2
ยท ๐) mod 2) =
0) |
50 | 49 | oveq1d 7364 |
. . . . . . . . 9
โข (๐ โ โค โ (((2
ยท ๐) mod 2) + 1) =
(0 + 1)) |
51 | | 0p1e1 12208 |
. . . . . . . . 9
โข (0 + 1) =
1 |
52 | 50, 51 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ โ โค โ (((2
ยท ๐) mod 2) + 1) =
1) |
53 | 52 | oveq1d 7364 |
. . . . . . 7
โข (๐ โ โค โ ((((2
ยท ๐) mod 2) + 1) mod
2) = (1 mod 2)) |
54 | | 2z 12465 |
. . . . . . . . . . 11
โข 2 โ
โค |
55 | 54 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โค โ 2 โ
โค) |
56 | | id 22 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โค) |
57 | 55, 56 | zmulcld 12545 |
. . . . . . . . 9
โข (๐ โ โค โ (2
ยท ๐) โ
โค) |
58 | 57 | zred 12539 |
. . . . . . . 8
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
59 | | 1red 11089 |
. . . . . . . 8
โข (๐ โ โค โ 1 โ
โ) |
60 | 3 | a1i 11 |
. . . . . . . 8
โข (๐ โ โค โ 2 โ
โ+) |
61 | | modaddmod 13743 |
. . . . . . . 8
โข (((2
ยท ๐) โ โ
โง 1 โ โ โง 2 โ โ+) โ ((((2
ยท ๐) mod 2) + 1) mod
2) = (((2 ยท ๐) + 1)
mod 2)) |
62 | 58, 59, 60, 61 | syl3anc 1371 |
. . . . . . 7
โข (๐ โ โค โ ((((2
ยท ๐) mod 2) + 1) mod
2) = (((2 ยท ๐) + 1)
mod 2)) |
63 | | 2re 12160 |
. . . . . . . . 9
โข 2 โ
โ |
64 | | 1lt2 12257 |
. . . . . . . . 9
โข 1 <
2 |
65 | 63, 64 | pm3.2i 471 |
. . . . . . . 8
โข (2 โ
โ โง 1 < 2) |
66 | | 1mod 13736 |
. . . . . . . 8
โข ((2
โ โ โง 1 < 2) โ (1 mod 2) = 1) |
67 | 65, 66 | mp1i 13 |
. . . . . . 7
โข (๐ โ โค โ (1 mod 2)
= 1) |
68 | 53, 62, 67 | 3eqtr3d 2785 |
. . . . . 6
โข (๐ โ โค โ (((2
ยท ๐) + 1) mod 2) =
1) |
69 | 68 | adantl 482 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) mod 2) =
1) |
70 | 42, 69 | sylan9eqr 2799 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ((2
ยท ๐) + 1) = ๐) โ (๐ mod 2) = 1) |
71 | 70 | rexlimdva2 3152 |
. . 3
โข (๐ โ โค โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐ โ (๐ mod 2) = 1)) |
72 | 40, 71 | impbid 211 |
. 2
โข (๐ โ โค โ ((๐ mod 2) = 1 โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
73 | | odd2np1 16157 |
. 2
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
74 | 72, 73 | bitr4d 281 |
1
โข (๐ โ โค โ ((๐ mod 2) = 1 โ ยฌ 2
โฅ ๐)) |