Metamath Proof Explorer

Theorem sadaddlem

Description: Lemma for sadadd . (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses sadaddlem.c 
|- C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. ( bits ` A ) , m e. ( bits ` B ) , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
sadaddlem.k 
|- K = `' ( bits |` NN0 )
sadaddlem.1 
|- ( ph -> A e. ZZ )
sadaddlem.2 
|- ( ph -> B e. ZZ )
sadaddlem.3 
|- ( ph -> N e. NN0 )
Assertion sadaddlem 
|- ( ph -> ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) = ( bits ` ( ( A + B ) mod ( 2 ^ N ) ) ) )

Proof

Step Hyp Ref Expression
1 sadaddlem.c 
 |-  C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. ( bits ` A ) , m e. ( bits ` B ) , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
2 sadaddlem.k 
 |-  K = `' ( bits |` NN0 )
3 sadaddlem.1 
 |-  ( ph -> A e. ZZ )
4 sadaddlem.2 
 |-  ( ph -> B e. ZZ )
5 sadaddlem.3 
 |-  ( ph -> N e. NN0 )
6 2nn 
 |-  2 e. NN
7 6 a1i 
 |-  ( ph -> 2 e. NN )
8 7 5 nnexpcld 
 |-  ( ph -> ( 2 ^ N ) e. NN )
9 8 nnzd 
 |-  ( ph -> ( 2 ^ N ) e. ZZ )
10 inss1 
 |-  ( ( bits ` A ) i^i ( 0 ..^ N ) ) C_ ( bits ` A )
11 bitsss 
 |-  ( bits ` A ) C_ NN0
12 10 11 sstri 
 |-  ( ( bits ` A ) i^i ( 0 ..^ N ) ) C_ NN0
13 fzofi 
 |-  ( 0 ..^ N ) e. Fin
14 inss2 
 |-  ( ( bits ` A ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
15 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( bits ` A ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( bits ` A ) i^i ( 0 ..^ N ) ) e. Fin )
16 13 14 15 mp2an 
 |-  ( ( bits ` A ) i^i ( 0 ..^ N ) ) e. Fin
17 elfpw 
 |-  ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( bits ` A ) i^i ( 0 ..^ N ) ) e. Fin ) )
18 12 16 17 mpbir2an 
 |-  ( ( bits ` A ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin )
19 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
20 f1ocnv 
 |-  ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
21 f1of 
 |-  ( `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
22 19 20 21 mp2b 
 |-  `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0
23 2 feq1i 
 |-  ( K : ( ~P NN0 i^i Fin ) --> NN0 <-> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
24 22 23 mpbir 
 |-  K : ( ~P NN0 i^i Fin ) --> NN0
25 24 ffvelcdmi 
 |-  ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) e. NN0 )
26 18 25 mp1i 
 |-  ( ph -> ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) e. NN0 )
27 26 nn0zd 
 |-  ( ph -> ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) e. ZZ )
28 3 27 zsubcld 
 |-  ( ph -> ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) e. ZZ )
29 inss1 
 |-  ( ( bits ` B ) i^i ( 0 ..^ N ) ) C_ ( bits ` B )
30 bitsss 
 |-  ( bits ` B ) C_ NN0
31 29 30 sstri 
 |-  ( ( bits ` B ) i^i ( 0 ..^ N ) ) C_ NN0
32 inss2 
 |-  ( ( bits ` B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
33 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( bits ` B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( bits ` B ) i^i ( 0 ..^ N ) ) e. Fin )
34 13 32 33 mp2an 
 |-  ( ( bits ` B ) i^i ( 0 ..^ N ) ) e. Fin
35 elfpw 
 |-  ( ( ( bits ` B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( bits ` B ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( bits ` B ) i^i ( 0 ..^ N ) ) e. Fin ) )
36 31 34 35 mpbir2an 
 |-  ( ( bits ` B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin )
37 24 ffvelcdmi 
 |-  ( ( ( bits ` B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) e. NN0 )
38 36 37 mp1i 
 |-  ( ph -> ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) e. NN0 )
39 38 nn0zd 
 |-  ( ph -> ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) e. ZZ )
40 4 39 zsubcld 
 |-  ( ph -> ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) e. ZZ )
41 2 fveq1i 
 |-  ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) )
42 3 8 zmodcld 
 |-  ( ph -> ( A mod ( 2 ^ N ) ) e. NN0 )
43 42 fvresd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( A mod ( 2 ^ N ) ) ) = ( bits ` ( A mod ( 2 ^ N ) ) ) )
44 bitsmod 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` ( A mod ( 2 ^ N ) ) ) = ( ( bits ` A ) i^i ( 0 ..^ N ) ) )
45 3 5 44 syl2anc 
 |-  ( ph -> ( bits ` ( A mod ( 2 ^ N ) ) ) = ( ( bits ` A ) i^i ( 0 ..^ N ) ) )
46 43 45 eqtrd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( A mod ( 2 ^ N ) ) ) = ( ( bits ` A ) i^i ( 0 ..^ N ) ) )
47 f1ocnvfv 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ ( A mod ( 2 ^ N ) ) e. NN0 ) -> ( ( ( bits |` NN0 ) ` ( A mod ( 2 ^ N ) ) ) = ( ( bits ` A ) i^i ( 0 ..^ N ) ) -> ( `' ( bits |` NN0 ) ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) = ( A mod ( 2 ^ N ) ) ) )
48 19 42 47 sylancr 
 |-  ( ph -> ( ( ( bits |` NN0 ) ` ( A mod ( 2 ^ N ) ) ) = ( ( bits ` A ) i^i ( 0 ..^ N ) ) -> ( `' ( bits |` NN0 ) ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) = ( A mod ( 2 ^ N ) ) ) )
49 46 48 mpd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) = ( A mod ( 2 ^ N ) ) )
50 41 49 eqtrid 
 |-  ( ph -> ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) = ( A mod ( 2 ^ N ) ) )
51 50 oveq2d 
 |-  ( ph -> ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) = ( A - ( A mod ( 2 ^ N ) ) ) )
52 51 oveq1d 
 |-  ( ph -> ( ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) / ( 2 ^ N ) ) = ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
53 3 zred 
 |-  ( ph -> A e. RR )
54 8 nnrpd 
 |-  ( ph -> ( 2 ^ N ) e. RR+ )
55 moddifz 
 |-  ( ( A e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) e. ZZ )
56 53 54 55 syl2anc 
 |-  ( ph -> ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) e. ZZ )
