Step | Hyp | Ref
| Expression |
1 | | inss1 3652 |
. . . . . . . . . . 11
  ..^   |
2 | | sadasslem.1 |
. . . . . . . . . . 11

  |
3 | 1, 2 | syl5ss 3443 |
. . . . . . . . . 10
   ..^    |
4 | | fzofi 12187 |
. . . . . . . . . . . 12
 ..^  |
5 | 4 | a1i 11 |
. . . . . . . . . . 11
  ..^   |
6 | | inss2 3653 |
. . . . . . . . . . 11
  ..^   ..^  |
7 | | ssfi 7792 |
. . . . . . . . . . 11
   ..^   ..^   ..^    ..^    |
8 | 5, 6, 7 | sylancl 668 |
. . . . . . . . . 10
   ..^    |
9 | | elfpw 7876 |
. . . . . . . . . 10
   ..^        ..^  
 ..^     |
10 | 3, 8, 9 | sylanbrc 670 |
. . . . . . . . 9
   ..^       |
11 | | bitsf1o 14419 |
. . . . . . . . . . 11
bits          |
12 | | f1ocnv 5826 |
. . . . . . . . . . 11
 bits          bits
          |
13 | | f1of 5814 |
. . . . . . . . . . 11
  bits        
 bits           |
14 | 11, 12, 13 | mp2b 10 |
. . . . . . . . . 10
 bits          |
15 | 14 | ffvelrni 6021 |
. . . . . . . . 9
   ..^    
  bits    
 ..^     |
16 | 10, 15 | syl 17 |
. . . . . . . 8
   bits      ..^     |
17 | 16 | nn0cnd 10927 |
. . . . . . 7
   bits      ..^     |
18 | | inss1 3652 |
. . . . . . . . . . 11
  ..^   |
19 | | sadasslem.2 |
. . . . . . . . . . 11

  |
20 | 18, 19 | syl5ss 3443 |
. . . . . . . . . 10
   ..^    |
21 | | inss2 3653 |
. . . . . . . . . . 11
  ..^   ..^  |
22 | | ssfi 7792 |
. . . . . . . . . . 11
   ..^   ..^   ..^    ..^    |
23 | 5, 21, 22 | sylancl 668 |
. . . . . . . . . 10
   ..^    |
24 | | elfpw 7876 |
. . . . . . . . . 10
   ..^        ..^  
 ..^     |
25 | 20, 23, 24 | sylanbrc 670 |
. . . . . . . . 9
   ..^       |
26 | 14 | ffvelrni 6021 |
. . . . . . . . 9
   ..^    
  bits    
 ..^     |
27 | 25, 26 | syl 17 |
. . . . . . . 8
   bits      ..^     |
28 | 27 | nn0cnd 10927 |
. . . . . . 7
   bits      ..^     |
29 | | inss1 3652 |
. . . . . . . . . . 11
  ..^   |
30 | | sadasslem.3 |
. . . . . . . . . . 11

  |
31 | 29, 30 | syl5ss 3443 |
. . . . . . . . . 10
   ..^    |
32 | | inss2 3653 |
. . . . . . . . . . 11
  ..^   ..^  |
33 | | ssfi 7792 |
. . . . . . . . . . 11
   ..^   ..^   ..^    ..^    |
34 | 5, 32, 33 | sylancl 668 |
. . . . . . . . . 10
   ..^    |
35 | | elfpw 7876 |
. . . . . . . . . 10
   ..^        ..^  
 ..^     |
36 | 31, 34, 35 | sylanbrc 670 |
. . . . . . . . 9
   ..^       |
37 | 14 | ffvelrni 6021 |
. . . . . . . . 9
   ..^    
  bits    
 ..^     |
38 | 36, 37 | syl 17 |
. . . . . . . 8
   bits      ..^     |
39 | 38 | nn0cnd 10927 |
. . . . . . 7
   bits      ..^     |
