Step | Hyp | Ref
| Expression |
1 | | smumullem.n |
. 2
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (0..^𝑥) = (0..^0)) |
3 | | fzo0 12361 |
. . . . . . . . . 10
⊢ (0..^0) =
∅ |
4 | 2, 3 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (0..^𝑥) = ∅) |
5 | 4 | ineq2d 3776 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ ∅)) |
6 | | in0 3920 |
. . . . . . . 8
⊢
((bits‘𝐴)
∩ ∅) = ∅ |
7 | 5, 6 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑥 = 0 → ((bits‘𝐴) ∩ (0..^𝑥)) = ∅) |
8 | 7 | oveq1d 6564 |
. . . . . 6
⊢ (𝑥 = 0 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (∅ smul (bits‘𝐵))) |
9 | | bitsss 14986 |
. . . . . . 7
⊢
(bits‘𝐵)
⊆ ℕ0 |
10 | | smu02 15047 |
. . . . . . 7
⊢
((bits‘𝐵)
⊆ ℕ0 → (∅ smul (bits‘𝐵)) = ∅) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
⊢ (∅
smul (bits‘𝐵)) =
∅ |
12 | 8, 11 | syl6eq 2660 |
. . . . 5
⊢ (𝑥 = 0 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = ∅) |
13 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (2↑𝑥) = (2↑0)) |
14 | | 2cn 10968 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
15 | | exp0 12726 |
. . . . . . . . . 10
⊢ (2 ∈
ℂ → (2↑0) = 1) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . 9
⊢
(2↑0) = 1 |
17 | 13, 16 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑥 = 0 → (2↑𝑥) = 1) |
18 | 17 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝐴 mod (2↑𝑥)) = (𝐴 mod 1)) |
19 | 18 | oveq1d 6564 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝐴 mod (2↑𝑥)) · 𝐵) = ((𝐴 mod 1) · 𝐵)) |
20 | 19 | fveq2d 6107 |
. . . . 5
⊢ (𝑥 = 0 → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod 1) · 𝐵))) |
21 | 12, 20 | eqeq12d 2625 |
. . . 4
⊢ (𝑥 = 0 → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ ∅ = (bits‘((𝐴 mod 1) · 𝐵)))) |
22 | 21 | imbi2d 329 |
. . 3
⊢ (𝑥 = 0 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → ∅ = (bits‘((𝐴 mod 1) · 𝐵))))) |
23 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (0..^𝑥) = (0..^𝑘)) |
24 | 23 | ineq2d 3776 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ (0..^𝑘))) |
25 | 24 | oveq1d 6564 |
. . . . 5
⊢ (𝑥 = 𝑘 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵))) |
26 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (2↑𝑥) = (2↑𝑘)) |
27 | 26 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝐴 mod (2↑𝑥)) = (𝐴 mod (2↑𝑘))) |
28 | 27 | oveq1d 6564 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝐴 mod (2↑𝑥)) · 𝐵) = ((𝐴 mod (2↑𝑘)) · 𝐵)) |
29 | 28 | fveq2d 6107 |
. . . . 5
⊢ (𝑥 = 𝑘 → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵))) |
30 | 25, 29 | eqeq12d 2625 |
. . . 4
⊢ (𝑥 = 𝑘 → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵)))) |
31 | 30 | imbi2d 329 |
. . 3
⊢ (𝑥 = 𝑘 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵))))) |
32 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (0..^𝑥) = (0..^(𝑘 + 1))) |
33 | 32 | ineq2d 3776 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ (0..^(𝑘 + 1)))) |
34 | 33 | oveq1d 6564 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵))) |
35 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (2↑𝑥) = (2↑(𝑘 + 1))) |
36 | 35 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝐴 mod (2↑𝑥)) = (𝐴 mod (2↑(𝑘 + 1)))) |
37 | 36 | oveq1d 6564 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → ((𝐴 mod (2↑𝑥)) · 𝐵) = ((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)) |
38 | 37 | fveq2d 6107 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))) |
39 | 34, 38 | eqeq12d 2625 |
. . . 4
⊢ (𝑥 = (𝑘 + 1) → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)))) |
40 | 39 | imbi2d 329 |
. . 3
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))))) |
41 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (0..^𝑥) = (0..^𝑁)) |
42 | 41 | ineq2d 3776 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ (0..^𝑁))) |
43 | 42 | oveq1d 6564 |
. . . . 5
⊢ (𝑥 = 𝑁 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵))) |
44 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁)) |
45 | 44 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐴 mod (2↑𝑥)) = (𝐴 mod (2↑𝑁))) |
46 | 45 | oveq1d 6564 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝐴 mod (2↑𝑥)) · 𝐵) = ((𝐴 mod (2↑𝑁)) · 𝐵)) |
47 | 46 | fveq2d 6107 |
. . . . 5
⊢ (𝑥 = 𝑁 → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))) |
48 | 43, 47 | eqeq12d 2625 |
. . . 4
⊢ (𝑥 = 𝑁 → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵)))) |
49 | 48 | imbi2d 329 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))))) |
50 | | smumullem.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℤ) |
51 | | zmod10 12548 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → (𝐴 mod 1) = 0) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴 mod 1) = 0) |
53 | 52 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → ((𝐴 mod 1) · 𝐵) = (0 · 𝐵)) |
54 | | smumullem.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℤ) |
55 | 54 | zcnd 11359 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
56 | 55 | mul02d 10113 |
. . . . . 6
⊢ (𝜑 → (0 · 𝐵) = 0) |
57 | 53, 56 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → ((𝐴 mod 1) · 𝐵) = 0) |
58 | 57 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (bits‘((𝐴 mod 1) · 𝐵)) =
(bits‘0)) |
59 | | 0bits 14999 |
. . . 4
⊢
(bits‘0) = ∅ |
60 | 58, 59 | syl6req 2661 |
. . 3
⊢ (𝜑 → ∅ =
(bits‘((𝐴 mod 1)
· 𝐵))) |
61 | | oveq1 6556 |
. . . . . 6
⊢
((((bits‘𝐴)
∩ (0..^𝑘)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) → ((((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) = ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) |
62 | | bitsss 14986 |
. . . . . . . . 9
⊢
(bits‘𝐴)
⊆ ℕ0 |
63 | 62 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘𝐴) ⊆
ℕ0) |
64 | 9 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘𝐵) ⊆
ℕ0) |
65 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
66 | 63, 64, 65 | smup1 15049 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((bits‘𝐴) ∩
(0..^(𝑘 + 1))) smul
(bits‘𝐵)) =
((((bits‘𝐴) ∩
(0..^𝑘)) smul
(bits‘𝐵)) sadd {𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) |
67 | | bitsinv1lem 15001 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝐴 mod
(2↑(𝑘 + 1))) = ((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) |
68 | 50, 67 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑(𝑘 + 1))) = ((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) |
69 | 68 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) = (((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) · 𝐵)) |
70 | 50 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈
ℤ) |
71 | | 2nn 11062 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℕ) |
73 | 72, 65 | nnexpcld 12892 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(2↑𝑘) ∈
ℕ) |
74 | 70, 73 | zmodcld 12553 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑𝑘)) ∈
ℕ0) |
75 | 74 | nn0cnd 11230 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑𝑘)) ∈ ℂ) |
76 | 73 | nnnn0d 11228 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(2↑𝑘) ∈
ℕ0) |
77 | | 0nn0 11184 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
78 | | ifcl 4080 |
. . . . . . . . . . . . 13
⊢
(((2↑𝑘) ∈
ℕ0 ∧ 0 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈
ℕ0) |
79 | 76, 77, 78 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈
ℕ0) |
80 | 79 | nn0cnd 11230 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈ ℂ) |
81 | 55 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) |
82 | 75, 80, 81 | adddird 9944 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) · 𝐵) = (((𝐴 mod (2↑𝑘)) · 𝐵) + (if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) · 𝐵))) |
83 | 80, 81 | mulcomd 9940 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) · 𝐵) = (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) |
84 | 83 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐴 mod (2↑𝑘)) · 𝐵) + (if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) · 𝐵)) = (((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) |
85 | 69, 82, 84 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) = (((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) |
86 | 85 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘((𝐴 mod
(2↑(𝑘 + 1))) ·
𝐵)) = (bits‘(((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))))) |
87 | 74 | nn0zd 11356 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑𝑘)) ∈ ℤ) |
88 | 54 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℤ) |
89 | 87, 88 | zmulcld 11364 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 mod (2↑𝑘)) · 𝐵) ∈ ℤ) |
90 | 79 | nn0zd 11356 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈ ℤ) |
91 | 88, 90 | zmulcld 11364 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) ∈ ℤ) |
92 | | sadadd 15027 |
. . . . . . . . 9
⊢ ((((𝐴 mod (2↑𝑘)) · 𝐵) ∈ ℤ ∧ (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) ∈ ℤ) →
((bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) sadd (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) = (bits‘(((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))))) |
93 | 89, 91, 92 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) sadd (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) = (bits‘(((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))))) |
94 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢
((2↑𝑘) =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
(𝐵 · (2↑𝑘)) = (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) |
95 | 94 | fveq2d 6107 |
. . . . . . . . . . 11
⊢
((2↑𝑘) =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
(bits‘(𝐵 ·
(2↑𝑘))) =
(bits‘(𝐵 ·
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘),
0)))) |
96 | 95 | eqeq1d 2612 |
. . . . . . . . . 10
⊢
((2↑𝑘) =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
((bits‘(𝐵 ·
(2↑𝑘))) = {𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))} ↔ (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) |
97 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (0 =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
(𝐵 · 0) = (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) |
98 | 97 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (0 =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
(bits‘(𝐵 · 0))
= (bits‘(𝐵 ·
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘),
0)))) |
99 | 98 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (0 =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
((bits‘(𝐵 ·
0)) = {𝑛 ∈
ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))} ↔ (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) |
100 | | bitsshft 15035 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ {𝑛 ∈
ℕ0 ∣ (𝑛 − 𝑘) ∈ (bits‘𝐵)} = (bits‘(𝐵 · (2↑𝑘)))) |
101 | 54, 100 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → {𝑛 ∈ ℕ0
∣ (𝑛 − 𝑘) ∈ (bits‘𝐵)} = (bits‘(𝐵 · (2↑𝑘)))) |
102 | | ibar 524 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (bits‘𝐴) → ((𝑛 − 𝑘) ∈ (bits‘𝐵) ↔ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵)))) |
103 | 102 | rabbidv 3164 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (bits‘𝐴) → {𝑛 ∈ ℕ0 ∣ (𝑛 − 𝑘) ∈ (bits‘𝐵)} = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) |
104 | 101, 103 | sylan9req 2665 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ∈ (bits‘𝐴)) → (bits‘(𝐵 · (2↑𝑘))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) |
105 | 81 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → 𝐵 ∈ ℂ) |
106 | 105 | mul01d 10114 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → (𝐵 · 0) = 0) |
107 | 106 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → (bits‘(𝐵 · 0)) =
(bits‘0)) |
108 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → ¬ 𝑘 ∈ (bits‘𝐴)) |
109 | 108 | intnanrd 954 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → ¬ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))) |
110 | 109 | ralrimivw 2950 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → ∀𝑛 ∈ ℕ0
¬ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))) |
111 | | rabeq0 3911 |
. . . . . . . . . . . 12
⊢ ({𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))} = ∅ ↔ ∀𝑛 ∈ ℕ0
¬ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))) |
112 | 110, 111 | sylibr 223 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))} = ∅) |
113 | 59, 107, 112 | 3eqtr4a 2670 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → (bits‘(𝐵 · 0)) = {𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) |
114 | 96, 99, 104, 113 | ifbothda 4073 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘(𝐵 ·
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0))) = {𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) |
115 | 114 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) sadd (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) = ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) |
116 | 86, 93, 115 | 3eqtr2d 2650 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘((𝐴 mod
(2↑(𝑘 + 1))) ·
𝐵)) = ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) |
117 | 66, 116 | eqeq12d 2625 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ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‘𝐵))}))) |
118 | 61, 117 | syl5ibr 235 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((((bits‘𝐴) ∩
(0..^𝑘)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)))) |
119 | 118 | expcom 450 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝜑 →
((((bits‘𝐴) ∩
(0..^𝑘)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))))) |
120 | 119 | a2d 29 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝜑 →
(((bits‘𝐴) ∩
(0..^𝑘)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑘)) · 𝐵))) → (𝜑 → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))))) |
121 | 22, 31, 40, 49, 60, 120 | nn0ind 11348 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝜑 →
(((bits‘𝐴) ∩
(0..^𝑁)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑁)) · 𝐵)))) |
122 | 1, 121 | mpcom 37 |
1
⊢ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))) |