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 ↑ 𝑁 ) ) · 𝐵 ) ) )