40 | 17, 28, 39 | addassd 9665 |
. . . . . 6
     bits    
 ..^     bits    
 ..^      bits
     ..^       bits      ..^      bits
     ..^     bits    
 ..^       |
41 | 40 | oveq1d 6305 |
. . . . 5
      bits
     ..^     bits    
 ..^      bits
     ..^             bits      ..^      bits
     ..^     bits    
 ..^            |
42 | | inss1 3652 |
. . . . . . . . . 10
  sadd   ..^ 
 sadd   |
43 | | sadcl 14436 |
. . . . . . . . . . 11
 
  sadd    |
44 | 2, 19, 43 | syl2anc 667 |
. . . . . . . . . 10
  sadd    |
45 | 42, 44 | syl5ss 3443 |
. . . . . . . . 9
   sadd 
 ..^    |
46 | | inss2 3653 |
. . . . . . . . . 10
  sadd   ..^ 
 ..^  |
47 | | ssfi 7792 |
. . . . . . . . . 10
   ..^   sadd
  ..^ 
 ..^    sadd 
 ..^    |
48 | 5, 46, 47 | sylancl 668 |
. . . . . . . . 9
   sadd 
 ..^    |
49 | | elfpw 7876 |
. . . . . . . . 9
   sadd   ..^        sadd   ..^ 
  sadd
  ..^     |
50 | 45, 48, 49 | sylanbrc 670 |
. . . . . . . 8
   sadd 
 ..^       |
51 | 14 | ffvelrni 6021 |
. . . . . . . 8
   sadd   ..^       bits      sadd
  ..^     |
52 | 50, 51 | syl 17 |
. . . . . . 7
   bits      sadd 
 ..^     |
53 | 52 | nn0red 10926 |
. . . . . 6
   bits      sadd 
 ..^     |
54 | 16 | nn0red 10926 |
. . . . . . 7
   bits      ..^     |
55 | 27 | nn0red 10926 |
. . . . . . 7
   bits      ..^     |
56 | 54, 55 | readdcld 9670 |
. . . . . 6
    bits      ..^     bits      ..^      |
57 | 38 | nn0red 10926 |
. . . . . 6
   bits      ..^     |
58 | | 2rp 11307 |
. . . . . . . 8
 |
59 | 58 | a1i 11 |
. . . . . . 7
   |
60 | | sadasslem.4 |
. . . . . . . 8
   |
61 | 60 | nn0zd 11038 |
. . . . . . 7
   |
62 | 59, 61 | rpexpcld 12439 |
. . . . . 6
       |
63 | | eqid 2451 |
. . . . . . 7
      cadd 
                     
 cadd                    |
64 | | eqid 2451 |
. . . . . . 7
 bits   bits   |
65 | 2, 19, 63, 60, 64 | sadadd3 14435 |
. . . . . 6
    bits      sadd
  ..^            bits      ..^     bits    
 ..^           |
66 | | eqidd 2452 |
. . . . . 6
    bits      ..^           bits      ..^          |
67 | 53, 56, 57, 57, 62, 65, 66 | modadd12d 12146 |
. . . . 5
     bits      sadd 
 ..^     bits      ..^              bits
     ..^     bits    
 ..^      bits
     ..^           |
68 | | inss1 3652 |
. . . . . . . . . 10
  sadd   ..^ 
 sadd   |
69 | | sadcl 14436 |
. . . . . . . . . . 11
 
  sadd    |
70 | 19, 30, 69 | syl2anc 667 |
. . . . . . . . . 10
  sadd    |
71 | 68, 70 | syl5ss 3443 |
. . . . . . . . 9
   sadd 
 ..^    |
72 | | inss2 3653 |
. . . . . . . . . 10
  sadd   ..^ 
 ..^  |
73 | | ssfi 7792 |
. . . . . . . . . 10
   ..^   sadd
  ..^ 
 ..^    sadd 
 ..^    |