57 52 56 eqeltrd 
 |-  ( ph -> ( ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) / ( 2 ^ N ) ) e. ZZ )
58 8 nnne0d 
 |-  ( ph -> ( 2 ^ N ) =/= 0 )
59 dvdsval2 
 |-  ( ( ( 2 ^ N ) e. ZZ /\ ( 2 ^ N ) =/= 0 /\ ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) e. ZZ ) -> ( ( 2 ^ N ) || ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) <-> ( ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) / ( 2 ^ N ) ) e. ZZ ) )
60 9 58 28 59 syl3anc 
 |-  ( ph -> ( ( 2 ^ N ) || ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) <-> ( ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) / ( 2 ^ N ) ) e. ZZ ) )
61 57 60 mpbird 
 |-  ( ph -> ( 2 ^ N ) || ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) )
62 2 fveq1i 
 |-  ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) )
63 4 8 zmodcld 
 |-  ( ph -> ( B mod ( 2 ^ N ) ) e. NN0 )
64 63 fvresd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( B mod ( 2 ^ N ) ) ) = ( bits ` ( B mod ( 2 ^ N ) ) ) )
65 bitsmod 
 |-  ( ( B e. ZZ /\ N e. NN0 ) -> ( bits ` ( B mod ( 2 ^ N ) ) ) = ( ( bits ` B ) i^i ( 0 ..^ N ) ) )
66 4 5 65 syl2anc 
 |-  ( ph -> ( bits ` ( B mod ( 2 ^ N ) ) ) = ( ( bits ` B ) i^i ( 0 ..^ N ) ) )
67 64 66 eqtrd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( B mod ( 2 ^ N ) ) ) = ( ( bits ` B ) i^i ( 0 ..^ N ) ) )
68 f1ocnvfv 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ ( B mod ( 2 ^ N ) ) e. NN0 ) -> ( ( ( bits |` NN0 ) ` ( B mod ( 2 ^ N ) ) ) = ( ( bits ` B ) i^i ( 0 ..^ N ) ) -> ( `' ( bits |` NN0 ) ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) = ( B mod ( 2 ^ N ) ) ) )
69 19 63 68 sylancr 
 |-  ( ph -> ( ( ( bits |` NN0 ) ` ( B mod ( 2 ^ N ) ) ) = ( ( bits ` B ) i^i ( 0 ..^ N ) ) -> ( `' ( bits |` NN0 ) ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) = ( B mod ( 2 ^ N ) ) ) )
70 67 69 mpd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) = ( B mod ( 2 ^ N ) ) )
71 62 70 eqtrid 
 |-  ( ph -> ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) = ( B mod ( 2 ^ N ) ) )
72 71 oveq2d 
 |-  ( ph -> ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) = ( B - ( B mod ( 2 ^ N ) ) ) )
73 72 oveq1d 
 |-  ( ph -> ( ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) / ( 2 ^ N ) ) = ( ( B - ( B mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
74 4 zred 
 |-  ( ph -> B e. RR )
75 moddifz 
 |-  ( ( B e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( ( B - ( B mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) e. ZZ )
76 74 54 75 syl2anc 
 |-  ( ph -> ( ( B - ( B mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) e. ZZ )
77 73 76 eqeltrd 
 |-  ( ph -> ( ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) / ( 2 ^ N ) ) e. ZZ )
78 dvdsval2 
 |-  ( ( ( 2 ^ N ) e. ZZ /\ ( 2 ^ N ) =/= 0 /\ ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) e. ZZ ) -> ( ( 2 ^ N ) || ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) <-> ( ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) / ( 2 ^ N ) ) e. ZZ ) )
79 9 58 40 78 syl3anc 
 |-  ( ph -> ( ( 2 ^ N ) || ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) <-> ( ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) / ( 2 ^ N ) ) e. ZZ ) )
80 77 79 mpbird 
 |-  ( ph -> ( 2 ^ N ) || ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) )
81 9 28 40 61 80 dvds2addd 
 |-  ( ph -> ( 2 ^ N ) || ( ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) + ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) ) )
82 3 zcnd 
 |-  ( ph -> A e. CC )
83 4 zcnd 
 |-  ( ph -> B e. CC )
84 26 nn0cnd 
 |-  ( ph -> ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) e. CC )
85 38 nn0cnd 
 |-  ( ph -> ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) e. CC )
86 82 83 84 85 addsub4d 
 |-  ( ph -> ( ( A + B ) - ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) ) = ( ( A - ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) ) + ( B - ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) ) )
