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 φN0
Assertion smumullem φbitsA0..^NsmulbitsB=bitsAmod2NB

Proof

Step Hyp Ref Expression
1 smumullem.a φA
2 smumullem.b φB
3 smumullem.n φN0
4 oveq2 x=00..^x=0..^0
5 fzo0 0..^0=
6 4 5 eqtrdi x=00..^x=
7 6 ineq2d x=0bitsA0..^x=bitsA
8 in0 bitsA=
9 7 8 eqtrdi x=0bitsA0..^x=
10 9 oveq1d x=0bitsA0..^xsmulbitsB=smulbitsB
11 bitsss bitsB0
12 smu02 bitsB0smulbitsB=
13 11 12 ax-mp smulbitsB=
14 10 13 eqtrdi x=0bitsA0..^xsmulbitsB=
15 oveq2 x=02x=20
16 2cn 2
17 exp0 220=1
18 16 17 ax-mp 20=1
19 15 18 eqtrdi x=02x=1
20 19 oveq2d x=0Amod2x=Amod1
21 20 fvoveq1d x=0bitsAmod2xB=bitsAmod1B
22 14 21 eqeq12d x=0bitsA0..^xsmulbitsB=bitsAmod2xB=bitsAmod1B
23 22 imbi2d x=0φbitsA0..^xsmulbitsB=bitsAmod2xBφ=bitsAmod1B
24 oveq2 x=k0..^x=0..^k
25 24 ineq2d x=kbitsA0..^x=bitsA0..^k
26 25 oveq1d x=kbitsA0..^xsmulbitsB=bitsA0..^ksmulbitsB
27 oveq2 x=k2x=2k
28 27 oveq2d x=kAmod2x=Amod2k
29 28 fvoveq1d x=kbitsAmod2xB=bitsAmod2kB
30 26 29 eqeq12d x=kbitsA0..^xsmulbitsB=bitsAmod2xBbitsA0..^ksmulbitsB=bitsAmod2kB
31 30 imbi2d x=kφbitsA0..^xsmulbitsB=bitsAmod2xBφbitsA0..^ksmulbitsB=bitsAmod2kB
32 oveq2 x=k+10..^x=0..^k+1
33 32 ineq2d x=k+1bitsA0..^x=bitsA0..^k+1
34 33 oveq1d x=k+1bitsA0..^xsmulbitsB=bitsA0..^k+1smulbitsB
35 oveq2 x=k+12x=2k+1
36 35 oveq2d x=k+1Amod2x=Amod2k+1
37 36 fvoveq1d x=k+1bitsAmod2xB=bitsAmod2k+1B
38 34 37 eqeq12d x=k+1bitsA0..^xsmulbitsB=bitsAmod2xBbitsA0..^k+1smulbitsB=bitsAmod2k+1B
39 38 imbi2d x=k+1φbitsA0..^xsmulbitsB=bitsAmod2xBφbitsA0..^k+1smulbitsB=bitsAmod2k+1B
40 oveq2 x=N0..^x=0..^N
41 40 ineq2d x=NbitsA0..^x=bitsA0..^N
42 41 oveq1d x=NbitsA0..^xsmulbitsB=bitsA0..^NsmulbitsB
43 oveq2 x=N2x=2N
44 43 oveq2d x=NAmod2x=Amod2N
45 44 fvoveq1d x=NbitsAmod2xB=bitsAmod2NB
46 42 45 eqeq12d x=NbitsA0..^xsmulbitsB=bitsAmod2xBbitsA0..^NsmulbitsB=bitsAmod2NB
47 46 imbi2d x=NφbitsA0..^xsmulbitsB=bitsAmod2xBφbitsA0..^NsmulbitsB=bitsAmod2NB
48 zmod10 AAmod1=0
49 1 48 syl φAmod1=0
50 49 oveq1d φAmod1B=0B
51 2 zcnd φB
52 51 mul02d φ0B=0
53 50 52 eqtrd φAmod1B=0
54 53 fveq2d φbitsAmod1B=bits0
55 0bits bits0=
56 54 55 eqtr2di φ=bitsAmod1B
57 oveq1 bitsA0..^ksmulbitsB=bitsAmod2kBbitsA0..^ksmulbitsBsaddn0|kbitsAnkbitsB=bitsAmod2kBsaddn0|kbitsAnkbitsB
58 bitsss bitsA0
59 58 a1i φk0bitsA0
60 11 a1i φk0bitsB0
61 simpr φk0k0
62 59 60 61 smup1 φk0bitsA0..^k+1smulbitsB=bitsA0..^ksmulbitsBsaddn0|kbitsAnkbitsB
63 bitsinv1lem Ak0Amod2k+1=Amod2k+ifkbitsA2k0
64 1 63 sylan φk0Amod2k+1=Amod2k+ifkbitsA2k0
65 64 oveq1d φk0Amod2k+1B=Amod2k+ifkbitsA2k0B
66 1 adantr φk0A
67 2nn 2
68 67 a1i φk02
69 68 61 nnexpcld φk02k
70 66 69 zmodcld φk0Amod2k0
71 70 nn0cnd φk0Amod2k
72 69 nnnn0d φk02k0
73 0nn0 00
74 ifcl 2k000ifkbitsA2k00
75 72 73 74 sylancl φk0ifkbitsA2k00
76 75 nn0cnd φk0ifkbitsA2k0
77 51 adantr φk0B
78 71 76 77 adddird φk0Amod2k+ifkbitsA2k0B=Amod2kB+ifkbitsA2k0B
79 76 77 mulcomd φk0ifkbitsA2k0B=BifkbitsA2k0
80 79 oveq2d φk0Amod2kB+ifkbitsA2k0B=Amod2kB+BifkbitsA2k0
81 65 78 80 3eqtrd φk0Amod2k+1B=Amod2kB+BifkbitsA2k0
82 81 fveq2d φk0bitsAmod2k+1B=bitsAmod2kB+BifkbitsA2k0
83 70 nn0zd φk0Amod2k
84 2 adantr φk0B
85 83 84 zmulcld φk0Amod2kB
86 75 nn0zd φk0ifkbitsA2k0
87 84 86 zmulcld φk0BifkbitsA2k0
88 sadadd Amod2kBBifkbitsA2k0bitsAmod2kBsaddbitsBifkbitsA2k0=bitsAmod2kB+BifkbitsA2k0
89 85 87 88 syl2anc φk0bitsAmod2kBsaddbitsBifkbitsA2k0=bitsAmod2kB+BifkbitsA2k0
90 oveq2 2k=ifkbitsA2k0B2k=BifkbitsA2k0
91 90 fveqeq2d 2k=ifkbitsA2k0bitsB2k=n0|kbitsAnkbitsBbitsBifkbitsA2k0=n0|kbitsAnkbitsB
92 oveq2 0=ifkbitsA2k0B0=BifkbitsA2k0
93 92 fveqeq2d 0=ifkbitsA2k0bitsB0=n0|kbitsAnkbitsBbitsBifkbitsA2k0=n0|kbitsAnkbitsB
94 bitsshft Bk0n0|nkbitsB=bitsB2k
95 2 94 sylan φk0n0|nkbitsB=bitsB2k
96 ibar kbitsAnkbitsBkbitsAnkbitsB
97 96 rabbidv kbitsAn0|nkbitsB=n0|kbitsAnkbitsB
98 95 97 sylan9req φk0kbitsAbitsB2k=n0|kbitsAnkbitsB
99 77 adantr φk0¬kbitsAB
100 99 mul01d φk0¬kbitsAB0=0
101 100 fveq2d φk0¬kbitsAbitsB0=bits0
102 simpr φk0¬kbitsA¬kbitsA
103 102 intnanrd φk0¬kbitsA¬kbitsAnkbitsB
104 103 ralrimivw φk0¬kbitsAn0¬kbitsAnkbitsB
105 rabeq0 n0|kbitsAnkbitsB=n0¬kbitsAnkbitsB
106 104 105 sylibr φk0¬kbitsAn0|kbitsAnkbitsB=
107 55 101 106 3eqtr4a φk0¬kbitsAbitsB0=n0|kbitsAnkbitsB
108 91 93 98 107 ifbothda φk0bitsBifkbitsA2k0=n0|kbitsAnkbitsB
109 108 oveq2d φk0bitsAmod2kBsaddbitsBifkbitsA2k0=bitsAmod2kBsaddn0|kbitsAnkbitsB
110 82 89 109 3eqtr2d φk0bitsAmod2k+1B=bitsAmod2kBsaddn0|kbitsAnkbitsB
111 62 110 eqeq12d φk0bitsA0..^k+1smulbitsB=bitsAmod2k+1BbitsA0..^ksmulbitsBsaddn0|kbitsAnkbitsB=bitsAmod2kBsaddn0|kbitsAnkbitsB
112 57 111 syl5ibr φk0bitsA0..^ksmulbitsB=bitsAmod2kBbitsA0..^k+1smulbitsB=bitsAmod2k+1B
113 112 expcom k0φbitsA0..^ksmulbitsB=bitsAmod2kBbitsA0..^k+1smulbitsB=bitsAmod2k+1B
114 113 a2d k0φbitsA0..^ksmulbitsB=bitsAmod2kBφbitsA0..^k+1smulbitsB=bitsAmod2k+1B
115 23 31 39 47 56 114 nn0ind N0φbitsA0..^NsmulbitsB=bitsAmod2NB
116 3 115 mpcom φbitsA0..^NsmulbitsB=bitsAmod2NB