Database
ELEMENTARY NUMBER THEORY
Elementary properties of divisibility
Bit sequences
smumullem
Next ⟩
smumul
Metamath Proof Explorer
Ascii
Unicode
Theorem
smumullem
Description:
Lemma for
smumul
.
(Contributed by
Mario Carneiro
, 22-Sep-2016)
Ref
Expression
Hypotheses
smumullem.a
⊢
φ
→
A
∈
ℤ
smumullem.b
⊢
φ
→
B
∈
ℤ
smumullem.n
⊢
φ
→
N
∈
ℕ
0
Assertion
smumullem
⊢
φ
→
bits
A
∩
0
..^
N
smul
bits
B
=
bits
A
mod
2
N
B
Proof
Step
Hyp
Ref
Expression
1
smumullem.a
⊢
φ
→
A
∈
ℤ
2
smumullem.b
⊢
φ
→
B
∈
ℤ
3
smumullem.n
⊢
φ
→
N
∈
ℕ
0
4
oveq2
⊢
x
=
0
→
0
..^
x
=
0
..^
0
5
fzo0
⊢
0
..^
0
=
∅
6
4
5
eqtrdi
⊢
x
=
0
→
0
..^
x
=
∅
7
6
ineq2d
⊢
x
=
0
→
bits
A
∩
0
..^
x
=
bits
A
∩
∅
8
in0
⊢
bits
A
∩
∅
=
∅
9
7
8
eqtrdi
⊢
x
=
0
→
bits
A
∩
0
..^
x
=
∅
10
9
oveq1d
⊢
x
=
0
→
bits
A
∩
0
..^
x
smul
bits
B
=
∅
smul
bits
B
11
bitsss
⊢
bits
B
⊆
ℕ
0
12
smu02
⊢
bits
B
⊆
ℕ
0
→
∅
smul
bits
B
=
∅
13
11
12
ax-mp
⊢
∅
smul
bits
B
=
∅
14
10
13
eqtrdi
⊢
x
=
0
→
bits
A
∩
0
..^
x
smul
bits
B
=
∅
15
oveq2
⊢
x
=
0
→
2
x
=
2
0
16
2cn
⊢
2
∈
ℂ
17
exp0
⊢
2
∈
ℂ
→
2
0
=
1
18
16
17
ax-mp
⊢
2
0
=
1
19
15
18
eqtrdi
⊢
x
=
0
→
2
x
=
1
20
19
oveq2d
⊢
x
=
0
→
A
mod
2
x
=
A
mod
1
21
20
fvoveq1d
⊢
x
=
0
→
bits
A
mod
2
x
B
=
bits
A
mod
1
B
22
14
21
eqeq12d
⊢
x
=
0
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
mod
2
x
B
↔
∅
=
bits
A
mod
1
B
23
22
imbi2d
⊢
x
=
0
→
φ
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
mod
2
x
B
↔
φ
→
∅
=
bits
A
mod
1
B
24
oveq2
⊢
x
=
k
→
0
..^
x
=
0
..^
k
25
24
ineq2d
⊢
x
=
k
→
bits
A
∩
0
..^
x
=
bits
A
∩
0
..^
k
26
25
oveq1d
⊢
x
=
k
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
∩
0
..^
k
smul
bits
B
27
oveq2
⊢
x
=
k
→
2
x
=
2
k
28
27
oveq2d
⊢
x
=
k
→
A
mod
2
x
=
A
mod
2
k
29
28
fvoveq1d
⊢
x
=
k
→
bits
A
mod
2
x
B
=
bits
A
mod
2
k
B
30
26
29
eqeq12d
⊢
x
=
k
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
mod
2
x
B
↔
bits
A
∩
0
..^
k
smul
bits
B
=
bits
A
mod
2
k
B
31
30
imbi2d
⊢
x
=
k
→
φ
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
mod
2
x
B
↔
φ
→
bits
A
∩
0
..^
k
smul
bits
B
=
bits
A
mod
2
k
B
32
oveq2
⊢
x
=
k
+
1
→
0
..^
x
=
0
..^
k
+
1
33
32
ineq2d
⊢
x
=
k
+
1
→
bits
A
∩
0
..^
x
=
bits
A
∩
0
..^
k
+
1
34
33
oveq1d
⊢
x
=
k
+
1
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
∩
0
..^
k
+
1
smul
bits
B
35
oveq2
⊢
x
=
k
+
1
→
2
x
=
2
k
+
1
36
35
oveq2d
⊢
x
=
k
+
1
→
A
mod
2
x
=
A
mod
2
k
+
1
37
36
fvoveq1d
⊢
x
=
k
+
1
→
bits
A
mod
2
x
B
=
bits
A
mod
2
k
+
1
B
38
34
37
eqeq12d
⊢
x
=
k
+
1
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
mod
2
x
B
↔
bits
A
∩
0
..^
k
+
1
smul
bits
B
=
bits
A
mod
2
k
+
1
B
39
38
imbi2d
⊢
x
=
k
+
1
→
φ
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
mod
2
x
B
↔
φ
→
bits
A
∩
0
..^
k
+
1
smul
bits
B
=
bits
A
mod
2
k
+
1
B
40
oveq2
⊢
x
=
N
→
0
..^
x
=
0
..^
N
41
40
ineq2d
⊢
x
=
N
→
bits
A
∩
0
..^
x
=
bits
A
∩
0
..^
N
42
41
oveq1d
⊢
x
=
N
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
∩
0
..^
N
smul
bits
B
43
oveq2
⊢
x
=
N
→
2
x
=
2
N
44
43
oveq2d
⊢
x
=
N
→
A
mod
2
x
=
A
mod
2
N
45
44
fvoveq1d
⊢
x
=
N
→
bits
A
mod
2
x
B
=
bits
A
mod
2
N
B
46
42
45
eqeq12d
⊢
x
=
N
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
mod
2
x
B
↔
bits
A
∩
0
..^
N
smul
bits
B
=
bits
A
mod
2
N
B
47
46
imbi2d
⊢
x
=
N
→
φ
→
bits
A
∩
0
..^
x
smul
bits
B
=
bits
A
mod
2
x
B
↔
φ
→
bits
A
∩
0
..^
N
smul
bits
B
=
bits
A
mod
2
N
B
48
zmod10
⊢
A
∈
ℤ
→
A
mod
1
=
0
49
1
48
syl
⊢
φ
→
A
mod
1
=
0
50
49
oveq1d
⊢
φ
→
A
mod
1
B
=
0
⋅
B
51
2
zcnd
⊢
φ
→
B
∈
ℂ
52
51
mul02d
⊢
φ
→
0
⋅
B
=
0
53
50
52
eqtrd
⊢
φ
→
A
mod
1
B
=
0
54
53
fveq2d
⊢
φ
→
bits
A
mod
1
B
=
bits
0
55
0bits
⊢
bits
0
=
∅
56
54
55
eqtr2di
⊢
φ
→
∅
=
bits
A
mod
1
B
57
oveq1
⊢
bits
A
∩
0
..^
k
smul
bits
B
=
bits
A
mod
2
k
B
→
bits
A
∩
0
..^
k
smul
bits
B
sadd
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
=
bits
A
mod
2
k
B
sadd
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
58
bitsss
⊢
bits
A
⊆
ℕ
0
59
58
a1i
⊢
φ
∧
k
∈
ℕ
0
→
bits
A
⊆
ℕ
0
60
11
a1i
⊢
φ
∧
k
∈
ℕ
0
→
bits
B
⊆
ℕ
0
61
simpr
⊢
φ
∧
k
∈
ℕ
0
→
k
∈
ℕ
0
62
59
60
61
smup1
⊢
φ
∧
k
∈
ℕ
0
→
bits
A
∩
0
..^
k
+
1
smul
bits
B
=
bits
A
∩
0
..^
k
smul
bits
B
sadd
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
63
bitsinv1lem
⊢
A
∈
ℤ
∧
k
∈
ℕ
0
→
A
mod
2
k
+
1
=
A
mod
2
k
+
if
k
∈
bits
A
2
k
0
64
1
63
sylan
⊢
φ
∧
k
∈
ℕ
0
→
A
mod
2
k
+
1
=
A
mod
2
k
+
if
k
∈
bits
A
2
k
0
65
64
oveq1d
⊢
φ
∧
k
∈
ℕ
0
→
A
mod
2
k
+
1
B
=
A
mod
2
k
+
if
k
∈
bits
A
2
k
0
B
66
1
adantr
⊢
φ
∧
k
∈
ℕ
0
→
A
∈
ℤ
67
2nn
⊢
2
∈
ℕ
68
67
a1i
⊢
φ
∧
k
∈
ℕ
0
→
2
∈
ℕ
69
68
61
nnexpcld
⊢
φ
∧
k
∈
ℕ
0
→
2
k
∈
ℕ
70
66
69
zmodcld
⊢
φ
∧
k
∈
ℕ
0
→
A
mod
2
k
∈
ℕ
0
71
70
nn0cnd
⊢
φ
∧
k
∈
ℕ
0
→
A
mod
2
k
∈
ℂ
72
69
nnnn0d
⊢
φ
∧
k
∈
ℕ
0
→
2
k
∈
ℕ
0
73
0nn0
⊢
0
∈
ℕ
0
74
ifcl
⊢
2
k
∈
ℕ
0
∧
0
∈
ℕ
0
→
if
k
∈
bits
A
2
k
0
∈
ℕ
0
75
72
73
74
sylancl
⊢
φ
∧
k
∈
ℕ
0
→
if
k
∈
bits
A
2
k
0
∈
ℕ
0
76
75
nn0cnd
⊢
φ
∧
k
∈
ℕ
0
→
if
k
∈
bits
A
2
k
0
∈
ℂ
77
51
adantr
⊢
φ
∧
k
∈
ℕ
0
→
B
∈
ℂ
78
71
76
77
adddird
⊢
φ
∧
k
∈
ℕ
0
→
A
mod
2
k
+
if
k
∈
bits
A
2
k
0
B
=
A
mod
2
k
B
+
if
k
∈
bits
A
2
k
0
B
79
76
77
mulcomd
⊢
φ
∧
k
∈
ℕ
0
→
if
k
∈
bits
A
2
k
0
B
=
B
if
k
∈
bits
A
2
k
0
80
79
oveq2d
⊢
φ
∧
k
∈
ℕ
0
→
A
mod
2
k
B
+
if
k
∈
bits
A
2
k
0
B
=
A
mod
2
k
B
+
B
if
k
∈
bits
A
2
k
0
81
65
78
80
3eqtrd
⊢
φ
∧
k
∈
ℕ
0
→
A
mod
2
k
+
1
B
=
A
mod
2
k
B
+
B
if
k
∈
bits
A
2
k
0
82
81
fveq2d
⊢
φ
∧
k
∈
ℕ
0
→
bits
A
mod
2
k
+
1
B
=
bits
A
mod
2
k
B
+
B
if
k
∈
bits
A
2
k
0
83
70
nn0zd
⊢
φ
∧
k
∈
ℕ
0
→
A
mod
2
k
∈
ℤ
84
2
adantr
⊢
φ
∧
k
∈
ℕ
0
→
B
∈
ℤ
85
83
84
zmulcld
⊢
φ
∧
k
∈
ℕ
0
→
A
mod
2
k
B
∈
ℤ
86
75
nn0zd
⊢
φ
∧
k
∈
ℕ
0
→
if
k
∈
bits
A
2
k
0
∈
ℤ
87
84
86
zmulcld
⊢
φ
∧
k
∈
ℕ
0
→
B
if
k
∈
bits
A
2
k
0
∈
ℤ
88
sadadd
⊢
A
mod
2
k
B
∈
ℤ
∧
B
if
k
∈
bits
A
2
k
0
∈
ℤ
→
bits
A
mod
2
k
B
sadd
bits
B
if
k
∈
bits
A
2
k
0
=
bits
A
mod
2
k
B
+
B
if
k
∈
bits
A
2
k
0
89
85
87
88
syl2anc
⊢
φ
∧
k
∈
ℕ
0
→
bits
A
mod
2
k
B
sadd
bits
B
if
k
∈
bits
A
2
k
0
=
bits
A
mod
2
k
B
+
B
if
k
∈
bits
A
2
k
0
90
oveq2
⊢
2
k
=
if
k
∈
bits
A
2
k
0
→
B
2
k
=
B
if
k
∈
bits
A
2
k
0
91
90
fveqeq2d
⊢
2
k
=
if
k
∈
bits
A
2
k
0
→
bits
B
2
k
=
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
↔
bits
B
if
k
∈
bits
A
2
k
0
=
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
92
oveq2
⊢
0
=
if
k
∈
bits
A
2
k
0
→
B
⋅
0
=
B
if
k
∈
bits
A
2
k
0
93
92
fveqeq2d
⊢
0
=
if
k
∈
bits
A
2
k
0
→
bits
B
⋅
0
=
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
↔
bits
B
if
k
∈
bits
A
2
k
0
=
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
94
bitsshft
⊢
B
∈
ℤ
∧
k
∈
ℕ
0
→
n
∈
ℕ
0
|
n
−
k
∈
bits
B
=
bits
B
2
k
95
2
94
sylan
⊢
φ
∧
k
∈
ℕ
0
→
n
∈
ℕ
0
|
n
−
k
∈
bits
B
=
bits
B
2
k
96
ibar
⊢
k
∈
bits
A
→
n
−
k
∈
bits
B
↔
k
∈
bits
A
∧
n
−
k
∈
bits
B
97
96
rabbidv
⊢
k
∈
bits
A
→
n
∈
ℕ
0
|
n
−
k
∈
bits
B
=
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
98
95
97
sylan9req
⊢
φ
∧
k
∈
ℕ
0
∧
k
∈
bits
A
→
bits
B
2
k
=
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
99
77
adantr
⊢
φ
∧
k
∈
ℕ
0
∧
¬
k
∈
bits
A
→
B
∈
ℂ
100
99
mul01d
⊢
φ
∧
k
∈
ℕ
0
∧
¬
k
∈
bits
A
→
B
⋅
0
=
0
101
100
fveq2d
⊢
φ
∧
k
∈
ℕ
0
∧
¬
k
∈
bits
A
→
bits
B
⋅
0
=
bits
0
102
simpr
⊢
φ
∧
k
∈
ℕ
0
∧
¬
k
∈
bits
A
→
¬
k
∈
bits
A
103
102
intnanrd
⊢
φ
∧
k
∈
ℕ
0
∧
¬
k
∈
bits
A
→
¬
k
∈
bits
A
∧
n
−
k
∈
bits
B
104
103
ralrimivw
⊢
φ
∧
k
∈
ℕ
0
∧
¬
k
∈
bits
A
→
∀
n
∈
ℕ
0
¬
k
∈
bits
A
∧
n
−
k
∈
bits
B
105
rabeq0
⊢
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
=
∅
↔
∀
n
∈
ℕ
0
¬
k
∈
bits
A
∧
n
−
k
∈
bits
B
106
104
105
sylibr
⊢
φ
∧
k
∈
ℕ
0
∧
¬
k
∈
bits
A
→
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
=
∅
107
55
101
106
3eqtr4a
⊢
φ
∧
k
∈
ℕ
0
∧
¬
k
∈
bits
A
→
bits
B
⋅
0
=
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
108
91
93
98
107
ifbothda
⊢
φ
∧
k
∈
ℕ
0
→
bits
B
if
k
∈
bits
A
2
k
0
=
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
109
108
oveq2d
⊢
φ
∧
k
∈
ℕ
0
→
bits
A
mod
2
k
B
sadd
bits
B
if
k
∈
bits
A
2
k
0
=
bits
A
mod
2
k
B
sadd
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
110
82
89
109
3eqtr2d
⊢
φ
∧
k
∈
ℕ
0
→
bits
A
mod
2
k
+
1
B
=
bits
A
mod
2
k
B
sadd
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
111
62
110
eqeq12d
⊢
φ
∧
k
∈
ℕ
0
→
bits
A
∩
0
..^
k
+
1
smul
bits
B
=
bits
A
mod
2
k
+
1
B
↔
bits
A
∩
0
..^
k
smul
bits
B
sadd
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
=
bits
A
mod
2
k
B
sadd
n
∈
ℕ
0
|
k
∈
bits
A
∧
n
−
k
∈
bits
B
112
57
111
syl5ibr
⊢
φ
∧
k
∈
ℕ
0
→
bits
A
∩
0
..^
k
smul
bits
B
=
bits
A
mod
2
k
B
→
bits
A
∩
0
..^
k
+
1
smul
bits
B
=
bits
A
mod
2
k
+
1
B
113
112
expcom
⊢
k
∈
ℕ
0
→
φ
→
bits
A
∩
0
..^
k
smul
bits
B
=
bits
A
mod
2
k
B
→
bits
A
∩
0
..^
k
+
1
smul
bits
B
=
bits
A
mod
2
k
+
1
B
114
113
a2d
⊢
k
∈
ℕ
0
→
φ
→
bits
A
∩
0
..^
k
smul
bits
B
=
bits
A
mod
2
k
B
→
φ
→
bits
A
∩
0
..^
k
+
1
smul
bits
B
=
bits
A
mod
2
k
+
1
B
115
23
31
39
47
56
114
nn0ind
⊢
N
∈
ℕ
0
→
φ
→
bits
A
∩
0
..^
N
smul
bits
B
=
bits
A
mod
2
N
B
116
3
115
mpcom
⊢
φ
→
bits
A
∩
0
..^
N
smul
bits
B
=
bits
A
mod
2
N
B