74 | 5, 72, 73 | sylancl 668 |
. . . . . . . . 9
   sadd 
 ..^    |
75 | | elfpw 7876 |
. . . . . . . . 9
   sadd   ..^        sadd   ..^ 
  sadd
  ..^     |
76 | 71, 74, 75 | sylanbrc 670 |
. . . . . . . 8
   sadd 
 ..^       |
77 | 14 | ffvelrni 6021 |
. . . . . . . 8
   sadd   ..^       bits      sadd
  ..^     |
78 | 76, 77 | syl 17 |
. . . . . . 7
   bits      sadd 
 ..^     |
79 | 78 | nn0red 10926 |
. . . . . 6
   bits      sadd 
 ..^     |
80 | 55, 57 | readdcld 9670 |
. . . . . 6
    bits      ..^     bits      ..^      |
81 | | eqidd 2452 |
. . . . . 6
    bits      ..^           bits      ..^          |
82 | | eqid 2451 |
. . . . . . 7
      cadd 
                     
 cadd                    |
83 | 19, 30, 82, 60, 64 | sadadd3 14435 |
. . . . . 6
    bits      sadd
  ..^            bits      ..^     bits    
 ..^           |
84 | 54, 54, 79, 80, 62, 81, 83 | modadd12d 12146 |
. . . . 5
     bits    
 ..^     bits      sadd 
 ..^             bits
     ..^      bits
     ..^     bits    
 ..^            |
85 | 41, 67, 84 | 3eqtr4d 2495 |
. . . 4
     bits      sadd 
 ..^     bits      ..^             bits    
 ..^     bits      sadd 
 ..^           |
86 | | eqid 2451 |
. . . . 5
      cadd  sadd                          cadd  sadd                     |
87 | 44, 30, 86, 60, 64 | sadadd3 14435 |
. . . 4
    bits       sadd  sadd   ..^            bits
     sadd 
 ..^     bits      ..^           |
88 | | eqid 2451 |
. . . . 5
      cadd 
 sadd                         cadd 
 sadd                    |
89 | 2, 70, 88, 60, 64 | sadadd3 14435 |
. . . 4
    bits      sadd
 sadd    ..^            bits
     ..^     bits      sadd 
 ..^           |
90 | 85, 87, 89 | 3eqtr4d 2495 |
. . 3
    bits       sadd  sadd   ..^           bits      sadd  sadd    ..^          |
91 | | inss1 3652 |
. . . . . . . 8
   sadd  sadd   ..^    sadd  sadd   |
92 | | sadcl 14436 |
. . . . . . . . 9
   sadd 

  sadd  sadd    |
93 | 44, 30, 92 | syl2anc 667 |
. . . . . . . 8
   sadd  sadd    |
94 | 91, 93 | syl5ss 3443 |
. . . . . . 7
    sadd  sadd   ..^    |
95 | | inss2 3653 |
. . . . . . . 8
   sadd  sadd   ..^   ..^  |
96 | | ssfi 7792 |
. . . . . . . 8
   ..^    sadd  sadd   ..^   ..^     sadd  sadd   ..^    |
97 | 5, 95, 96 | sylancl 668 |
. . . . . . 7
    sadd  sadd   ..^    |
98 | | elfpw 7876 |
. . . . . . 7
    sadd  sadd   ..^    
    sadd  sadd   ..^ 
   sadd  sadd   ..^     |
99 | 94, 97, 98 | sylanbrc 670 |
. . . . . 6
    sadd  sadd   ..^       |
100 | 14 | ffvelrni 6021 |
. . . . . 6
    sadd  sadd   ..^       bits
      sadd  sadd   ..^     |
101 | 99, 100 | syl 17 |
. . . . 5
   bits       sadd  sadd   ..^     |
102 | 101 | nn0red 10926 |
. . . 4
   bits       sadd  sadd   ..^     |
103 | 101 | nn0ge0d 10928 |
. . . 4

  bits       sadd  sadd   ..^     |
