Step | Hyp | Ref
| Expression |
1 | | nnre 12249 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
2 | | 2nn 12315 |
. . . . . . . 8
โข 2 โ
โ |
3 | 2 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 2 โ
โ) |
4 | | blennnelnn 47761 |
. . . . . . . 8
โข (๐ โ โ โ
(#bโ๐)
โ โ) |
5 | | nnm1nn0 12543 |
. . . . . . . 8
โข
((#bโ๐) โ โ โ
((#bโ๐)
โ 1) โ โ0) |
6 | 4, 5 | syl 17 |
. . . . . . 7
โข (๐ โ โ โ
((#bโ๐)
โ 1) โ โ0) |
7 | 3, 6 | nnexpcld 14239 |
. . . . . 6
โข (๐ โ โ โ
(2โ((#bโ๐) โ 1)) โ
โ) |
8 | 7 | nnrpd 13046 |
. . . . 5
โข (๐ โ โ โ
(2โ((#bโ๐) โ 1)) โ
โ+) |
9 | | modeqmodmin 13938 |
. . . . 5
โข ((๐ โ โ โง
(2โ((#bโ๐) โ 1)) โ โ+)
โ (๐ mod
(2โ((#bโ๐) โ 1))) = ((๐ โ (2โ((#bโ๐) โ 1))) mod
(2โ((#bโ๐) โ 1)))) |
10 | 1, 8, 9 | syl2anc 582 |
. . . 4
โข (๐ โ โ โ (๐ mod
(2โ((#bโ๐) โ 1))) = ((๐ โ (2โ((#bโ๐) โ 1))) mod
(2โ((#bโ๐) โ 1)))) |
11 | 7 | nnred 12257 |
. . . . . 6
โข (๐ โ โ โ
(2โ((#bโ๐) โ 1)) โ
โ) |
12 | 1, 11 | resubcld 11672 |
. . . . 5
โข (๐ โ โ โ (๐ โ
(2โ((#bโ๐) โ 1))) โ
โ) |
13 | | nnpw2blen 47765 |
. . . . . 6
โข (๐ โ โ โ
((2โ((#bโ๐) โ 1)) โค ๐ โง ๐ < (2โ(#bโ๐)))) |
14 | 1, 11 | subge0d 11834 |
. . . . . . 7
โข (๐ โ โ โ (0 โค
(๐ โ
(2โ((#bโ๐) โ 1))) โ
(2โ((#bโ๐) โ 1)) โค ๐)) |
15 | 1, 11, 11 | ltsubadd2d 11842 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ โ
(2โ((#bโ๐) โ 1))) <
(2โ((#bโ๐) โ 1)) โ ๐ < ((2โ((#bโ๐) โ 1)) +
(2โ((#bโ๐) โ 1))))) |
16 | | 2cn 12317 |
. . . . . . . . . . . 12
โข 2 โ
โ |
17 | | exp1 14064 |
. . . . . . . . . . . . 13
โข (2 โ
โ โ (2โ1) = 2) |
18 | 17 | eqcomd 2731 |
. . . . . . . . . . . 12
โข (2 โ
โ โ 2 = (2โ1)) |
19 | 16, 18 | mp1i 13 |
. . . . . . . . . . 11
โข (๐ โ โ โ 2 =
(2โ1)) |
20 | 19 | oveq1d 7431 |
. . . . . . . . . 10
โข (๐ โ โ โ (2
ยท (2โ((#bโ๐) โ 1))) = ((2โ1) ยท
(2โ((#bโ๐) โ 1)))) |
21 | 7 | nncnd 12258 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(2โ((#bโ๐) โ 1)) โ
โ) |
22 | 21 | 2timesd 12485 |
. . . . . . . . . 10
โข (๐ โ โ โ (2
ยท (2โ((#bโ๐) โ 1))) =
((2โ((#bโ๐) โ 1)) +
(2โ((#bโ๐) โ 1)))) |
23 | 16 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 2 โ
โ) |
24 | | 1nn0 12518 |
. . . . . . . . . . . . 13
โข 1 โ
โ0 |
25 | 24 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 1 โ
โ0) |
26 | 23, 6, 25 | expaddd 14144 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(2โ(1 + ((#bโ๐) โ 1))) = ((2โ1) ยท
(2โ((#bโ๐) โ 1)))) |
27 | | 1cnd 11239 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 1 โ
โ) |
28 | 4 | nncnd 12258 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(#bโ๐)
โ โ) |
29 | 27, 28 | pncan3d 11604 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1 +
((#bโ๐)
โ 1)) = (#bโ๐)) |
30 | 29 | oveq2d 7432 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(2โ(1 + ((#bโ๐) โ 1))) =
(2โ(#bโ๐))) |
31 | 26, 30 | eqtr3d 2767 |
. . . . . . . . . 10
โข (๐ โ โ โ
((2โ1) ยท (2โ((#bโ๐) โ 1))) =
(2โ(#bโ๐))) |
32 | 20, 22, 31 | 3eqtr3d 2773 |
. . . . . . . . 9
โข (๐ โ โ โ
((2โ((#bโ๐) โ 1)) +
(2โ((#bโ๐) โ 1))) =
(2โ(#bโ๐))) |
33 | 32 | breq2d 5155 |
. . . . . . . 8
โข (๐ โ โ โ (๐ <
((2โ((#bโ๐) โ 1)) +
(2โ((#bโ๐) โ 1))) โ ๐ < (2โ(#bโ๐)))) |
34 | 15, 33 | bitrd 278 |
. . . . . . 7
โข (๐ โ โ โ ((๐ โ
(2โ((#bโ๐) โ 1))) <
(2โ((#bโ๐) โ 1)) โ ๐ < (2โ(#bโ๐)))) |
35 | 14, 34 | anbi12d 630 |
. . . . . 6
โข (๐ โ โ โ ((0 โค
(๐ โ
(2โ((#bโ๐) โ 1))) โง (๐ โ (2โ((#bโ๐) โ 1))) <
(2โ((#bโ๐) โ 1))) โ
((2โ((#bโ๐) โ 1)) โค ๐ โง ๐ < (2โ(#bโ๐))))) |
36 | 13, 35 | mpbird 256 |
. . . . 5
โข (๐ โ โ โ (0 โค
(๐ โ
(2โ((#bโ๐) โ 1))) โง (๐ โ (2โ((#bโ๐) โ 1))) <
(2โ((#bโ๐) โ 1)))) |
37 | | modid 13893 |
. . . . 5
โข ((((๐ โ
(2โ((#bโ๐) โ 1))) โ โ โง
(2โ((#bโ๐) โ 1)) โ โ+)
โง (0 โค (๐ โ
(2โ((#bโ๐) โ 1))) โง (๐ โ (2โ((#bโ๐) โ 1))) <
(2โ((#bโ๐) โ 1)))) โ ((๐ โ (2โ((#bโ๐) โ 1))) mod
(2โ((#bโ๐) โ 1))) = (๐ โ (2โ((#bโ๐) โ 1)))) |
38 | 12, 8, 36, 37 | syl21anc 836 |
. . . 4
โข (๐ โ โ โ ((๐ โ
(2โ((#bโ๐) โ 1))) mod
(2โ((#bโ๐) โ 1))) = (๐ โ (2โ((#bโ๐) โ 1)))) |
39 | 10, 38 | eqtr2d 2766 |
. . 3
โข (๐ โ โ โ (๐ โ
(2โ((#bโ๐) โ 1))) = (๐ mod (2โ((#bโ๐) โ 1)))) |
40 | | nncn 12250 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ) |
41 | | nnz 12609 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
42 | 41, 7 | zmodcld 13889 |
. . . . 5
โข (๐ โ โ โ (๐ mod
(2โ((#bโ๐) โ 1))) โ
โ0) |
43 | 42 | nn0cnd 12564 |
. . . 4
โข (๐ โ โ โ (๐ mod
(2โ((#bโ๐) โ 1))) โ
โ) |
44 | 40, 21, 43 | subaddd 11619 |
. . 3
โข (๐ โ โ โ ((๐ โ
(2โ((#bโ๐) โ 1))) = (๐ mod (2โ((#bโ๐) โ 1))) โ
((2โ((#bโ๐) โ 1)) + (๐ mod (2โ((#bโ๐) โ 1)))) = ๐)) |
45 | 39, 44 | mpbid 231 |
. 2
โข (๐ โ โ โ
((2โ((#bโ๐) โ 1)) + (๐ mod (2โ((#bโ๐) โ 1)))) = ๐) |
46 | 45 | eqcomd 2731 |
1
โข (๐ โ โ โ ๐ =
((2โ((#bโ๐) โ 1)) + (๐ mod (2โ((#bโ๐) โ
1))))) |