Metamath Proof Explorer

Theorem smumullem

Description: Lemma for smumul . (Contributed by Mario Carneiro, 22-Sep-2016)

Ref Expression
Hypotheses smumullem.a ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
smumullem.b ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
smumullem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion smumullem ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 smumullem.a ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2 smumullem.b ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
3 smumullem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 oveq2 ⊢ ( 𝑥 = 0 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 0 ) )
5 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
6 4 5 eqtrdi ⊢ ( 𝑥 = 0 → ( 0 ..^ 𝑥 ) = ∅ )
7 6 ineq2d ⊢ ( 𝑥 = 0 → ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) = ( ( bits ‘ 𝐴 ) ∩ ∅ ) )
8 in0 ⊢ ( ( bits ‘ 𝐴 ) ∩ ∅ ) = ∅
9 7 8 eqtrdi ⊢ ( 𝑥 = 0 → ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) = ∅ )
10 9 oveq1d ⊢ ( 𝑥 = 0 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( ∅ smul ( bits ‘ 𝐵 ) ) )
11 bitsss ⊢ ( bits ‘ 𝐵 ) ⊆ ℕ0
12 smu02 ⊢ ( ( bits ‘ 𝐵 ) ⊆ ℕ0 → ( ∅ smul ( bits ‘ 𝐵 ) ) = ∅ )
13 11 12 ax-mp ⊢ ( ∅ smul ( bits ‘ 𝐵 ) ) = ∅
14 10 13 eqtrdi ⊢ ( 𝑥 = 0 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ∅ )
15 oveq2 ⊢ ( 𝑥 = 0 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 0 ) )
16 2cn ⊢ 2 ∈ ℂ
17 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
18 16 17 ax-mp ⊢ ( 2 ↑ 0 ) = 1
19 15 18 eqtrdi ⊢ ( 𝑥 = 0 → ( 2 ↑ 𝑥 ) = 1 )
20 19 oveq2d ⊢ ( 𝑥 = 0 → ( 𝐴 mod ( 2 ↑ 𝑥 ) ) = ( 𝐴 mod 1 ) )
21 20 fvoveq1d ⊢ ( 𝑥 = 0 → ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod 1 ) · 𝐵 ) ) )
22 14 21 eqeq12d ⊢ ( 𝑥 = 0 → ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) ↔ ∅ = ( bits ‘ ( ( 𝐴 mod 1 ) · 𝐵 ) ) ) )
23 22 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) ) ↔ ( 𝜑 → ∅ = ( bits ‘ ( ( 𝐴 mod 1 ) · 𝐵 ) ) ) ) )
24 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 𝑘 ) )
25 24 ineq2d ⊢ ( 𝑥 = 𝑘 → ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) = ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) )
26 25 oveq1d ⊢ ( 𝑥 = 𝑘 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) )
27 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝑘 ) )
28 27 oveq2d ⊢ ( 𝑥 = 𝑘 → ( 𝐴 mod ( 2 ↑ 𝑥 ) ) = ( 𝐴 mod ( 2 ↑ 𝑘 ) ) )
29 28 fvoveq1d ⊢ ( 𝑥 = 𝑘 → ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) )
30 26 29 eqeq12d ⊢ ( 𝑥 = 𝑘 → ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) ↔ ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) ) )
31 30 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) ) ↔ ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) ) ) )
32 oveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 0 ..^ 𝑥 ) = ( 0 ..^ ( 𝑘 + 1 ) ) )
33 32 ineq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) = ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) )
34 33 oveq1d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) smul ( bits ‘ 𝐵 ) ) )
35 oveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 2 ↑ 𝑥 ) = ( 2 ↑ ( 𝑘 + 1 ) ) )
36 35 oveq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐴 mod ( 2 ↑ 𝑥 ) ) = ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) )
37 36 fvoveq1d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) ) )
38 34 37 eqeq12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) ↔ ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) ) ) )
39 38 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) ) ↔ ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) ) ) ) )
40 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 𝑁 ) )
41 40 ineq2d ⊢ ( 𝑥 = 𝑁 → ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) = ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) )
42 41 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) smul ( bits ‘ 𝐵 ) ) )
43 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝑁 ) )
44 43 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝐴 mod ( 2 ↑ 𝑥 ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
45 44 fvoveq1d ⊢ ( 𝑥 = 𝑁 → ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) · 𝐵 ) ) )
46 42 45 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) ↔ ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) · 𝐵 ) ) ) )
47 46 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑥 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑥 ) ) · 𝐵 ) ) ) ↔ ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) · 𝐵 ) ) ) ) )
48 zmod10 ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 mod 1 ) = 0 )
49 1 48 syl ⊢ ( 𝜑 → ( 𝐴 mod 1 ) = 0 )
50 49 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 mod 1 ) · 𝐵 ) = ( 0 · 𝐵 ) )
51 2 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
52 51 mul02d ⊢ ( 𝜑 → ( 0 · 𝐵 ) = 0 )
53 50 52 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 mod 1 ) · 𝐵 ) = 0 )
54 53 fveq2d ⊢ ( 𝜑 → ( bits ‘ ( ( 𝐴 mod 1 ) · 𝐵 ) ) = ( bits ‘ 0 ) )
55 0bits ⊢ ( bits ‘ 0 ) = ∅
56 54 55 eqtr2di ⊢ ( 𝜑 → ∅ = ( bits ‘ ( ( 𝐴 mod 1 ) · 𝐵 ) ) )
57 oveq1 ⊢ ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) → ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ) = ( ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ) )
58 bitsss ⊢ ( bits ‘ 𝐴 ) ⊆ ℕ0
59 58 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( bits ‘ 𝐴 ) ⊆ ℕ0 )
60 11 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( bits ‘ 𝐵 ) ⊆ ℕ0 )
61 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
62 59 60 61 smup1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) smul ( bits ‘ 𝐵 ) ) = ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ) )
63 bitsinv1lem ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) + if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) )
64 1 63 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) + if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) )
65 64 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) = ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) + if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) · 𝐵 ) )
66 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
67 2nn ⊢ 2 ∈ ℕ
68 67 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 2 ∈ ℕ )
69 68 61 nnexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
70 66 69 zmodcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 mod ( 2 ↑ 𝑘 ) ) ∈ ℕ0 )
71 70 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 mod ( 2 ↑ 𝑘 ) ) ∈ ℂ )
72 69 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ0 )
73 0nn0 ⊢ 0 ∈ ℕ0
74 ifcl ⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ∈ ℕ0 )
75 72 73 74 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ∈ ℕ0 )
76 75 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ∈ ℂ )
77 51 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
78 71 76 77 adddird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) + if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) · 𝐵 ) = ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) + ( if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) · 𝐵 ) ) )
79 76 77 mulcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) · 𝐵 ) = ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) )
80 79 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) + ( if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) · 𝐵 ) ) = ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) + ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) )
81 65 78 80 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) = ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) + ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) )
82 81 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( bits ‘ ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) ) = ( bits ‘ ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) + ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) ) )
83 70 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 mod ( 2 ↑ 𝑘 ) ) ∈ ℤ )
84 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℤ )
85 83 84 zmulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ∈ ℤ )
86 75 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ∈ ℤ )
87 84 86 zmulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ∈ ℤ )
88 sadadd ⊢ ( ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ∈ ℤ ∧ ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ∈ ℤ ) → ( ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) sadd ( bits ‘ ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) ) = ( bits ‘ ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) + ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) ) )
89 85 87 88 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) sadd ( bits ‘ ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) ) = ( bits ‘ ( ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) + ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) ) )
90 oveq2 ⊢ ( ( 2 ↑ 𝑘 ) = if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) → ( 𝐵 · ( 2 ↑ 𝑘 ) ) = ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) )
91 90 fveqeq2d ⊢ ( ( 2 ↑ 𝑘 ) = if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) → ( ( bits ‘ ( 𝐵 · ( 2 ↑ 𝑘 ) ) ) = { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ↔ ( bits ‘ ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) = { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ) )
92 oveq2 ⊢ ( 0 = if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) → ( 𝐵 · 0 ) = ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) )
93 92 fveqeq2d ⊢ ( 0 = if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) → ( ( bits ‘ ( 𝐵 · 0 ) ) = { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ↔ ( bits ‘ ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) = { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ) )
94 bitsshft ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) } = ( bits ‘ ( 𝐵 · ( 2 ↑ 𝑘 ) ) ) )
95 2 94 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) } = ( bits ‘ ( 𝐵 · ( 2 ↑ 𝑘 ) ) ) )
96 ibar ⊢ ( 𝑘 ∈ ( bits ‘ 𝐴 ) → ( ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ↔ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) ) )
97 96 rabbidv ⊢ ( 𝑘 ∈ ( bits ‘ 𝐴 ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } )
98 95 97 sylan9req ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ∈ ( bits ‘ 𝐴 ) ) → ( bits ‘ ( 𝐵 · ( 2 ↑ 𝑘 ) ) ) = { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } )
99 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( bits ‘ 𝐴 ) ) → 𝐵 ∈ ℂ )
100 99 mul01d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( bits ‘ 𝐴 ) ) → ( 𝐵 · 0 ) = 0 )
101 100 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( bits ‘ 𝐴 ) ) → ( bits ‘ ( 𝐵 · 0 ) ) = ( bits ‘ 0 ) )
102 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( bits ‘ 𝐴 ) ) → ¬ 𝑘 ∈ ( bits ‘ 𝐴 ) )
103 102 intnanrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( bits ‘ 𝐴 ) ) → ¬ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) )
104 103 ralrimivw ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( bits ‘ 𝐴 ) ) → ∀ 𝑛 ∈ ℕ0 ¬ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) )
105 rabeq0 ⊢ ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } = ∅ ↔ ∀ 𝑛 ∈ ℕ0 ¬ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) )
106 104 105 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( bits ‘ 𝐴 ) ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } = ∅ )
107 55 101 106 3eqtr4a ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( bits ‘ 𝐴 ) ) → ( bits ‘ ( 𝐵 · 0 ) ) = { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } )
108 91 93 98 107 ifbothda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( bits ‘ ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) = { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } )
109 108 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) sadd ( bits ‘ ( 𝐵 · if ( 𝑘 ∈ ( bits ‘ 𝐴 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) ) = ( ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ) )
110 82 89 109 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( bits ‘ ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) ) = ( ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ) )
111 62 110 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) ) ↔ ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ) = ( ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ ( bits ‘ 𝐴 ) ∧ ( 𝑛 − 𝑘 ) ∈ ( bits ‘ 𝐵 ) ) } ) ) )
112 57 111 imbitrrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) ) ) )
113 112 expcom ⊢ ( 𝑘 ∈ ℕ0 → ( 𝜑 → ( ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) ) ) ) )
114 113 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑘 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑘 ) ) · 𝐵 ) ) ) → ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ ( 𝑘 + 1 ) ) ) · 𝐵 ) ) ) ) )
115 23 31 39 47 56 114 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) · 𝐵 ) ) ) )
116 3 115 mpcom ⊢ ( 𝜑 → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) smul ( bits ‘ 𝐵 ) ) = ( bits ‘ ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) · 𝐵 ) ) )