Metamath Proof Explorer

Theorem sadasslem

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

Ref Expression
Hypotheses sadasslem.1 
|- ( ph -> A C_ NN0 )
sadasslem.2 
|- ( ph -> B C_ NN0 )
sadasslem.3 
|- ( ph -> C C_ NN0 )
sadasslem.4 
|- ( ph -> N e. NN0 )
Assertion sadasslem 
|- ( ph -> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) = ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 sadasslem.1 
 |-  ( ph -> A C_ NN0 )
2 sadasslem.2 
 |-  ( ph -> B C_ NN0 )
3 sadasslem.3 
 |-  ( ph -> C C_ NN0 )
4 sadasslem.4 
 |-  ( ph -> N e. NN0 )
5 inss1 
 |-  ( A i^i ( 0 ..^ N ) ) C_ A
6 5 1 sstrid 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) C_ NN0 )
7 fzofi 
 |-  ( 0 ..^ N ) e. Fin
8 7 a1i 
 |-  ( ph -> ( 0 ..^ N ) e. Fin )
9 inss2 
 |-  ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
10 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( A i^i ( 0 ..^ N ) ) e. Fin )
11 8 9 10 sylancl 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) e. Fin )
12 elfpw 
 |-  ( ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( A i^i ( 0 ..^ N ) ) C_ NN0 /\ ( A i^i ( 0 ..^ N ) ) e. Fin ) )
13 6 11 12 sylanbrc 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
14 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
15 f1ocnv 
 |-  ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
16 f1of 
 |-  ( `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
17 14 15 16 mp2b 
 |-  `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0
18 17 ffvelcdmi 
 |-  ( ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) e. NN0 )
19 13 18 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) e. NN0 )
20 19 nn0cnd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) e. CC )
21 inss1 
 |-  ( B i^i ( 0 ..^ N ) ) C_ B
22 21 2 sstrid 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) C_ NN0 )
23 inss2 
 |-  ( B i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
24 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( B i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( B i^i ( 0 ..^ N ) ) e. Fin )
25 8 23 24 sylancl 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) e. Fin )
26 elfpw 
 |-  ( ( B i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( B i^i ( 0 ..^ N ) ) C_ NN0 /\ ( B i^i ( 0 ..^ N ) ) e. Fin ) )
27 22 25 26 sylanbrc 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
28 17 ffvelcdmi 
 |-  ( ( B i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) e. NN0 )
29 27 28 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) e. NN0 )
30 29 nn0cnd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) e. CC )
31 inss1 
 |-  ( C i^i ( 0 ..^ N ) ) C_ C
32 31 3 sstrid 
 |-  ( ph -> ( C i^i ( 0 ..^ N ) ) C_ NN0 )
33 inss2 
 |-  ( C i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
34 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( C i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( C i^i ( 0 ..^ N ) ) e. Fin )
35 8 33 34 sylancl 
 |-  ( ph -> ( C i^i ( 0 ..^ N ) ) e. Fin )
36 elfpw 
 |-  ( ( C i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( C i^i ( 0 ..^ N ) ) C_ NN0 /\ ( C i^i ( 0 ..^ N ) ) e. Fin ) )
37 32 35 36 sylanbrc 
 |-  ( ph -> ( C i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
38 17 ffvelcdmi 
 |-  ( ( C i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) e. NN0 )
39 37 38 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) e. NN0 )
40 39 nn0cnd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) e. CC )
41 20 30 40 addassd 
 |-  ( ph -> ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) = ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) ) )
42 41 oveq1d 
 |-  ( ph -> ( ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) = ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) ) mod ( 2 ^ N ) ) )
43 inss1 
 |-  ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( A sadd B )
44 sadcl 
 |-  ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A sadd B ) C_ NN0 )
45 1 2 44 syl2anc 
 |-  ( ph -> ( A sadd B ) C_ NN0 )
46 43 45 sstrid 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ NN0 )
47 inss2 
 |-  ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