104 | | fvres 5879 |
. . . . . . . . 9
   bits
      sadd  sadd   ..^    bits      bits       sadd  sadd   ..^    bits   bits
      sadd  sadd   ..^      |
105 | 101, 104 | syl 17 |
. . . . . . . 8
  bits      bits       sadd  sadd   ..^    bits   bits
      sadd  sadd   ..^      |
106 | | f1ocnvfv2 6176 |
. . . . . . . . 9
  bits            sadd  sadd 
 ..^       bits      bits
      sadd  sadd   ..^       sadd  sadd 
 ..^    |
107 | 11, 99, 106 | sylancr 669 |
. . . . . . . 8
  bits      bits       sadd  sadd   ..^       sadd  sadd 
 ..^    |
108 | 105, 107 | eqtr3d 2487 |
. . . . . . 7
 bits   bits       sadd  sadd   ..^       sadd  sadd 
 ..^    |
109 | 108, 95 | syl6eqss 3482 |
. . . . . 6
 bits   bits       sadd  sadd   ..^     ..^   |
110 | 101 | nn0zd 11038 |
. . . . . . 7
   bits       sadd  sadd   ..^     |
111 | | bitsfzo 14409 |
. . . . . . 7
    bits       sadd  sadd   ..^       bits       sadd  sadd   ..^    ..^     bits   bits       sadd  sadd   ..^     ..^    |
112 | 110, 60, 111 | syl2anc 667 |
. . . . . 6
    bits       sadd  sadd   ..^    ..^    
bits   bits
      sadd  sadd   ..^     ..^    |
113 | 109, 112 | mpbird 236 |
. . . . 5
   bits       sadd  sadd   ..^    ..^       |
114 | | elfzolt2 11929 |
. . . . 5
   bits
      sadd  sadd   ..^    ..^       bits       sadd  sadd   ..^         |
115 | 113, 114 | syl 17 |
. . . 4
   bits       sadd  sadd   ..^         |
116 | | modid 12121 |
. . . 4
     bits       sadd  sadd   ..^           bits
      sadd  sadd   ..^     bits
      sadd  sadd   ..^            bits       sadd  sadd   ..^          bits       sadd  sadd   ..^     |
117 | 102, 62, 103, 115, 116 | syl22anc 1269 |
. . 3
    bits       sadd  sadd   ..^          bits       sadd  sadd   ..^     |
118 | | inss1 3652 |
. . . . . . . 8
  sadd  sadd    ..^   sadd  sadd    |
119 | | sadcl 14436 |
. . . . . . . . 9
 
 sadd    sadd  sadd     |
120 | 2, 70, 119 | syl2anc 667 |
. . . . . . . 8
  sadd  sadd     |
121 | 118, 120 | syl5ss 3443 |
. . . . . . 7
   sadd  sadd    ..^ 
  |
122 | | inss2 3653 |
. . . . . . . 8
  sadd  sadd    ..^   ..^  |
123 | | ssfi 7792 |
. . . . . . . 8
   ..^   sadd
 sadd    ..^   ..^    sadd
 sadd    ..^    |
124 | 5, 122, 123 | sylancl 668 |
. . . . . . 7
   sadd  sadd    ..^    |
125 | | elfpw 7876 |
. . . . . . 7
   sadd  sadd    ..^   
    sadd  sadd    ..^ 
  sadd
 sadd    ..^     |
126 | 121, 124,
125 | sylanbrc 670 |
. . . . . 6
   sadd  sadd    ..^   
   |
127 | 14 | ffvelrni 6021 |
. . . . . 6
   sadd  sadd    ..^   
   bits      sadd  sadd    ..^     |
128 | 126, 127 | syl 17 |
. . . . 5
   bits      sadd  sadd    ..^     |
129 | 128 | nn0red 10926 |
. . . 4
   bits      sadd  sadd    ..^     |
130 | | 2nn 10767 |
. . . . . . 7
 |
