| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smumullem.n | . 2
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 2 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑥 = 0 → (0..^𝑥) = (0..^0)) | 
| 3 |  | fzo0 13723 | . . . . . . . . . 10
⊢ (0..^0) =
∅ | 
| 4 | 2, 3 | eqtrdi 2793 | . . . . . . . . 9
⊢ (𝑥 = 0 → (0..^𝑥) = ∅) | 
| 5 | 4 | ineq2d 4220 | . . . . . . . 8
⊢ (𝑥 = 0 → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ ∅)) | 
| 6 |  | in0 4395 | . . . . . . . 8
⊢
((bits‘𝐴)
∩ ∅) = ∅ | 
| 7 | 5, 6 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑥 = 0 → ((bits‘𝐴) ∩ (0..^𝑥)) = ∅) | 
| 8 | 7 | oveq1d 7446 | . . . . . 6
⊢ (𝑥 = 0 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (∅ smul (bits‘𝐵))) | 
| 9 |  | bitsss 16463 | . . . . . . 7
⊢
(bits‘𝐵)
⊆ ℕ0 | 
| 10 |  | smu02 16524 | . . . . . . 7
⊢
((bits‘𝐵)
⊆ ℕ0 → (∅ smul (bits‘𝐵)) = ∅) | 
| 11 | 9, 10 | ax-mp 5 | . . . . . 6
⊢ (∅
smul (bits‘𝐵)) =
∅ | 
| 12 | 8, 11 | eqtrdi 2793 | . . . . 5
⊢ (𝑥 = 0 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = ∅) | 
| 13 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑥 = 0 → (2↑𝑥) = (2↑0)) | 
| 14 |  | 2cn 12341 | . . . . . . . . 9
⊢ 2 ∈
ℂ | 
| 15 |  | exp0 14106 | . . . . . . . . 9
⊢ (2 ∈
ℂ → (2↑0) = 1) | 
| 16 | 14, 15 | ax-mp 5 | . . . . . . . 8
⊢
(2↑0) = 1 | 
| 17 | 13, 16 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑥 = 0 → (2↑𝑥) = 1) | 
| 18 | 17 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = 0 → (𝐴 mod (2↑𝑥)) = (𝐴 mod 1)) | 
| 19 | 18 | fvoveq1d 7453 | . . . . 5
⊢ (𝑥 = 0 → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod 1) · 𝐵))) | 
| 20 | 12, 19 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = 0 → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ ∅ = (bits‘((𝐴 mod 1) · 𝐵)))) | 
| 21 | 20 | imbi2d 340 | . . 3
⊢ (𝑥 = 0 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → ∅ = (bits‘((𝐴 mod 1) · 𝐵))))) | 
| 22 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = 𝑘 → (0..^𝑥) = (0..^𝑘)) | 
| 23 | 22 | ineq2d 4220 | . . . . . 6
⊢ (𝑥 = 𝑘 → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ (0..^𝑘))) | 
| 24 | 23 | oveq1d 7446 | . . . . 5
⊢ (𝑥 = 𝑘 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵))) | 
| 25 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = 𝑘 → (2↑𝑥) = (2↑𝑘)) | 
| 26 | 25 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = 𝑘 → (𝐴 mod (2↑𝑥)) = (𝐴 mod (2↑𝑘))) | 
| 27 | 26 | fvoveq1d 7453 | . . . . 5
⊢ (𝑥 = 𝑘 → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵))) | 
| 28 | 24, 27 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = 𝑘 → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵)))) | 
| 29 | 28 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑘 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵))))) | 
| 30 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (0..^𝑥) = (0..^(𝑘 + 1))) | 
| 31 | 30 | ineq2d 4220 | . . . . . 6
⊢ (𝑥 = (𝑘 + 1) → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ (0..^(𝑘 + 1)))) | 
| 32 | 31 | oveq1d 7446 | . . . . 5
⊢ (𝑥 = (𝑘 + 1) → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵))) | 
| 33 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (2↑𝑥) = (2↑(𝑘 + 1))) | 
| 34 | 33 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (𝐴 mod (2↑𝑥)) = (𝐴 mod (2↑(𝑘 + 1)))) | 
| 35 | 34 | fvoveq1d 7453 | . . . . 5
⊢ (𝑥 = (𝑘 + 1) → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))) | 
| 36 | 32, 35 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = (𝑘 + 1) → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)))) | 
| 37 | 36 | imbi2d 340 | . . 3
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))))) | 
| 38 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (0..^𝑥) = (0..^𝑁)) | 
| 39 | 38 | ineq2d 4220 | . . . . . 6
⊢ (𝑥 = 𝑁 → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ (0..^𝑁))) | 
| 40 | 39 | oveq1d 7446 | . . . . 5
⊢ (𝑥 = 𝑁 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵))) | 
| 41 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁)) | 
| 42 | 41 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = 𝑁 → (𝐴 mod (2↑𝑥)) = (𝐴 mod (2↑𝑁))) | 
| 43 | 42 | fvoveq1d 7453 | . . . . 5
⊢ (𝑥 = 𝑁 → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))) | 
| 44 | 40, 43 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = 𝑁 → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵)))) | 
| 45 | 44 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑁 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))))) | 
| 46 |  | smumullem.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 47 |  | zmod10 13927 | . . . . . . . 8
⊢ (𝐴 ∈ ℤ → (𝐴 mod 1) = 0) | 
| 48 | 46, 47 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝐴 mod 1) = 0) | 
| 49 | 48 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → ((𝐴 mod 1) · 𝐵) = (0 · 𝐵)) | 
| 50 |  | smumullem.b | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 51 | 50 | zcnd 12723 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 52 | 51 | mul02d 11459 | . . . . . 6
⊢ (𝜑 → (0 · 𝐵) = 0) | 
| 53 | 49, 52 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → ((𝐴 mod 1) · 𝐵) = 0) | 
| 54 | 53 | fveq2d 6910 | . . . 4
⊢ (𝜑 → (bits‘((𝐴 mod 1) · 𝐵)) =
(bits‘0)) | 
| 55 |  | 0bits 16476 | . . . 4
⊢
(bits‘0) = ∅ | 
| 56 | 54, 55 | eqtr2di 2794 | . . 3
⊢ (𝜑 → ∅ =
(bits‘((𝐴 mod 1)
· 𝐵))) | 
| 57 |  | oveq1 7438 | . . . . . 6
⊢
((((bits‘𝐴)
∩ (0..^𝑘)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) → ((((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) = ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) | 
| 58 |  | bitsss 16463 | . . . . . . . . 9
⊢
(bits‘𝐴)
⊆ ℕ0 | 
| 59 | 58 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘𝐴) ⊆
ℕ0) | 
| 60 | 9 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘𝐵) ⊆
ℕ0) | 
| 61 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 62 | 59, 60, 61 | smup1 16526 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((bits‘𝐴) ∩
(0..^(𝑘 + 1))) smul
(bits‘𝐵)) =
((((bits‘𝐴) ∩
(0..^𝑘)) smul
(bits‘𝐵)) sadd {𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) | 
| 63 |  | bitsinv1lem 16478 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝐴 mod
(2↑(𝑘 + 1))) = ((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) | 
| 64 | 46, 63 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑(𝑘 + 1))) = ((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) | 
| 65 | 64 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) = (((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) · 𝐵)) | 
| 66 | 46 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈
ℤ) | 
| 67 |  | 2nn 12339 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ | 
| 68 | 67 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℕ) | 
| 69 | 68, 61 | nnexpcld 14284 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(2↑𝑘) ∈
ℕ) | 
| 70 | 66, 69 | zmodcld 13932 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑𝑘)) ∈
ℕ0) | 
| 71 | 70 | nn0cnd 12589 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑𝑘)) ∈ ℂ) | 
| 72 | 69 | nnnn0d 12587 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(2↑𝑘) ∈
ℕ0) | 
| 73 |  | 0nn0 12541 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 | 
| 74 |  | ifcl 4571 | . . . . . . . . . . . . 13
⊢
(((2↑𝑘) ∈
ℕ0 ∧ 0 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈
ℕ0) | 
| 75 | 72, 73, 74 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈
ℕ0) | 
| 76 | 75 | nn0cnd 12589 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈ ℂ) | 
| 77 | 51 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) | 
| 78 | 71, 76, 77 | adddird 11286 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) · 𝐵) = (((𝐴 mod (2↑𝑘)) · 𝐵) + (if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) · 𝐵))) | 
| 79 | 76, 77 | mulcomd 11282 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) · 𝐵) = (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) | 
| 80 | 79 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐴 mod (2↑𝑘)) · 𝐵) + (if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) · 𝐵)) = (((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) | 
| 81 | 65, 78, 80 | 3eqtrd 2781 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) = (((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) | 
| 82 | 81 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘((𝐴 mod
(2↑(𝑘 + 1))) ·
𝐵)) = (bits‘(((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))))) | 
| 83 | 70 | nn0zd 12639 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑𝑘)) ∈ ℤ) | 
| 84 | 50 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℤ) | 
| 85 | 83, 84 | zmulcld 12728 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 mod (2↑𝑘)) · 𝐵) ∈ ℤ) | 
| 86 | 75 | nn0zd 12639 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈ ℤ) | 
| 87 | 84, 86 | zmulcld 12728 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) ∈ ℤ) | 
| 88 |  | sadadd 16504 | . . . . . . . . 9
⊢ ((((𝐴 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 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) sadd (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) = (bits‘(((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))))) | 
| 90 |  | oveq2 7439 | . . . . . . . . . . 11
⊢
((2↑𝑘) =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
(𝐵 · (2↑𝑘)) = (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) | 
| 91 | 90 | fveqeq2d 6914 | . . . . . . . . . 10
⊢
((2↑𝑘) =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
((bits‘(𝐵 ·
(2↑𝑘))) = {𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))} ↔ (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) | 
| 92 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (0 =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
(𝐵 · 0) = (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) | 
| 93 | 92 | fveqeq2d 6914 | . . . . . . . . . 10
⊢ (0 =
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0) →
((bits‘(𝐵 ·
0)) = {𝑛 ∈
ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))} ↔ (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) | 
| 94 |  | bitsshft 16512 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ {𝑛 ∈
ℕ0 ∣ (𝑛 − 𝑘) ∈ (bits‘𝐵)} = (bits‘(𝐵 · (2↑𝑘)))) | 
| 95 | 50, 94 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → {𝑛 ∈ ℕ0
∣ (𝑛 − 𝑘) ∈ (bits‘𝐵)} = (bits‘(𝐵 · (2↑𝑘)))) | 
| 96 |  | ibar 528 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (bits‘𝐴) → ((𝑛 − 𝑘) ∈ (bits‘𝐵) ↔ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵)))) | 
| 97 | 96 | rabbidv 3444 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (bits‘𝐴) → {𝑛 ∈ ℕ0 ∣ (𝑛 − 𝑘) ∈ (bits‘𝐵)} = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) | 
| 98 | 95, 97 | sylan9req 2798 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ∈ (bits‘𝐴)) → (bits‘(𝐵 · (2↑𝑘))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) | 
| 99 | 77 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → 𝐵 ∈ ℂ) | 
| 100 | 99 | mul01d 11460 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → (𝐵 · 0) = 0) | 
| 101 | 100 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → (bits‘(𝐵 · 0)) =
(bits‘0)) | 
| 102 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → ¬ 𝑘 ∈ (bits‘𝐴)) | 
| 103 | 102 | intnanrd 489 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → ¬ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))) | 
| 104 | 103 | ralrimivw 3150 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → ∀𝑛 ∈ ℕ0
¬ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))) | 
| 105 |  | rabeq0 4388 | . . . . . . . . . . . 12
⊢ ({𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))} = ∅ ↔ ∀𝑛 ∈ ℕ0
¬ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))) | 
| 106 | 104, 105 | sylibr 234 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))} = ∅) | 
| 107 | 55, 101, 106 | 3eqtr4a 2803 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (bits‘𝐴)) → (bits‘(𝐵 · 0)) = {𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) | 
| 108 | 91, 93, 98, 107 | ifbothda 4564 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘(𝐵 ·
if(𝑘 ∈
(bits‘𝐴),
(2↑𝑘), 0))) = {𝑛 ∈ ℕ0
∣ (𝑘 ∈
(bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))}) | 
| 109 | 108 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) sadd (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) = ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) | 
| 110 | 82, 89, 109 | 3eqtr2d 2783 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(bits‘((𝐴 mod
(2↑(𝑘 + 1))) ·
𝐵)) = ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛 − 𝑘) ∈ (bits‘𝐵))})) | 
| 111 | 62, 110 | eqeq12d 2753 | . . . . . 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‘𝐵))}))) | 
| 112 | 57, 111 | imbitrrid 246 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((((bits‘𝐴) ∩
(0..^𝑘)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)))) | 
| 113 | 112 | expcom 413 | . . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝜑 →
((((bits‘𝐴) ∩
(0..^𝑘)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑘)) · 𝐵)) → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))))) | 
| 114 | 113 | a2d 29 | . . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝜑 →
(((bits‘𝐴) ∩
(0..^𝑘)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑘)) · 𝐵))) → (𝜑 → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))))) | 
| 115 | 21, 29, 37, 45, 56, 114 | nn0ind 12713 | . 2
⊢ (𝑁 ∈ ℕ0
→ (𝜑 →
(((bits‘𝐴) ∩
(0..^𝑁)) smul
(bits‘𝐵)) =
(bits‘((𝐴 mod
(2↑𝑁)) · 𝐵)))) | 
| 116 | 1, 115 | mpcom 38 | 1
⊢ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))) |