48 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin )
49 8 47 48 sylancl 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin )
50 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 ) )
51 46 49 50 sylanbrc 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
52 17 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 )
53 51 52 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. NN0 )
54 53 nn0red 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. RR )
55 19 nn0red 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) e. RR )
56 29 nn0red 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) e. RR )
57 55 56 readdcld 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) ) e. RR )
58 39 nn0red 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) e. RR )
59 2rp 
 |-  2 e. RR+
60 59 a1i 
 |-  ( ph -> 2 e. RR+ )
61 4 nn0zd 
 |-  ( ph -> N e. ZZ )
62 60 61 rpexpcld 
 |-  ( ph -> ( 2 ^ N ) e. RR+ )
63 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 ) ) ) )
64 eqid 
 |-  `' ( bits |` NN0 ) = `' ( bits |` NN0 )
65 1 2 63 4 64 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 ) ) )
66 eqidd 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) )
67 54 57 58 58 62 65 66 modadd12d 
 |-  ( ph -> ( ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) = ( ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
68 inss1 
 |-  ( ( B sadd C ) i^i ( 0 ..^ N ) ) C_ ( B sadd C )
69 sadcl 
 |-  ( ( B C_ NN0 /\ C C_ NN0 ) -> ( B sadd C ) C_ NN0 )
70 2 3 69 syl2anc 
 |-  ( ph -> ( B sadd C ) C_ NN0 )
71 68 70 sstrid 
 |-  ( ph -> ( ( B sadd C ) i^i ( 0 ..^ N ) ) C_ NN0 )
72 inss2 
 |-  ( ( B sadd C ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
73 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( B sadd C ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( B sadd C ) i^i ( 0 ..^ N ) ) e. Fin )
74 8 72 73 sylancl 
 |-  ( ph -> ( ( B sadd C ) i^i ( 0 ..^ N ) ) e. Fin )
75 elfpw 
 |-  ( ( ( B sadd C ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( B sadd C ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( B sadd C ) i^i ( 0 ..^ N ) ) e. Fin ) )
76 71 74 75 sylanbrc 
 |-  ( ph -> ( ( B sadd C ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
77 17 ffvelcdmi 
 |-  ( ( ( B sadd C ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( `' ( bits |` NN0 ) ` ( ( B sadd C ) i^i ( 0 ..^ N ) ) ) e. NN0 )
78 76 77 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( B sadd C ) i^i ( 0 ..^ N ) ) ) e. NN0 )
79 78 nn0red 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( B sadd C ) i^i ( 0 ..^ N ) ) ) e. RR )
80 56 58 readdcld 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) e. RR )
81 eqidd 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) )
82 eqid 
 |-  seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. B , m e. C , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. B , m e. C , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
83 2 3 82 4 64 sadadd3 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( B sadd C ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
84 55 55 79 80 62 81 83 modadd12d 
 |-  ( ph -> ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( ( B sadd C ) i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) = ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) ) mod ( 2 ^ N ) ) )
85 42 67 84 3eqtr4d 
 |-  ( ph -> ( ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) = ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( ( B sadd C ) i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
86 eqid 
 |-  seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. ( A sadd B ) , m e. C , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. ( A sadd B ) , m e. C , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
87 45 3 86 4 64 sadadd3 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( ( `' ( bits |` NN0 ) ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( C i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
88 eqid 
 |-  seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. ( B sadd C ) , (/) 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 sadd C ) , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
89 1 70 88 4 64 sadadd3 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) + ( `' ( bits |` NN0 ) ` ( ( B sadd C ) i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
90 85 87 89 3eqtr4d 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) )
91 inss1 
 |-  ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) C_ ( ( A sadd B ) sadd C )
92 sadcl 
 |-  ( ( ( A sadd B ) C_ NN0 /\ C C_ NN0 ) -> ( ( A sadd B ) sadd C ) C_ NN0 )
93 45 3 92 syl2anc 
 |-  ( ph -> ( ( A sadd B ) sadd C ) C_ NN0 )
94 91 93 sstrid 
 |-  ( ph -> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) C_ NN0 )
95 inss2 
 |-  ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
96 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) e. Fin )
97 8 95 96 sylancl 
 |-  ( ph -> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) e. Fin )
98 elfpw 
 |-  ( ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) e. Fin ) )
99 94 97 98 sylanbrc 
 |-  ( ph -> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
100 17 ffvelcdmi 
 |-  ( ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. NN0 )
101 99 100 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. NN0 )
102 101 nn0red 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. RR )
103 101 nn0ge0d 
 |-  ( ph -> 0 <_ ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) )
104 101 fvresd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) ) = ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) ) )
105 f1ocnvfv2 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) ) -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) ) = ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) )
106 14 99 105 sylancr 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) ) = ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) )
107 104 106 eqtr3d 
 |-  ( ph -> ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) ) = ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) )
108 107 95 eqsstrdi 
 |-  ( ph -> ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) )
109 101 nn0zd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. ZZ )
110 bitsfzo 
 |-  ( ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. ZZ /\ N e. NN0 ) -> ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
111 109 4 110 syl2anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
112 108 111 mpbird 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) )
113 elfzolt2 
 |-  ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) -> ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
114 112 113 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
115 modid 
 |-  ( ( ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) e. RR /\ ( 2 ^ N ) e. RR+ ) /\ ( 0 <_ ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) /\ ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) ) ) -> ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) )
116 102 62 103 114 115 syl22anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) )
117 inss1 
 |-  ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) C_ ( A sadd ( B sadd C ) )
118 sadcl 
 |-  ( ( A C_ NN0 /\ ( B sadd C ) C_ NN0 ) -> ( A sadd ( B sadd C ) ) C_ NN0 )
119 1 70 118 syl2anc 
 |-  ( ph -> ( A sadd ( B sadd C ) ) C_ NN0 )
120 117 119 sstrid 
 |-  ( ph -> ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) C_ NN0 )
121 inss2 
 |-  ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
122 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) e. Fin )
123 8 121 122 sylancl 
 |-  ( ph -> ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) e. Fin )
124 elfpw 
 |-  ( ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) e. Fin ) )
125 120 123 124 sylanbrc 
 |-  ( ph -> ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
126 17 ffvelcdmi 
 |-  ( ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. NN0 )
127 125 126 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. NN0 )
128 127 nn0red 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. RR )
129 2nn 
 |-  2 e. NN
130 129 a1i 
 |-  ( ph -> 2 e. NN )
131 130 4 nnexpcld 
 |-  ( ph -> ( 2 ^ N ) e. NN )
132 131 nnrpd 
 |-  ( ph -> ( 2 ^ N ) e. RR+ )
133 127 nn0ge0d 
 |-  ( ph -> 0 <_ ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) )
134 127 fvresd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) ) = ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) ) )
135 f1ocnvfv2 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) ) -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) )
136 14 125 135 sylancr 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) )
137 134 136 eqtr3d 
 |-  ( ph -> ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) ) = ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) )
138 137 121 eqsstrdi 
 |-  ( ph -> ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) )
139 127 nn0zd 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. ZZ )
140 bitsfzo 
 |-  ( ( ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. ZZ /\ N e. NN0 ) -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
141 139 4 140 syl2anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
142 138 141 mpbird 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) )
143 elfzolt2 
 |-  ( ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) -> ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
144 142 143 syl 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
145 modid 
 |-  ( ( ( ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) e. RR /\ ( 2 ^ N ) e. RR+ ) /\ ( 0 <_ ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) /\ ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) ) ) -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) )
146 128 132 133 144 145 syl22anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) )
147 90 116 146 3eqtr3d 
 |-  ( ph -> ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) )
148 f1of1 
 |-  ( `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-> NN0 )
149 14 15 148 mp2b 
 |-  `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-> NN0
150 f1fveq 
 |-  ( ( `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-> NN0 /\ ( ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) /\ ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) ) ) -> ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) <-> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) = ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) )
151 149 150 mpan 
 |-  ( ( ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) /\ ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) ) -> ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) <-> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) = ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) )
152 99 125 151 syl2anc 
 |-  ( ph -> ( ( `' ( bits |` NN0 ) ` ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) <-> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) = ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) ) )
153 147 152 mpbid 
 |-  ( ph -> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ N ) ) = ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ N ) ) )