Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( A e. ZZ /\ N e. NN0 ) -> A e. ZZ ) |
2 |
|
2nn |
|- 2 e. NN |
3 |
2
|
a1i |
|- ( ( A e. ZZ /\ N e. NN0 ) -> 2 e. NN ) |
4 |
|
simpr |
|- ( ( A e. ZZ /\ N e. NN0 ) -> N e. NN0 ) |
5 |
3 4
|
nnexpcld |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. NN ) |
6 |
1 5
|
zmodcld |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A mod ( 2 ^ N ) ) e. NN0 ) |
7 |
6
|
nn0zd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A mod ( 2 ^ N ) ) e. ZZ ) |
8 |
7
|
znegcld |
|- ( ( A e. ZZ /\ N e. NN0 ) -> -u ( A mod ( 2 ^ N ) ) e. ZZ ) |
9 |
|
sadadd |
|- ( ( -u ( A mod ( 2 ^ N ) ) e. ZZ /\ A e. ZZ ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) = ( bits ` ( -u ( A mod ( 2 ^ N ) ) + A ) ) ) |
10 |
8 1 9
|
syl2anc |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) = ( bits ` ( -u ( A mod ( 2 ^ N ) ) + A ) ) ) |
11 |
|
sadadd |
|- ( ( -u ( A mod ( 2 ^ N ) ) e. ZZ /\ ( A mod ( 2 ^ N ) ) e. ZZ ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) = ( bits ` ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) ) ) |
12 |
8 7 11
|
syl2anc |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) = ( bits ` ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) ) ) |
13 |
8
|
zcnd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> -u ( A mod ( 2 ^ N ) ) e. CC ) |
14 |
7
|
zcnd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A mod ( 2 ^ N ) ) e. CC ) |
15 |
13 14
|
addcomd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) = ( ( A mod ( 2 ^ N ) ) + -u ( A mod ( 2 ^ N ) ) ) ) |
16 |
14
|
negidd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( A mod ( 2 ^ N ) ) + -u ( A mod ( 2 ^ N ) ) ) = 0 ) |
17 |
15 16
|
eqtrd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) = 0 ) |
18 |
17
|
fveq2d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) ) = ( bits ` 0 ) ) |
19 |
|
0bits |
|- ( bits ` 0 ) = (/) |
20 |
18 19
|
eqtrdi |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) ) = (/) ) |
21 |
12 20
|
eqtrd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) = (/) ) |
22 |
21
|
oveq1d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( (/) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) ) |
23 |
|
bitsss |
|- ( bits ` -u ( A mod ( 2 ^ N ) ) ) C_ NN0 |
24 |
|
bitsss |
|- ( bits ` ( A mod ( 2 ^ N ) ) ) C_ NN0 |
25 |
|
inss1 |
|- ( ( bits ` A ) i^i ( ZZ>= ` N ) ) C_ ( bits ` A ) |
26 |
|
bitsss |
|- ( bits ` A ) C_ NN0 |
27 |
26
|
a1i |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` A ) C_ NN0 ) |
28 |
25 27
|
sstrid |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( ZZ>= ` N ) ) C_ NN0 ) |
29 |
|
sadass |
|- ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) C_ NN0 /\ ( bits ` ( A mod ( 2 ^ N ) ) ) C_ NN0 /\ ( ( bits ` A ) i^i ( ZZ>= ` N ) ) C_ NN0 ) -> ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) ) ) |
30 |
23 24 28 29
|
mp3an12i |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) ) ) |
31 |
|
bitsmod |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` ( A mod ( 2 ^ N ) ) ) = ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) |
32 |
31
|
oveq1d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) ) |
33 |
|
inss1 |
|- ( ( bits ` A ) i^i ( 0 ..^ N ) ) C_ ( bits ` A ) |
34 |
33 27
|
sstrid |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( 0 ..^ N ) ) C_ NN0 ) |
35 |
|
fzouzdisj |
|- ( ( 0 ..^ N ) i^i ( ZZ>= ` N ) ) = (/) |
36 |
35
|
ineq2i |
|- ( ( bits ` A ) i^i ( ( 0 ..^ N ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` A ) i^i (/) ) |
37 |
|
inindi |
|- ( ( bits ` A ) i^i ( ( 0 ..^ N ) i^i ( ZZ>= ` N ) ) ) = ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) i^i ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) |
38 |
|
in0 |
|- ( ( bits ` A ) i^i (/) ) = (/) |
39 |
36 37 38
|
3eqtr3i |
|- ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) i^i ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = (/) |
40 |
39
|
a1i |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) i^i ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = (/) ) |
41 |
34 28 40
|
saddisj |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) u. ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) ) |
42 |
|
indi |
|- ( ( bits ` A ) i^i ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) = ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) u. ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) |
43 |
41 42
|
eqtr4di |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` A ) i^i ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) ) |
44 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
45 |
4 44
|
eleqtrdi |
|- ( ( A e. ZZ /\ N e. NN0 ) -> N e. ( ZZ>= ` 0 ) ) |
46 |
|
fzouzsplit |
|- ( N e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) |
47 |
45 46
|
syl |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) |
48 |
44 47
|
syl5eq |
|- ( ( A e. ZZ /\ N e. NN0 ) -> NN0 = ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) |
49 |
26 48
|
sseqtrid |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` A ) C_ ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) |
50 |
|
df-ss |
|- ( ( bits ` A ) C_ ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) <-> ( ( bits ` A ) i^i ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) = ( bits ` A ) ) |
51 |
49 50
|
sylib |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) = ( bits ` A ) ) |
52 |
43 51
|
eqtrd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( bits ` A ) ) |
53 |
32 52
|
eqtrd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( bits ` A ) ) |
54 |
53
|
oveq2d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) ) = ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) ) |
55 |
30 54
|
eqtrd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) ) |
56 |
|
sadid2 |
|- ( ( ( bits ` A ) i^i ( ZZ>= ` N ) ) C_ NN0 -> ( (/) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) |
57 |
28 56
|
syl |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( (/) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) |
58 |
22 55 57
|
3eqtr3d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) = ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) |
59 |
1
|
zcnd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> A e. CC ) |
60 |
13 59
|
addcomd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( -u ( A mod ( 2 ^ N ) ) + A ) = ( A + -u ( A mod ( 2 ^ N ) ) ) ) |
61 |
59 14
|
negsubd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A + -u ( A mod ( 2 ^ N ) ) ) = ( A - ( A mod ( 2 ^ N ) ) ) ) |
62 |
59 14
|
subcld |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A - ( A mod ( 2 ^ N ) ) ) e. CC ) |
63 |
5
|
nncnd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. CC ) |
64 |
5
|
nnne0d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) =/= 0 ) |
65 |
62 63 64
|
divcan1d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) x. ( 2 ^ N ) ) = ( A - ( A mod ( 2 ^ N ) ) ) ) |
66 |
1
|
zred |
|- ( ( A e. ZZ /\ N e. NN0 ) -> A e. RR ) |
67 |
5
|
nnrpd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. RR+ ) |
68 |
|
moddiffl |
|- ( ( A e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) = ( |_ ` ( A / ( 2 ^ N ) ) ) ) |
69 |
66 67 68
|
syl2anc |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) = ( |_ ` ( A / ( 2 ^ N ) ) ) ) |
70 |
69
|
oveq1d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) x. ( 2 ^ N ) ) = ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) |
71 |
61 65 70
|
3eqtr2d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A + -u ( A mod ( 2 ^ N ) ) ) = ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) |
72 |
60 71
|
eqtrd |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( -u ( A mod ( 2 ^ N ) ) + A ) = ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) |
73 |
72
|
fveq2d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` ( -u ( A mod ( 2 ^ N ) ) + A ) ) = ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) ) |
74 |
10 58 73
|
3eqtr3d |
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( ZZ>= ` N ) ) = ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) ) |