Step | Hyp | Ref
| Expression |
1 | | zre 12562 |
. . . . . 6
โข (๐ด โ โค โ ๐ด โ
โ) |
2 | 1 | 3ad2ant1 1134 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ๐ด โ
โ) |
3 | | 2rp 12979 |
. . . . . . . . 9
โข 2 โ
โ+ |
4 | 3 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ 2 โ
โ+) |
5 | | nnz 12579 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
6 | 4, 5 | rpexpcld 14210 |
. . . . . . 7
โข (๐ โ โ โ
(2โ๐) โ
โ+) |
7 | 6 | rpred 13016 |
. . . . . 6
โข (๐ โ โ โ
(2โ๐) โ
โ) |
8 | 7 | 3ad2ant3 1136 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (2โ๐) โ
โ) |
9 | 2, 8 | resubcld 11642 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (๐ด โ
(2โ๐)) โ
โ) |
10 | 6 | 3ad2ant3 1136 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (2โ๐) โ
โ+) |
11 | 9, 10 | modcld 13840 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ
(2โ๐)) mod
(2โ๐)) โ
โ) |
12 | 9, 11 | resubcld 11642 |
. . 3
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ
(2โ๐)) โ ((๐ด โ (2โ๐)) mod (2โ๐))) โ โ) |
13 | | peano2zm 12605 |
. . . . . 6
โข (๐ด โ โค โ (๐ด โ 1) โ
โค) |
14 | 13 | zred 12666 |
. . . . 5
โข (๐ด โ โค โ (๐ด โ 1) โ
โ) |
15 | 14 | 3ad2ant1 1134 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (๐ด โ 1) โ
โ) |
16 | 15, 10 | modcld 13840 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ 1) mod
(2โ๐)) โ
โ) |
17 | 15, 16 | resubcld 11642 |
. . 3
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ 1)
โ ((๐ด โ 1) mod
(2โ๐))) โ
โ) |
18 | | 1red 11215 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ 1 โ โ) |
19 | 18, 16 | readdcld 11243 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (1 + ((๐ด โ 1)
mod (2โ๐))) โ
โ) |
20 | 8, 11 | readdcld 11243 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((2โ๐) +
((๐ด โ (2โ๐)) mod (2โ๐))) โ โ) |
21 | | 2nn 12285 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
22 | 21 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 2 โ
โ) |
23 | | nnnn0 12479 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ0) |
24 | 22, 23 | nnexpcld 14208 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(2โ๐) โ
โ) |
25 | 24 | anim2i 618 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ด โ โค โง
(2โ๐) โ
โ)) |
26 | 25 | 3adant2 1132 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (๐ด โ โค
โง (2โ๐) โ
โ)) |
27 | | m1modmmod 47207 |
. . . . . . . . . 10
โข ((๐ด โ โค โง
(2โ๐) โ โ)
โ (((๐ด โ 1) mod
(2โ๐)) โ (๐ด mod (2โ๐))) = if((๐ด mod (2โ๐)) = 0, ((2โ๐) โ 1), -1)) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (((๐ด โ 1) mod
(2โ๐)) โ (๐ด mod (2โ๐))) = if((๐ด mod (2โ๐)) = 0, ((2โ๐) โ 1), -1)) |
29 | | nnz 12579 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ 1) / 2) โ โ
โ ((๐ด โ 1) / 2)
โ โค) |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โค โง ๐ โ โ) โ (((๐ด โ 1) / 2) โ โ
โ ((๐ด โ 1) / 2)
โ โค)) |
31 | | zcn 12563 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด โ โค โ ๐ด โ
โ) |
32 | | xp1d2m1eqxm1d2 12466 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ด โ โ โ (((๐ด + 1) / 2) โ 1) = ((๐ด โ 1) /
2)) |
33 | 32 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด โ โ โ ((๐ด โ 1) / 2) = (((๐ด + 1) / 2) โ
1)) |
34 | 31, 33 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ โค โ ((๐ด โ 1) / 2) = (((๐ด + 1) / 2) โ
1)) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ด โ 1) / 2) = (((๐ด + 1) / 2) โ
1)) |
36 | 35 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โค โง ๐ โ โ) โ (((๐ด โ 1) / 2) โ โค
โ (((๐ด + 1) / 2)
โ 1) โ โค)) |
37 | | peano2z 12603 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด + 1) / 2) โ 1) โ
โค โ ((((๐ด + 1) /
2) โ 1) + 1) โ โค) |
38 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ โค โง ๐ โ โ) โ ๐ด โ
โ) |
39 | | 1cnd 11209 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ โค โง ๐ โ โ) โ 1 โ
โ) |
40 | 38, 39 | addcld 11233 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ด + 1) โ
โ) |
41 | 40 | halfcld 12457 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ด + 1) / 2) โ
โ) |
42 | 41, 39 | npcand 11575 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โค โง ๐ โ โ) โ
((((๐ด + 1) / 2) โ 1)
+ 1) = ((๐ด + 1) /
2)) |
43 | 42 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ โ โ) โ
(((((๐ด + 1) / 2) โ 1)
+ 1) โ โค โ ((๐ด + 1) / 2) โ โค)) |
44 | 37, 43 | imbitrid 243 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โค โง ๐ โ โ) โ
((((๐ด + 1) / 2) โ 1)
โ โค โ ((๐ด +
1) / 2) โ โค)) |
45 | 36, 44 | sylbid 239 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โค โง ๐ โ โ) โ (((๐ด โ 1) / 2) โ โค
โ ((๐ด + 1) / 2) โ
โค)) |
46 | | mod0 13841 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง
(2โ๐) โ
โ+) โ ((๐ด mod (2โ๐)) = 0 โ (๐ด / (2โ๐)) โ โค)) |
47 | 1, 6, 46 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ด mod (2โ๐)) = 0 โ (๐ด / (2โ๐)) โ โค)) |
48 | 22 | nnzd 12585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ 2 โ
โค) |
49 | | nnm1nn0 12513 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
50 | | zexpcl 14042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((2
โ โค โง (๐
โ 1) โ โ0) โ (2โ(๐ โ 1)) โ
โค) |
51 | 48, 49, 50 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ
(2โ(๐ โ 1))
โ โค) |
52 | 51 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด โ โค โง ๐ โ โ) โ
(2โ(๐ โ 1))
โ โค) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ด โ โค โง ๐ โ โ) โง (๐ด / (2โ๐)) โ โค) โ (2โ(๐ โ 1)) โ
โค) |
54 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ด โ โค โง ๐ โ โ) โง (๐ด / (2โ๐)) โ โค) โ (๐ด / (2โ๐)) โ โค) |
55 | 53, 54 | zmulcld 12672 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ด โ โค โง ๐ โ โ) โง (๐ด / (2โ๐)) โ โค) โ ((2โ(๐ โ 1)) ยท (๐ด / (2โ๐))) โ โค) |
56 | 55 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ด / (2โ๐)) โ โค โ ((2โ(๐ โ 1)) ยท (๐ด / (2โ๐))) โ โค)) |
57 | 5 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ด โ โค โง ๐ โ โ) โ ๐ โ
โค) |
58 | 57 | zcnd 12667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ด โ โค โง ๐ โ โ) โ ๐ โ
โ) |
59 | 39 | negcld 11558 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ด โ โค โง ๐ โ โ) โ -1
โ โ) |
60 | 58, 39 | negsubd 11577 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ + -1) = (๐ โ 1)) |
61 | 60 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ โ 1) = (๐ + -1)) |
62 | 58, 59, 61 | mvrladdd 11627 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ โ 1) โ ๐) = -1) |
63 | 62 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ด โ โค โง ๐ โ โ) โ
(2โ((๐ โ 1)
โ ๐)) =
(2โ-1)) |
64 | | 2cnd 12290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด โ โค โง ๐ โ โ) โ 2 โ
โ) |
65 | | 2ne0 12316 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 2 โ
0 |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด โ โค โง ๐ โ โ) โ 2 โ
0) |
67 | | 1zzd 12593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ 1 โ
โค) |
68 | 5, 67 | zsubcld 12671 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ (๐ โ 1) โ
โค) |
69 | 68, 5 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ ((๐ โ 1) โ โค โง
๐ โ
โค)) |
70 | 69 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ โ 1) โ โค โง
๐ โ
โค)) |
71 | | expsub 14076 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((2
โ โ โง 2 โ 0) โง ((๐ โ 1) โ โค โง ๐ โ โค)) โ
(2โ((๐ โ 1)
โ ๐)) =
((2โ(๐ โ 1)) /
(2โ๐))) |
72 | 64, 66, 70, 71 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ด โ โค โง ๐ โ โ) โ
(2โ((๐ โ 1)
โ ๐)) =
((2โ(๐ โ 1)) /
(2โ๐))) |
73 | | expn1 14037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (2 โ
โ โ (2โ-1) = (1 / 2)) |
74 | 64, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ด โ โค โง ๐ โ โ) โ
(2โ-1) = (1 / 2)) |
75 | 63, 72, 74 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด โ โค โง ๐ โ โ) โ
((2โ(๐ โ 1)) /
(2โ๐)) = (1 /
2)) |
76 | 75 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ด ยท ((2โ(๐ โ 1)) / (2โ๐))) = (๐ด ยท (1 / 2))) |
77 | | 2cnd 12290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ 2 โ
โ) |
78 | 77, 49 | expcld 14111 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ
(2โ(๐ โ 1))
โ โ) |
79 | 78 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด โ โค โง ๐ โ โ) โ
(2โ(๐ โ 1))
โ โ) |
80 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด โ โค โง ๐ โ โ) โ 2 โ
โ+) |
81 | 80, 57 | rpexpcld 14210 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ด โ โค โง ๐ โ โ) โ
(2โ๐) โ
โ+) |
82 | 81 | rpcnne0d 13025 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด โ โค โง ๐ โ โ) โ
((2โ๐) โ โ
โง (2โ๐) โ
0)) |
83 | | div12 11894 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((2โ(๐ โ
1)) โ โ โง ๐ด
โ โ โง ((2โ๐) โ โ โง (2โ๐) โ 0)) โ
((2โ(๐ โ 1))
ยท (๐ด / (2โ๐))) = (๐ด ยท ((2โ(๐ โ 1)) / (2โ๐)))) |
84 | 79, 38, 82, 83 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ โค โง ๐ โ โ) โ
((2โ(๐ โ 1))
ยท (๐ด / (2โ๐))) = (๐ด ยท ((2โ(๐ โ 1)) / (2โ๐)))) |
85 | 38, 64, 66 | divrecd 11993 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ด / 2) = (๐ด ยท (1 / 2))) |
86 | 76, 84, 85 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โค โง ๐ โ โ) โ
((2โ(๐ โ 1))
ยท (๐ด / (2โ๐))) = (๐ด / 2)) |
87 | 86 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โค โง ๐ โ โ) โ
(((2โ(๐ โ 1))
ยท (๐ด / (2โ๐))) โ โค โ (๐ด / 2) โ
โค)) |
88 | 56, 87 | sylibd 238 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ด / (2โ๐)) โ โค โ (๐ด / 2) โ โค)) |
89 | 47, 88 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ด mod (2โ๐)) = 0 โ (๐ด / 2) โ โค)) |
90 | | zeo2 12649 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ โค โ ((๐ด / 2) โ โค โ
ยฌ ((๐ด + 1) / 2) โ
โค)) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ด / 2) โ โค โ
ยฌ ((๐ด + 1) / 2) โ
โค)) |
92 | 89, 91 | sylibd 238 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ด mod (2โ๐)) = 0 โ ยฌ ((๐ด + 1) / 2) โ โค)) |
93 | 92 | necon2ad 2956 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โค โง ๐ โ โ) โ (((๐ด + 1) / 2) โ โค โ
(๐ด mod (2โ๐)) โ 0)) |
94 | 30, 45, 93 | 3syld 60 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง ๐ โ โ) โ (((๐ด โ 1) / 2) โ โ
โ (๐ด mod (2โ๐)) โ 0)) |
95 | 94 | ex 414 |
. . . . . . . . . . . . 13
โข (๐ด โ โค โ (๐ โ โ โ (((๐ด โ 1) / 2) โ โ
โ (๐ด mod (2โ๐)) โ 0))) |
96 | 95 | com23 86 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ (((๐ด โ 1) / 2) โ โ
โ (๐ โ โ
โ (๐ด mod (2โ๐)) โ 0))) |
97 | 96 | 3imp 1112 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (๐ด mod (2โ๐)) โ 0) |
98 | 97 | neneqd 2946 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ยฌ (๐ด mod
(2โ๐)) =
0) |
99 | 98 | iffalsed 4540 |
. . . . . . . . 9
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ if((๐ด mod
(2โ๐)) = 0,
((2โ๐) โ 1), -1)
= -1) |
100 | 28, 99 | eqtrd 2773 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (((๐ด โ 1) mod
(2โ๐)) โ (๐ด mod (2โ๐))) = -1) |
101 | | neg1lt0 12329 |
. . . . . . . . . 10
โข -1 <
0 |
102 | | 2re 12286 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
103 | | 1lt2 12383 |
. . . . . . . . . . . . 13
โข 1 <
2 |
104 | | expgt1 14066 |
. . . . . . . . . . . . 13
โข ((2
โ โ โง ๐
โ โ โง 1 < 2) โ 1 < (2โ๐)) |
105 | 102, 103,
104 | mp3an13 1453 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 1 <
(2โ๐)) |
106 | | 1red 11215 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 1 โ
โ) |
107 | 106, 7 | posdifd 11801 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1 <
(2โ๐) โ 0 <
((2โ๐) โ
1))) |
108 | 105, 107 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ โ โ 0 <
((2โ๐) โ
1)) |
109 | 106 | renegcld 11641 |
. . . . . . . . . . . 12
โข (๐ โ โ โ -1 โ
โ) |
110 | | 0red 11217 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 โ
โ) |
111 | 7, 106 | resubcld 11642 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
((2โ๐) โ 1)
โ โ) |
112 | | lttr 11290 |
. . . . . . . . . . . 12
โข ((-1
โ โ โง 0 โ โ โง ((2โ๐) โ 1) โ โ) โ ((-1
< 0 โง 0 < ((2โ๐) โ 1)) โ -1 < ((2โ๐) โ 1))) |
113 | 109, 110,
111, 112 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((-1 <
0 โง 0 < ((2โ๐)
โ 1)) โ -1 < ((2โ๐) โ 1))) |
114 | 108, 113 | mpan2d 693 |
. . . . . . . . . 10
โข (๐ โ โ โ (-1 <
0 โ -1 < ((2โ๐) โ 1))) |
115 | 101, 114 | mpi 20 |
. . . . . . . . 9
โข (๐ โ โ โ -1 <
((2โ๐) โ
1)) |
116 | 115 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ -1 < ((2โ๐)
โ 1)) |
117 | 100, 116 | eqbrtrd 5171 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (((๐ด โ 1) mod
(2โ๐)) โ (๐ด mod (2โ๐))) < ((2โ๐) โ 1)) |
118 | 2, 10 | modcld 13840 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (๐ด mod (2โ๐)) โ
โ) |
119 | | ltsubadd2b 47197 |
. . . . . . . 8
โข (((1
โ โ โง (2โ๐) โ โ) โง ((๐ด mod (2โ๐)) โ โ โง ((๐ด โ 1) mod (2โ๐)) โ โ)) โ ((((๐ด โ 1) mod (2โ๐)) โ (๐ด mod (2โ๐))) < ((2โ๐) โ 1) โ (1 + ((๐ด โ 1) mod (2โ๐))) < ((2โ๐) + (๐ด mod (2โ๐))))) |
120 | 18, 8, 118, 16, 119 | syl22anc 838 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((((๐ด โ 1) mod
(2โ๐)) โ (๐ด mod (2โ๐))) < ((2โ๐) โ 1) โ (1 + ((๐ด โ 1) mod (2โ๐))) < ((2โ๐) + (๐ด mod (2โ๐))))) |
121 | 117, 120 | mpbid 231 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (1 + ((๐ด โ 1)
mod (2โ๐))) <
((2โ๐) + (๐ด mod (2โ๐)))) |
122 | | modid0 13862 |
. . . . . . . . . . . 12
โข
((2โ๐) โ
โ+ โ ((2โ๐) mod (2โ๐)) = 0) |
123 | 10, 122 | syl 17 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((2โ๐) mod
(2โ๐)) =
0) |
124 | 123 | oveq2d 7425 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด mod
(2โ๐)) โ
((2โ๐) mod
(2โ๐))) = ((๐ด mod (2โ๐)) โ 0)) |
125 | 118 | recnd 11242 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (๐ด mod (2โ๐)) โ
โ) |
126 | 125 | subid1d 11560 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด mod
(2โ๐)) โ 0) =
(๐ด mod (2โ๐))) |
127 | 124, 126 | eqtrd 2773 |
. . . . . . . . 9
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด mod
(2โ๐)) โ
((2โ๐) mod
(2โ๐))) = (๐ด mod (2โ๐))) |
128 | 127 | oveq1d 7424 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (((๐ด mod
(2โ๐)) โ
((2โ๐) mod
(2โ๐))) mod
(2โ๐)) = ((๐ด mod (2โ๐)) mod (2โ๐))) |
129 | | modsubmodmod 13895 |
. . . . . . . . 9
โข ((๐ด โ โ โง
(2โ๐) โ โ
โง (2โ๐) โ
โ+) โ (((๐ด mod (2โ๐)) โ ((2โ๐) mod (2โ๐))) mod (2โ๐)) = ((๐ด โ (2โ๐)) mod (2โ๐))) |
130 | 2, 8, 10, 129 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (((๐ด mod
(2โ๐)) โ
((2โ๐) mod
(2โ๐))) mod
(2โ๐)) = ((๐ด โ (2โ๐)) mod (2โ๐))) |
131 | | modabs2 13870 |
. . . . . . . . 9
โข ((๐ด โ โ โง
(2โ๐) โ
โ+) โ ((๐ด mod (2โ๐)) mod (2โ๐)) = (๐ด mod (2โ๐))) |
132 | 2, 10, 131 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด mod
(2โ๐)) mod
(2โ๐)) = (๐ด mod (2โ๐))) |
133 | 128, 130,
132 | 3eqtr3d 2781 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ
(2โ๐)) mod
(2โ๐)) = (๐ด mod (2โ๐))) |
134 | 133 | oveq2d 7425 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((2โ๐) +
((๐ด โ (2โ๐)) mod (2โ๐))) = ((2โ๐) + (๐ด mod (2โ๐)))) |
135 | 121, 134 | breqtrrd 5177 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (1 + ((๐ด โ 1)
mod (2โ๐))) <
((2โ๐) + ((๐ด โ (2โ๐)) mod (2โ๐)))) |
136 | 19, 20, 2, 135 | ltsub2dd 11827 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (๐ด โ
((2โ๐) + ((๐ด โ (2โ๐)) mod (2โ๐)))) < (๐ด โ (1 + ((๐ด โ 1) mod (2โ๐))))) |
137 | 31 | 3ad2ant1 1134 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ๐ด โ
โ) |
138 | 8 | recnd 11242 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (2โ๐) โ
โ) |
139 | 11 | recnd 11242 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ
(2โ๐)) mod
(2โ๐)) โ
โ) |
140 | 137, 138,
139 | subsub4d 11602 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ
(2โ๐)) โ ((๐ด โ (2โ๐)) mod (2โ๐))) = (๐ด โ ((2โ๐) + ((๐ด โ (2โ๐)) mod (2โ๐))))) |
141 | | 1cnd 11209 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ 1 โ โ) |
142 | 16 | recnd 11242 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ 1) mod
(2โ๐)) โ
โ) |
143 | 137, 141,
142 | subsub4d 11602 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ 1)
โ ((๐ด โ 1) mod
(2โ๐))) = (๐ด โ (1 + ((๐ด โ 1) mod (2โ๐))))) |
144 | 136, 140,
143 | 3brtr4d 5181 |
. . 3
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ ((๐ด โ
(2โ๐)) โ ((๐ด โ (2โ๐)) mod (2โ๐))) < ((๐ด โ 1) โ ((๐ด โ 1) mod (2โ๐)))) |
145 | 12, 17, 10, 144 | ltdiv1dd 13073 |
. 2
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (((๐ด โ
(2โ๐)) โ ((๐ด โ (2โ๐)) mod (2โ๐))) / (2โ๐)) < (((๐ด โ 1) โ ((๐ด โ 1) mod (2โ๐))) / (2โ๐))) |
146 | 7 | recnd 11242 |
. . . . 5
โข (๐ โ โ โ
(2โ๐) โ
โ) |
147 | 146 | 3ad2ant3 1136 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (2โ๐) โ
โ) |
148 | 65 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 2 โ
0) |
149 | 77, 148, 5 | expne0d 14117 |
. . . . 5
โข (๐ โ โ โ
(2โ๐) โ
0) |
150 | 149 | 3ad2ant3 1136 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (2โ๐) โ
0) |
151 | | divsub1dir 47198 |
. . . . 5
โข ((๐ด โ โ โง
(2โ๐) โ โ
โง (2โ๐) โ 0)
โ ((๐ด / (2โ๐)) โ 1) = ((๐ด โ (2โ๐)) / (2โ๐))) |
152 | 151 | fveq2d 6896 |
. . . 4
โข ((๐ด โ โ โง
(2โ๐) โ โ
โง (2โ๐) โ 0)
โ (โโ((๐ด /
(2โ๐)) โ 1)) =
(โโ((๐ด โ
(2โ๐)) / (2โ๐)))) |
153 | 137, 147,
150, 152 | syl3anc 1372 |
. . 3
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (โโ((๐ด /
(2โ๐)) โ 1)) =
(โโ((๐ด โ
(2โ๐)) / (2โ๐)))) |
154 | | fldivmod 47204 |
. . . 4
โข (((๐ด โ (2โ๐)) โ โ โง
(2โ๐) โ
โ+) โ (โโ((๐ด โ (2โ๐)) / (2โ๐))) = (((๐ด โ (2โ๐)) โ ((๐ด โ (2โ๐)) mod (2โ๐))) / (2โ๐))) |
155 | 9, 10, 154 | syl2anc 585 |
. . 3
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (โโ((๐ด
โ (2โ๐)) /
(2โ๐))) = (((๐ด โ (2โ๐)) โ ((๐ด โ (2โ๐)) mod (2โ๐))) / (2โ๐))) |
156 | 153, 155 | eqtrd 2773 |
. 2
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (โโ((๐ด /
(2โ๐)) โ 1)) =
(((๐ด โ (2โ๐)) โ ((๐ด โ (2โ๐)) mod (2โ๐))) / (2โ๐))) |
157 | | fldivmod 47204 |
. . 3
โข (((๐ด โ 1) โ โ โง
(2โ๐) โ
โ+) โ (โโ((๐ด โ 1) / (2โ๐))) = (((๐ด โ 1) โ ((๐ด โ 1) mod (2โ๐))) / (2โ๐))) |
158 | 15, 10, 157 | syl2anc 585 |
. 2
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (โโ((๐ด
โ 1) / (2โ๐))) =
(((๐ด โ 1) โ
((๐ด โ 1) mod
(2โ๐))) /
(2โ๐))) |
159 | 145, 156,
158 | 3brtr4d 5181 |
1
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ โ)
โ (โโ((๐ด /
(2โ๐)) โ 1))
< (โโ((๐ด
โ 1) / (2โ๐)))) |