Metamath Proof Explorer


Theorem smumullem

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

Ref Expression
Hypotheses smumullem.a φ A
smumullem.b φ B
smumullem.n φ N 0
Assertion smumullem φ bits A 0 ..^ N smul bits B = bits A mod 2 N B

Proof

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