87 81 86 breqtrrd 
 |-  ( ph -> ( 2 ^ N ) || ( ( A + B ) - ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) ) )
88 3 4 zaddcld 
 |-  ( ph -> ( A + B ) e. ZZ )
89 27 39 zaddcld 
 |-  ( ph -> ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) e. ZZ )
90 moddvds 
 |-  ( ( ( 2 ^ N ) e. NN /\ ( A + B ) e. ZZ /\ ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) e. ZZ ) -> ( ( ( A + B ) mod ( 2 ^ N ) ) = ( ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) <-> ( 2 ^ N ) || ( ( A + B ) - ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) ) ) )
91 8 88 89 90 syl3anc 
 |-  ( ph -> ( ( ( A + B ) mod ( 2 ^ N ) ) = ( ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) <-> ( 2 ^ N ) || ( ( A + B ) - ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) ) ) )
92 87 91 mpbird 
 |-  ( ph -> ( ( A + B ) mod ( 2 ^ N ) ) = ( ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
93 11 a1i 
 |-  ( ph -> ( bits ` A ) C_ NN0 )
94 30 a1i 
 |-  ( ph -> ( bits ` B ) C_ NN0 )
95 93 94 1 5 2 sadadd3 
 |-  ( ph -> ( ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( ( K ` ( ( bits ` A ) i^i ( 0 ..^ N ) ) ) + ( K ` ( ( bits ` B ) i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
96 inss1 
 |-  ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) C_ ( ( bits ` A ) sadd ( bits ` B ) )
97 sadcl 
 |-  ( ( ( bits ` A ) C_ NN0 /\ ( bits ` B ) C_ NN0 ) -> ( ( bits ` A ) sadd ( bits ` B ) ) C_ NN0 )
98 11 30 97 mp2an 
 |-  ( ( bits ` A ) sadd ( bits ` B ) ) C_ NN0
99 96 98 sstri 
 |-  ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) C_ NN0
100 inss2 
 |-  ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
101 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) e. Fin )
102 13 100 101 mp2an 
 |-  ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) e. Fin
103 elfpw 
 |-  ( ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) e. Fin ) )
104 99 102 103 mpbir2an 
 |-  ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin )
105 24 ffvelcdmi 
 |-  ( ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. NN0 )
106 104 105 mp1i 
 |-  ( ph -> ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. NN0 )
107 106 nn0red 
 |-  ( ph -> ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. RR )
108 106 nn0ge0d 
 |-  ( ph -> 0 <_ ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) )
109 2 fveq1i 
 |-  ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) )
110 109 fveq2i 
 |-  ( ( bits |` NN0 ) ` ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) )
111 106 fvresd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) = ( bits ` ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) )
112 104 a1i 
 |-  ( ph -> ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
113 f1ocnvfv2 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) ) -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) )
114 19 112 113 sylancr 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) )
115 110 111 114 3eqtr3a 
 |-  ( ph -> ( bits ` ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) )
116 115 100 eqsstrdi 
 |-  ( ph -> ( bits ` ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) )
117 106 nn0zd 
 |-  ( ph -> ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. ZZ )
118 bitsfzo 
 |-  ( ( ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. ZZ /\ N e. NN0 ) -> ( ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
119 117 5 118 syl2anc 
 |-  ( ph -> ( ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
120 116 119 mpbird 
 |-  ( ph -> ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) )
121 elfzolt2 
 |-  ( ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) -> ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
122 120 121 syl 
 |-  ( ph -> ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
123 modid 
 |-  ( ( ( ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) e. RR /\ ( 2 ^ N ) e. RR+ ) /\ ( 0 <_ ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) /\ ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) ) ) -> ( ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) )
124 107 54 108 122 123 syl22anc 
 |-  ( ph -> ( ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) )
125 92 95 124 3eqtr2d 
 |-  ( ph -> ( ( A + B ) mod ( 2 ^ N ) ) = ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) )
126 125 fveq2d 
 |-  ( ph -> ( bits ` ( ( A + B ) mod ( 2 ^ N ) ) ) = ( bits ` ( K ` ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) ) ) )
127 126 115 eqtr2d 
 |-  ( ph -> ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ N ) ) = ( bits ` ( ( A + B ) mod ( 2 ^ N ) ) ) )