131 | 130 | a1i 11 |
. . . . . 6
   |
132 | 131, 60 | nnexpcld 12437 |
. . . . 5
       |
133 | 132 | nnrpd 11339 |
. . . 4
       |
134 | 128 | nn0ge0d 10928 |
. . . 4

  bits      sadd  sadd    ..^     |
135 | | fvres 5879 |
. . . . . . . . 9
   bits
     sadd  sadd    ..^    bits      bits      sadd  sadd    ..^    bits   bits      sadd  sadd    ..^      |
136 | 128, 135 | syl 17 |
. . . . . . . 8
  bits      bits      sadd  sadd    ..^    bits   bits      sadd  sadd    ..^      |
137 | | f1ocnvfv2 6176 |
. . . . . . . . 9
  bits           sadd  sadd    ..^       bits      bits
     sadd  sadd    ..^      sadd  sadd    ..^    |
138 | 11, 126, 137 | sylancr 669 |
. . . . . . . 8
  bits      bits      sadd  sadd    ..^      sadd  sadd    ..^    |
139 | 136, 138 | eqtr3d 2487 |
. . . . . . 7
 bits   bits      sadd  sadd    ..^      sadd  sadd    ..^    |
140 | 139, 122 | syl6eqss 3482 |
. . . . . 6
 bits   bits      sadd  sadd    ..^     ..^   |
141 | 128 | nn0zd 11038 |
. . . . . . 7
   bits      sadd  sadd    ..^     |
142 | | bitsfzo 14409 |
. . . . . . 7
    bits      sadd  sadd    ..^       bits      sadd
 sadd    ..^    ..^    
bits   bits
     sadd  sadd    ..^     ..^    |
143 | 141, 60, 142 | syl2anc 667 |
. . . . . 6
    bits      sadd
 sadd    ..^    ..^    
bits   bits
     sadd  sadd    ..^     ..^    |
144 | 140, 143 | mpbird 236 |
. . . . 5
   bits      sadd  sadd    ..^    ..^       |
145 | | elfzolt2 11929 |
. . . . 5
   bits
     sadd  sadd    ..^    ..^       bits      sadd  sadd    ..^         |
146 | 144, 145 | syl 17 |
. . . 4
   bits      sadd  sadd    ..^         |
147 | | modid 12121 |
. . . 4
     bits      sadd
 sadd    ..^           bits
     sadd  sadd    ..^     bits
     sadd  sadd    ..^            bits      sadd  sadd    ..^          bits      sadd  sadd    ..^     |
148 | 129, 133,
134, 146, 147 | syl22anc 1269 |
. . 3
    bits      sadd
 sadd    ..^          bits      sadd
 sadd    ..^     |
149 | 90, 117, 148 | 3eqtr3d 2493 |
. 2
   bits       sadd  sadd   ..^     bits      sadd  sadd    ..^     |
150 | | f1of1 5813 |
. . . . 5
  bits        
 bits           |
151 | 11, 12, 150 | mp2b 10 |
. . . 4
 bits          |
152 | | f1fveq 6163 |
. . . 4
   bits
            sadd  sadd 
 ..^       sadd  sadd    ..^          bits       sadd  sadd   ..^     bits      sadd  sadd    ..^  
   sadd
 sadd   ..^    sadd  sadd    ..^     |
153 | 151, 152 | mpan 676 |
. . 3
     sadd  sadd   ..^       sadd  sadd    ..^         bits       sadd  sadd   ..^     bits      sadd  sadd    ..^  
   sadd
 sadd   ..^    sadd  sadd    ..^     |
154 | 99, 126, 153 | syl2anc 667 |
. 2
    bits       sadd  sadd   ..^     bits      sadd  sadd    ..^  
   sadd
 sadd   ..^    sadd  sadd    ..^     |
155 | 149, 154 | mpbid 214 |
1
    sadd  sadd   ..^    sadd  sadd    ..^    |