Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  smumullem Structured version   Visualization version   GIF version

Theorem smumullem 15138
 Description: Lemma for smumul 15139. (Contributed by Mario Carneiro, 22-Sep-2016.)
Hypotheses
Ref Expression
smumullem.a (𝜑𝐴 ∈ ℤ)
smumullem.b (𝜑𝐵 ∈ ℤ)
smumullem.n (𝜑𝑁 ∈ ℕ0)
Assertion
Ref Expression
smumullem (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵)))

Proof of Theorem smumullem
Dummy variables 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smumullem.n . 2 (𝜑𝑁 ∈ ℕ0)
2 oveq2 6612 . . . . . . . . . 10 (𝑥 = 0 → (0..^𝑥) = (0..^0))
3 fzo0 12433 . . . . . . . . . 10 (0..^0) = ∅
42, 3syl6eq 2671 . . . . . . . . 9 (𝑥 = 0 → (0..^𝑥) = ∅)
54ineq2d 3792 . . . . . . . 8 (𝑥 = 0 → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ ∅))
6 in0 3940 . . . . . . . 8 ((bits‘𝐴) ∩ ∅) = ∅
75, 6syl6eq 2671 . . . . . . 7 (𝑥 = 0 → ((bits‘𝐴) ∩ (0..^𝑥)) = ∅)
87oveq1d 6619 . . . . . 6 (𝑥 = 0 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (∅ smul (bits‘𝐵)))
9 bitsss 15072 . . . . . . 7 (bits‘𝐵) ⊆ ℕ0
10 smu02 15133 . . . . . . 7 ((bits‘𝐵) ⊆ ℕ0 → (∅ smul (bits‘𝐵)) = ∅)
119, 10ax-mp 5 . . . . . 6 (∅ smul (bits‘𝐵)) = ∅
128, 11syl6eq 2671 . . . . 5 (𝑥 = 0 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = ∅)
13 oveq2 6612 . . . . . . . . 9 (𝑥 = 0 → (2↑𝑥) = (2↑0))
14 2cn 11035 . . . . . . . . . 10 2 ∈ ℂ
15 exp0 12804 . . . . . . . . . 10 (2 ∈ ℂ → (2↑0) = 1)
1614, 15ax-mp 5 . . . . . . . . 9 (2↑0) = 1
1713, 16syl6eq 2671 . . . . . . . 8 (𝑥 = 0 → (2↑𝑥) = 1)
1817oveq2d 6620 . . . . . . 7 (𝑥 = 0 → (𝐴 mod (2↑𝑥)) = (𝐴 mod 1))
1918oveq1d 6619 . . . . . 6 (𝑥 = 0 → ((𝐴 mod (2↑𝑥)) · 𝐵) = ((𝐴 mod 1) · 𝐵))
2019fveq2d 6152 . . . . 5 (𝑥 = 0 → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod 1) · 𝐵)))
2112, 20eqeq12d 2636 . . . 4 (𝑥 = 0 → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ ∅ = (bits‘((𝐴 mod 1) · 𝐵))))
2221imbi2d 330 . . 3 (𝑥 = 0 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → ∅ = (bits‘((𝐴 mod 1) · 𝐵)))))
23 oveq2 6612 . . . . . . 7 (𝑥 = 𝑘 → (0..^𝑥) = (0..^𝑘))
2423ineq2d 3792 . . . . . 6 (𝑥 = 𝑘 → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ (0..^𝑘)))
2524oveq1d 6619 . . . . 5 (𝑥 = 𝑘 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)))
26 oveq2 6612 . . . . . . . 8 (𝑥 = 𝑘 → (2↑𝑥) = (2↑𝑘))
2726oveq2d 6620 . . . . . . 7 (𝑥 = 𝑘 → (𝐴 mod (2↑𝑥)) = (𝐴 mod (2↑𝑘)))
2827oveq1d 6619 . . . . . 6 (𝑥 = 𝑘 → ((𝐴 mod (2↑𝑥)) · 𝐵) = ((𝐴 mod (2↑𝑘)) · 𝐵))
2928fveq2d 6152 . . . . 5 (𝑥 = 𝑘 → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵)))
3025, 29eqeq12d 2636 . . . 4 (𝑥 = 𝑘 → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵))))
3130imbi2d 330 . . 3 (𝑥 = 𝑘 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵)))))
32 oveq2 6612 . . . . . . 7 (𝑥 = (𝑘 + 1) → (0..^𝑥) = (0..^(𝑘 + 1)))
3332ineq2d 3792 . . . . . 6 (𝑥 = (𝑘 + 1) → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ (0..^(𝑘 + 1))))
3433oveq1d 6619 . . . . 5 (𝑥 = (𝑘 + 1) → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)))
35 oveq2 6612 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (2↑𝑥) = (2↑(𝑘 + 1)))
3635oveq2d 6620 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝐴 mod (2↑𝑥)) = (𝐴 mod (2↑(𝑘 + 1))))
3736oveq1d 6619 . . . . . 6 (𝑥 = (𝑘 + 1) → ((𝐴 mod (2↑𝑥)) · 𝐵) = ((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))
3837fveq2d 6152 . . . . 5 (𝑥 = (𝑘 + 1) → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)))
3934, 38eqeq12d 2636 . . . 4 (𝑥 = (𝑘 + 1) → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))))
4039imbi2d 330 . . 3 (𝑥 = (𝑘 + 1) → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)))))
41 oveq2 6612 . . . . . . 7 (𝑥 = 𝑁 → (0..^𝑥) = (0..^𝑁))
4241ineq2d 3792 . . . . . 6 (𝑥 = 𝑁 → ((bits‘𝐴) ∩ (0..^𝑥)) = ((bits‘𝐴) ∩ (0..^𝑁)))
4342oveq1d 6619 . . . . 5 (𝑥 = 𝑁 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)))
44 oveq2 6612 . . . . . . . 8 (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁))
4544oveq2d 6620 . . . . . . 7 (𝑥 = 𝑁 → (𝐴 mod (2↑𝑥)) = (𝐴 mod (2↑𝑁)))
4645oveq1d 6619 . . . . . 6 (𝑥 = 𝑁 → ((𝐴 mod (2↑𝑥)) · 𝐵) = ((𝐴 mod (2↑𝑁)) · 𝐵))
4746fveq2d 6152 . . . . 5 (𝑥 = 𝑁 → (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵)))
4843, 47eqeq12d 2636 . . . 4 (𝑥 = 𝑁 → ((((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵)) ↔ (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))))
4948imbi2d 330 . . 3 (𝑥 = 𝑁 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑥)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑥)) · 𝐵))) ↔ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵)))))
50 smumullem.a . . . . . . . 8 (𝜑𝐴 ∈ ℤ)
51 zmod10 12626 . . . . . . . 8 (𝐴 ∈ ℤ → (𝐴 mod 1) = 0)
5250, 51syl 17 . . . . . . 7 (𝜑 → (𝐴 mod 1) = 0)
5352oveq1d 6619 . . . . . 6 (𝜑 → ((𝐴 mod 1) · 𝐵) = (0 · 𝐵))
54 smumullem.b . . . . . . . 8 (𝜑𝐵 ∈ ℤ)
5554zcnd 11427 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
5655mul02d 10178 . . . . . 6 (𝜑 → (0 · 𝐵) = 0)
5753, 56eqtrd 2655 . . . . 5 (𝜑 → ((𝐴 mod 1) · 𝐵) = 0)
5857fveq2d 6152 . . . 4 (𝜑 → (bits‘((𝐴 mod 1) · 𝐵)) = (bits‘0))
59 0bits 15085 . . . 4 (bits‘0) = ∅
6058, 59syl6req 2672 . . 3 (𝜑 → ∅ = (bits‘((𝐴 mod 1) · 𝐵)))
61 oveq1 6611 . . . . . 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 15072 . . . . . . . . 9 (bits‘𝐴) ⊆ ℕ0
6362a1i 11 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (bits‘𝐴) ⊆ ℕ0)
649a1i 11 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (bits‘𝐵) ⊆ ℕ0)
65 simpr 477 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
6663, 64, 65smup1 15135 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = ((((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))}))
67 bitsinv1lem 15087 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑(𝑘 + 1))) = ((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))
6850, 67sylan 488 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝐴 mod (2↑(𝑘 + 1))) = ((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))
6968oveq1d 6619 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) = (((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) · 𝐵))
7050adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 𝐴 ∈ ℤ)
71 2nn 11129 . . . . . . . . . . . . . . 15 2 ∈ ℕ
7271a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℕ)
7372, 65nnexpcld 12970 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
7470, 73zmodcld 12631 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (𝐴 mod (2↑𝑘)) ∈ ℕ0)
7574nn0cnd 11297 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝐴 mod (2↑𝑘)) ∈ ℂ)
7673nnnn0d 11295 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ0)
77 0nn0 11251 . . . . . . . . . . . . 13 0 ∈ ℕ0
78 ifcl 4102 . . . . . . . . . . . . 13 (((2↑𝑘) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈ ℕ0)
7976, 77, 78sylancl 693 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈ ℕ0)
8079nn0cnd 11297 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈ ℂ)
8155adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
8275, 80, 81adddird 10009 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝐴 mod (2↑𝑘)) + if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) · 𝐵) = (((𝐴 mod (2↑𝑘)) · 𝐵) + (if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) · 𝐵)))
8380, 81mulcomd 10005 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) · 𝐵) = (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))
8483oveq2d 6620 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝐴 mod (2↑𝑘)) · 𝐵) + (if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) · 𝐵)) = (((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))))
8569, 82, 843eqtrd 2659 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) = (((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))))
8685fveq2d 6152 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)) = (bits‘(((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))))
8774nn0zd 11424 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (𝐴 mod (2↑𝑘)) ∈ ℤ)
8854adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℤ)
8987, 88zmulcld 11432 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝐴 mod (2↑𝑘)) · 𝐵) ∈ ℤ)
9079nn0zd 11424 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) ∈ ℤ)
9188, 90zmulcld 11432 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) ∈ ℤ)
92 sadadd 15113 . . . . . . . . 9 ((((𝐴 mod (2↑𝑘)) · 𝐵) ∈ ℤ ∧ (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)) ∈ ℤ) → ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) = (bits‘(((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))))
9389, 91, 92syl2anc 692 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) = (bits‘(((𝐴 mod (2↑𝑘)) · 𝐵) + (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))))
94 oveq2 6612 . . . . . . . . . . . 12 ((2↑𝑘) = if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) → (𝐵 · (2↑𝑘)) = (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))
9594fveq2d 6152 . . . . . . . . . . 11 ((2↑𝑘) = if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) → (bits‘(𝐵 · (2↑𝑘))) = (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))))
9695eqeq1d 2623 . . . . . . . . . 10 ((2↑𝑘) = if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) → ((bits‘(𝐵 · (2↑𝑘))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))} ↔ (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))}))
97 oveq2 6612 . . . . . . . . . . . 12 (0 = if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) → (𝐵 · 0) = (𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))
9897fveq2d 6152 . . . . . . . . . . 11 (0 = if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) → (bits‘(𝐵 · 0)) = (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))))
9998eqeq1d 2623 . . . . . . . . . 10 (0 = if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0) → ((bits‘(𝐵 · 0)) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))} ↔ (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))}))
100 bitsshft 15121 . . . . . . . . . . . 12 ((𝐵 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → {𝑛 ∈ ℕ0 ∣ (𝑛𝑘) ∈ (bits‘𝐵)} = (bits‘(𝐵 · (2↑𝑘))))
10154, 100sylan 488 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → {𝑛 ∈ ℕ0 ∣ (𝑛𝑘) ∈ (bits‘𝐵)} = (bits‘(𝐵 · (2↑𝑘))))
102 ibar 525 . . . . . . . . . . . 12 (𝑘 ∈ (bits‘𝐴) → ((𝑛𝑘) ∈ (bits‘𝐵) ↔ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))))
103102rabbidv 3177 . . . . . . . . . . 11 (𝑘 ∈ (bits‘𝐴) → {𝑛 ∈ ℕ0 ∣ (𝑛𝑘) ∈ (bits‘𝐵)} = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))})
104101, 103sylan9req 2676 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑘 ∈ (bits‘𝐴)) → (bits‘(𝐵 · (2↑𝑘))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))})
10581adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ∈ (bits‘𝐴)) → 𝐵 ∈ ℂ)
106105mul01d 10179 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ∈ (bits‘𝐴)) → (𝐵 · 0) = 0)
107106fveq2d 6152 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ∈ (bits‘𝐴)) → (bits‘(𝐵 · 0)) = (bits‘0))
108 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ∈ (bits‘𝐴)) → ¬ 𝑘 ∈ (bits‘𝐴))
109108intnanrd 962 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ∈ (bits‘𝐴)) → ¬ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵)))
110109ralrimivw 2961 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ∈ (bits‘𝐴)) → ∀𝑛 ∈ ℕ0 ¬ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵)))
111 rabeq0 3931 . . . . . . . . . . . 12 ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))} = ∅ ↔ ∀𝑛 ∈ ℕ0 ¬ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵)))
112110, 111sylibr 224 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ∈ (bits‘𝐴)) → {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))} = ∅)
11359, 107, 1123eqtr4a 2681 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ∈ (bits‘𝐴)) → (bits‘(𝐵 · 0)) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))})
11496, 99, 104, 113ifbothda 4095 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0))) = {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))})
115114oveq2d 6620 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd (bits‘(𝐵 · if(𝑘 ∈ (bits‘𝐴), (2↑𝑘), 0)))) = ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))}))
11686, 93, 1153eqtr2d 2661 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)) = ((bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ (bits‘𝐴) ∧ (𝑛𝑘) ∈ (bits‘𝐵))}))
11766, 116eqeq12d 2636 . . . . . 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‘𝐵))})))
11861, 117syl5ibr 236 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵))))
119118expcom 451 . . . 4 (𝑘 ∈ ℕ0 → (𝜑 → ((((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵)) → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)))))
120119a2d 29 . . 3 (𝑘 ∈ ℕ0 → ((𝜑 → (((bits‘𝐴) ∩ (0..^𝑘)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑘)) · 𝐵))) → (𝜑 → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)))))
12122, 31, 40, 49, 60, 120nn0ind 11416 . 2 (𝑁 ∈ ℕ0 → (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))))
1221, 121mpcom 38 1 (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵)))