Metamath Proof Explorer

Theorem sadeq

Description: Any element of a sequence sum only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses sadeq.a 
|- ( ph -> A C_ NN0 )
sadeq.b 
|- ( ph -> B C_ NN0 )
sadeq.n 
|- ( ph -> N e. NN0 )
Assertion sadeq 
|- ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) = ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 sadeq.a 
 |-  ( ph -> A C_ NN0 )
2 sadeq.b 
 |-  ( ph -> B C_ NN0 )
3 sadeq.n 
 |-  ( ph -> N e. NN0 )
4 inass 
 |-  ( ( A i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) = ( A i^i ( ( 0 ..^ N ) i^i ( 0 ..^ N ) ) )
5 inidm 
 |-  ( ( 0 ..^ N ) i^i ( 0 ..^ N ) ) = ( 0 ..^ N )
6 5 ineq2i 
 |-  ( A i^i ( ( 0 ..^ N ) i^i ( 0 ..^ N ) ) ) = ( A i^i ( 0 ..^ N ) )
7 4 6 eqtri 
 |-  ( ( A i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) = ( A i^i ( 0 ..^ N ) )
8 7 fveq2i 
 |-  ( `' ( bits |` NN0 ) ` ( ( A i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) )
9 inass 
 |-  ( ( B i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) = ( B i^i ( ( 0 ..^ N ) i^i ( 0 ..^ N ) ) )
10 5 ineq2i 
 |-  ( B i^i ( ( 0 ..^ N ) i^i ( 0 ..^ N ) ) ) = ( B i^i ( 0 ..^ N ) )
11 9 10 eqtri 
 |-  ( ( B i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) = ( B i^i ( 0 ..^ N ) )
12 11 fveq2i 
 |-  ( `' ( bits |` NN0 ) ` ( ( B i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) )
13 8 12 oveq12i 
 |-  ( ( `' ( bits |` NN0 ) ` ( ( A i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( ( B i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) )
14 13 oveq1i 
 |-  ( ( ( `' ( bits |` NN0 ) ` ( ( A i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( ( B i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) = ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) )
15 inss1 
 |-  ( A i^i ( 0 ..^ N ) ) C_ A
16 15 1 sstrid 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) C_ NN0 )
17 inss1 
 |-  ( B i^i ( 0 ..^ N ) ) C_ B
18 17 2 sstrid 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) C_ NN0 )
19 eqid 
 |-  seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. ( A i^i ( 0 ..^ N ) ) , m e. ( B i^i ( 0 ..^ N ) ) , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. ( A i^i ( 0 ..^ N ) ) , m e. ( B i^i ( 0 ..^ N ) ) , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
20 eqid 
 |-  `' ( bits |` NN0 ) = `' ( bits |` NN0 )
