Metamath Proof Explorer

Theorem smumullem

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

Ref Expression
Hypotheses smumullem.a 
|- ( ph -> A e. ZZ )
smumullem.b 
|- ( ph -> B e. ZZ )
smumullem.n 
|- ( ph -> N e. NN0 )
Assertion smumullem 
|- ( ph -> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) smul ( bits ` B ) ) = ( bits ` ( ( A mod ( 2 ^ N ) ) x. B ) ) )

Proof

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