Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β π΄ β
β€) |
2 | | 2nn 12231 |
. . . . . . . 8
β’ 2 β
β |
3 | 2 | a1i 11 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β0)
β 2 β β) |
4 | | simpr 486 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β0)
β π β
β0) |
5 | 3, 4 | nnexpcld 14154 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β (2βπ) β
β) |
6 | 1, 5 | zmodcld 13803 |
. . . . 5
β’ ((π΄ β β€ β§ π β β0)
β (π΄ mod (2βπ)) β
β0) |
7 | 6 | nn0zd 12530 |
. . . 4
β’ ((π΄ β β€ β§ π β β0)
β (π΄ mod (2βπ)) β
β€) |
8 | 7 | znegcld 12614 |
. . 3
β’ ((π΄ β β€ β§ π β β0)
β -(π΄ mod
(2βπ)) β
β€) |
9 | | sadadd 16352 |
. . 3
β’ ((-(π΄ mod (2βπ)) β β€ β§ π΄ β β€) β ((bitsβ-(π΄ mod (2βπ))) sadd (bitsβπ΄)) = (bitsβ(-(π΄ mod (2βπ)) + π΄))) |
10 | 8, 1, 9 | syl2anc 585 |
. 2
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβ-(π΄ mod
(2βπ))) sadd
(bitsβπ΄)) =
(bitsβ(-(π΄ mod
(2βπ)) + π΄))) |
11 | | sadadd 16352 |
. . . . . 6
β’ ((-(π΄ mod (2βπ)) β β€ β§ (π΄ mod (2βπ)) β β€) β
((bitsβ-(π΄ mod
(2βπ))) sadd
(bitsβ(π΄ mod
(2βπ)))) =
(bitsβ(-(π΄ mod
(2βπ)) + (π΄ mod (2βπ))))) |
12 | 8, 7, 11 | syl2anc 585 |
. . . . 5
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβ-(π΄ mod
(2βπ))) sadd
(bitsβ(π΄ mod
(2βπ)))) =
(bitsβ(-(π΄ mod
(2βπ)) + (π΄ mod (2βπ))))) |
13 | 8 | zcnd 12613 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β0)
β -(π΄ mod
(2βπ)) β
β) |
14 | 7 | zcnd 12613 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β0)
β (π΄ mod (2βπ)) β
β) |
15 | 13, 14 | addcomd 11362 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β0)
β (-(π΄ mod
(2βπ)) + (π΄ mod (2βπ))) = ((π΄ mod (2βπ)) + -(π΄ mod (2βπ)))) |
16 | 14 | negidd 11507 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β0)
β ((π΄ mod
(2βπ)) + -(π΄ mod (2βπ))) = 0) |
17 | 15, 16 | eqtrd 2773 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β0)
β (-(π΄ mod
(2βπ)) + (π΄ mod (2βπ))) = 0) |
18 | 17 | fveq2d 6847 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β (bitsβ(-(π΄ mod
(2βπ)) + (π΄ mod (2βπ)))) = (bitsβ0)) |
19 | | 0bits 16324 |
. . . . . 6
β’
(bitsβ0) = β
|
20 | 18, 19 | eqtrdi 2789 |
. . . . 5
β’ ((π΄ β β€ β§ π β β0)
β (bitsβ(-(π΄ mod
(2βπ)) + (π΄ mod (2βπ)))) = β
) |
21 | 12, 20 | eqtrd 2773 |
. . . 4
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβ-(π΄ mod
(2βπ))) sadd
(bitsβ(π΄ mod
(2βπ)))) =
β
) |
22 | 21 | oveq1d 7373 |
. . 3
β’ ((π΄ β β€ β§ π β β0)
β (((bitsβ-(π΄
mod (2βπ))) sadd
(bitsβ(π΄ mod
(2βπ)))) sadd
((bitsβπ΄) β©
(β€β₯βπ))) = (β
sadd ((bitsβπ΄) β©
(β€β₯βπ)))) |
23 | | bitsss 16311 |
. . . . 5
β’
(bitsβ-(π΄ mod
(2βπ))) β
β0 |
24 | | bitsss 16311 |
. . . . 5
β’
(bitsβ(π΄ mod
(2βπ))) β
β0 |
25 | | inss1 4189 |
. . . . . 6
β’
((bitsβπ΄)
β© (β€β₯βπ)) β (bitsβπ΄) |
26 | | bitsss 16311 |
. . . . . . 7
β’
(bitsβπ΄)
β β0 |
27 | 26 | a1i 11 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β (bitsβπ΄)
β β0) |
28 | 25, 27 | sstrid 3956 |
. . . . 5
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβπ΄)
β© (β€β₯βπ)) β
β0) |
29 | | sadass 16356 |
. . . . 5
β’
(((bitsβ-(π΄
mod (2βπ))) β
β0 β§ (bitsβ(π΄ mod (2βπ))) β β0 β§
((bitsβπ΄) β©
(β€β₯βπ)) β β0) β
(((bitsβ-(π΄ mod
(2βπ))) sadd
(bitsβ(π΄ mod
(2βπ)))) sadd
((bitsβπ΄) β©
(β€β₯βπ))) = ((bitsβ-(π΄ mod (2βπ))) sadd ((bitsβ(π΄ mod (2βπ))) sadd ((bitsβπ΄) β© (β€β₯βπ))))) |
30 | 23, 24, 28, 29 | mp3an12i 1466 |
. . . 4
β’ ((π΄ β β€ β§ π β β0)
β (((bitsβ-(π΄
mod (2βπ))) sadd
(bitsβ(π΄ mod
(2βπ)))) sadd
((bitsβπ΄) β©
(β€β₯βπ))) = ((bitsβ-(π΄ mod (2βπ))) sadd ((bitsβ(π΄ mod (2βπ))) sadd ((bitsβπ΄) β© (β€β₯βπ))))) |
31 | | bitsmod 16321 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β0)
β (bitsβ(π΄ mod
(2βπ))) =
((bitsβπ΄) β©
(0..^π))) |
32 | 31 | oveq1d 7373 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβ(π΄ mod
(2βπ))) sadd
((bitsβπ΄) β©
(β€β₯βπ))) = (((bitsβπ΄) β© (0..^π)) sadd ((bitsβπ΄) β© (β€β₯βπ)))) |
33 | | inss1 4189 |
. . . . . . . . . 10
β’
((bitsβπ΄)
β© (0..^π)) β
(bitsβπ΄) |
34 | 33, 27 | sstrid 3956 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβπ΄)
β© (0..^π)) β
β0) |
35 | | fzouzdisj 13614 |
. . . . . . . . . . . 12
β’
((0..^π) β©
(β€β₯βπ)) = β
|
36 | 35 | ineq2i 4170 |
. . . . . . . . . . 11
β’
((bitsβπ΄)
β© ((0..^π) β©
(β€β₯βπ))) = ((bitsβπ΄) β© β
) |
37 | | inindi 4187 |
. . . . . . . . . . 11
β’
((bitsβπ΄)
β© ((0..^π) β©
(β€β₯βπ))) = (((bitsβπ΄) β© (0..^π)) β© ((bitsβπ΄) β© (β€β₯βπ))) |
38 | | in0 4352 |
. . . . . . . . . . 11
β’
((bitsβπ΄)
β© β
) = β
|
39 | 36, 37, 38 | 3eqtr3i 2769 |
. . . . . . . . . 10
β’
(((bitsβπ΄)
β© (0..^π)) β©
((bitsβπ΄) β©
(β€β₯βπ))) = β
|
40 | 39 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β0)
β (((bitsβπ΄)
β© (0..^π)) β©
((bitsβπ΄) β©
(β€β₯βπ))) = β
) |
41 | 34, 28, 40 | saddisj 16350 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β0)
β (((bitsβπ΄)
β© (0..^π)) sadd
((bitsβπ΄) β©
(β€β₯βπ))) = (((bitsβπ΄) β© (0..^π)) βͺ ((bitsβπ΄) β© (β€β₯βπ)))) |
42 | | indi 4234 |
. . . . . . . 8
β’
((bitsβπ΄)
β© ((0..^π) βͺ
(β€β₯βπ))) = (((bitsβπ΄) β© (0..^π)) βͺ ((bitsβπ΄) β© (β€β₯βπ))) |
43 | 41, 42 | eqtr4di 2791 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β0)
β (((bitsβπ΄)
β© (0..^π)) sadd
((bitsβπ΄) β©
(β€β₯βπ))) = ((bitsβπ΄) β© ((0..^π) βͺ (β€β₯βπ)))) |
44 | | nn0uz 12810 |
. . . . . . . . . 10
β’
β0 = (β€β₯β0) |
45 | 4, 44 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ ((π΄ β β€ β§ π β β0)
β π β
(β€β₯β0)) |
46 | | fzouzsplit 13613 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β0) β (β€β₯β0) =
((0..^π) βͺ
(β€β₯βπ))) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ π β β0)
β (β€β₯β0) = ((0..^π) βͺ (β€β₯βπ))) |
48 | 44, 47 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β0)
β β0 = ((0..^π) βͺ (β€β₯βπ))) |
49 | 26, 48 | sseqtrid 3997 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β0)
β (bitsβπ΄)
β ((0..^π) βͺ
(β€β₯βπ))) |
50 | | df-ss 3928 |
. . . . . . . 8
β’
((bitsβπ΄)
β ((0..^π) βͺ
(β€β₯βπ)) β ((bitsβπ΄) β© ((0..^π) βͺ (β€β₯βπ))) = (bitsβπ΄)) |
51 | 49, 50 | sylib 217 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβπ΄)
β© ((0..^π) βͺ
(β€β₯βπ))) = (bitsβπ΄)) |
52 | 43, 51 | eqtrd 2773 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β (((bitsβπ΄)
β© (0..^π)) sadd
((bitsβπ΄) β©
(β€β₯βπ))) = (bitsβπ΄)) |
53 | 32, 52 | eqtrd 2773 |
. . . . 5
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβ(π΄ mod
(2βπ))) sadd
((bitsβπ΄) β©
(β€β₯βπ))) = (bitsβπ΄)) |
54 | 53 | oveq2d 7374 |
. . . 4
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβ-(π΄ mod
(2βπ))) sadd
((bitsβ(π΄ mod
(2βπ))) sadd
((bitsβπ΄) β©
(β€β₯βπ)))) = ((bitsβ-(π΄ mod (2βπ))) sadd (bitsβπ΄))) |
55 | 30, 54 | eqtrd 2773 |
. . 3
β’ ((π΄ β β€ β§ π β β0)
β (((bitsβ-(π΄
mod (2βπ))) sadd
(bitsβ(π΄ mod
(2βπ)))) sadd
((bitsβπ΄) β©
(β€β₯βπ))) = ((bitsβ-(π΄ mod (2βπ))) sadd (bitsβπ΄))) |
56 | | sadid2 16354 |
. . . 4
β’
(((bitsβπ΄)
β© (β€β₯βπ)) β β0 β
(β
sadd ((bitsβπ΄) β© (β€β₯βπ))) = ((bitsβπ΄) β©
(β€β₯βπ))) |
57 | 28, 56 | syl 17 |
. . 3
β’ ((π΄ β β€ β§ π β β0)
β (β
sadd ((bitsβπ΄) β© (β€β₯βπ))) = ((bitsβπ΄) β©
(β€β₯βπ))) |
58 | 22, 55, 57 | 3eqtr3d 2781 |
. 2
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβ-(π΄ mod
(2βπ))) sadd
(bitsβπ΄)) =
((bitsβπ΄) β©
(β€β₯βπ))) |
59 | 1 | zcnd 12613 |
. . . . 5
β’ ((π΄ β β€ β§ π β β0)
β π΄ β
β) |
60 | 13, 59 | addcomd 11362 |
. . . 4
β’ ((π΄ β β€ β§ π β β0)
β (-(π΄ mod
(2βπ)) + π΄) = (π΄ + -(π΄ mod (2βπ)))) |
61 | 59, 14 | negsubd 11523 |
. . . . 5
β’ ((π΄ β β€ β§ π β β0)
β (π΄ + -(π΄ mod (2βπ))) = (π΄ β (π΄ mod (2βπ)))) |
62 | 59, 14 | subcld 11517 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β (π΄ β (π΄ mod (2βπ))) β β) |
63 | 5 | nncnd 12174 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β (2βπ) β
β) |
64 | 5 | nnne0d 12208 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β (2βπ) β
0) |
65 | 62, 63, 64 | divcan1d 11937 |
. . . . 5
β’ ((π΄ β β€ β§ π β β0)
β (((π΄ β (π΄ mod (2βπ))) / (2βπ)) Β· (2βπ)) = (π΄ β (π΄ mod (2βπ)))) |
66 | 1 | zred 12612 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β0)
β π΄ β
β) |
67 | 5 | nnrpd 12960 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β0)
β (2βπ) β
β+) |
68 | | moddiffl 13793 |
. . . . . . 7
β’ ((π΄ β β β§
(2βπ) β
β+) β ((π΄ β (π΄ mod (2βπ))) / (2βπ)) = (ββ(π΄ / (2βπ)))) |
69 | 66, 67, 68 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β0)
β ((π΄ β (π΄ mod (2βπ))) / (2βπ)) = (ββ(π΄ / (2βπ)))) |
70 | 69 | oveq1d 7373 |
. . . . 5
β’ ((π΄ β β€ β§ π β β0)
β (((π΄ β (π΄ mod (2βπ))) / (2βπ)) Β· (2βπ)) = ((ββ(π΄ / (2βπ))) Β· (2βπ))) |
71 | 61, 65, 70 | 3eqtr2d 2779 |
. . . 4
β’ ((π΄ β β€ β§ π β β0)
β (π΄ + -(π΄ mod (2βπ))) = ((ββ(π΄ / (2βπ))) Β· (2βπ))) |
72 | 60, 71 | eqtrd 2773 |
. . 3
β’ ((π΄ β β€ β§ π β β0)
β (-(π΄ mod
(2βπ)) + π΄) = ((ββ(π΄ / (2βπ))) Β· (2βπ))) |
73 | 72 | fveq2d 6847 |
. 2
β’ ((π΄ β β€ β§ π β β0)
β (bitsβ(-(π΄ mod
(2βπ)) + π΄)) =
(bitsβ((ββ(π΄ / (2βπ))) Β· (2βπ)))) |
74 | 10, 58, 73 | 3eqtr3d 2781 |
1
β’ ((π΄ β β€ β§ π β β0)
β ((bitsβπ΄)
β© (β€β₯βπ)) = (bitsβ((ββ(π΄ / (2βπ))) Β· (2βπ)))) |