21 16 18 19 3 20 sadadd3 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( ( `' ( bits |` NN0 ) ` ( ( A i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( ( B i^i ( 0 ..^ N ) ) i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
22 eqid 
 |-  seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
23 1 2 22 3 20 sadadd3 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
24 14 21 23 3eqtr4a 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) )
25 inss1 
 |-  ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) C_ ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) )
26 sadcl 
 |-  ( ( ( A i^i ( 0 ..^ N ) ) C_ NN0 /\ ( B i^i ( 0 ..^ N ) ) C_ NN0 ) -> ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) C_ NN0 )
27 16 18 26 syl2anc 
 |-  ( ph -> ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) C_ NN0 )
28 25 27 sstrid 
 |-  ( ph -> ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) C_ NN0 )
29 fzofi 
 |-  ( 0 ..^ N ) e. Fin
30 29 a1i 
 |-  ( ph -> ( 0 ..^ N ) e. Fin )
31 inss2 
 |-  ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
32 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) e. Fin )
33 30 31 32 sylancl 
 |-  ( ph -> ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) e. Fin )
34 elfpw 
 |-  ( ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) e. Fin ) )
35 28 33 34 sylanbrc 
 |-  ( ph -> ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
36 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
37 f1ocnv 
 |-  ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
38 f1of 
 |-  ( `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
39 36 37 38 mp2b 
 |-  `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0
40 39 ffvelcdmi 
 |-  ( ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. NN0 )
41 35 40 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. NN0 )
42 41 nn0red 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. RR )
43 2rp 
 |-  2 e. RR+
44 43 a1i 
 |-  ( ph -> 2 e. RR+ )
45 3 nn0zd 
 |-  ( ph -> N e. ZZ )
46 44 45 rpexpcld 
 |-  ( ph -> ( 2 ^ N ) e. RR+ )
47 41 nn0ge0d 
 |-  ( ph -> 0 <_ ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) )
48 41 fvresd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) ) = ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) ) )
49 f1ocnvfv2 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) ) -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )
50 36 35 49 sylancr 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )
51 48 50 eqtr3d 
 |-  ( ph -> ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )
52 51 31 eqsstrdi 
 |-  ( ph -> ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) )
53 41 nn0zd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. ZZ )
54 bitsfzo 
 |-  ( ( ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. ZZ /\ N e. NN0 ) -> ( ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
55 53 3 54 syl2anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
56 52 55 mpbird 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) )
57 elfzolt2 
 |-  ( ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) -> ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
58 56 57 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
59 modid 
 |-  ( ( ( ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) e. RR /\ ( 2 ^ N ) e. RR+ ) /\ ( 0 <_ ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) /\ ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) ) ) -> ( ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) )
60 42 46 47 58 59 syl22anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) )
61 inss1 
 |-  ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( A sadd B )
62 sadcl 
 |-  ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A sadd B ) C_ NN0 )
63 1 2 62 syl2anc 
 |-  ( ph -> ( A sadd B ) C_ NN0 )
64 61 63 sstrid 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ NN0 )
65 inss2 
 |-  ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
66 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin )
67 30 65 66 sylancl 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin )
68 elfpw 
 |-  ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin ) )
69 64 67 68 sylanbrc 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
70 39 ffvelcdmi 
 |-  ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. NN0 )
71 69 70 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. NN0 )
72 71 nn0red 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. RR )
73 71 nn0ge0d 
 |-  ( ph -> 0 <_ ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) )
74 71 fvresd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) = ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) )
75 f1ocnvfv2 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) ) -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) = ( ( A sadd B ) i^i ( 0 ..^ N ) ) )
76 36 69 75 sylancr 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) = ( ( A sadd B ) i^i ( 0 ..^ N ) ) )
77 74 76 eqtr3d 
 |-  ( ph -> ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) = ( ( A sadd B ) i^i ( 0 ..^ N ) ) )
78 77 65 eqsstrdi 
 |-  ( ph -> ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) )
79 71 nn0zd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. ZZ )
80 bitsfzo 
 |-  ( ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. ZZ /\ N e. NN0 ) -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
81 79 3 80 syl2anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
82 78 81 mpbird 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) )
83 elfzolt2 
 |-  ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
84 82 83 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
85 modid 
 |-  ( ( ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. RR /\ ( 2 ^ N ) e. RR+ ) /\ ( 0 <_ ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) /\ ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) ) ) -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) )
86 72 46 73 84 85 syl22anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) )
87 24 60 86 3eqtr3rd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) )
88 f1of1 
 |-  ( `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-> NN0 )
89 36 37 88 mp2b 
 |-  `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-> NN0
90 f1fveq 
 |-  ( ( `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-> NN0 /\ ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) /\ ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) ) ) -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) <-> ( ( A sadd B ) i^i ( 0 ..^ N ) ) = ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) )
91 89 90 mpan 
 |-  ( ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) /\ ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) ) -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) <-> ( ( A sadd B ) i^i ( 0 ..^ N ) ) = ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) )
92 69 35 91 syl2anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) <-> ( ( A sadd B ) i^i ( 0 ..^ N ) ) = ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) )
93 87 92 mpbid 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) = ( ( ( A i^i ( 0 ..^ N ) ) sadd ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )