Proof of Theorem sadcaddlem
Step | Hyp | Ref
| Expression |
1 | | cad1 1521 |
. . . . 5
    
cadd

     

    |
2 | 1 | adantl 468 |
. . . 4
 
    
cadd

     

    |
3 | | 2nn 10774 |
. . . . . . . . . . 11
 |
4 | 3 | a1i 11 |
. . . . . . . . . 10
   |
5 | | sadcp1.n |
. . . . . . . . . 10
   |
6 | 4, 5 | nnexpcld 12444 |
. . . . . . . . 9
       |
7 | 6 | nnred 10631 |
. . . . . . . 8
       |
8 | 7 | ad2antrr 733 |
. . . . . . 7
                 |
9 | | inss1 3654 |
. . . . . . . . . . . . 13
  ..^   |
10 | | sadval.a |
. . . . . . . . . . . . 13

  |
11 | 9, 10 | syl5ss 3445 |
. . . . . . . . . . . 12
   ..^    |
12 | | fzofi 12194 |
. . . . . . . . . . . . . 14
 ..^  |
13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
  ..^   |
14 | | inss2 3655 |
. . . . . . . . . . . . 13
  ..^   ..^  |
15 | | ssfi 7797 |
. . . . . . . . . . . . 13
   ..^   ..^   ..^    ..^    |
16 | 13, 14, 15 | sylancl 669 |
. . . . . . . . . . . 12
   ..^    |
17 | | elfpw 7881 |
. . . . . . . . . . . 12
   ..^        ..^  
 ..^     |
18 | 11, 16, 17 | sylanbrc 671 |
. . . . . . . . . . 11
   ..^       |
19 | | bitsf1o 14431 |
. . . . . . . . . . . . . . 15
bits          |
20 | | f1ocnv 5831 |
. . . . . . . . . . . . . . 15
 bits          bits
          |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . 14
 bits          |
22 | | sadcadd.k |
. . . . . . . . . . . . . . 15
 bits
  |
23 | | f1oeq1 5810 |
. . . . . . . . . . . . . . 15
  bits           bits
           |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
         bits
          |
25 | 21, 24 | mpbir 213 |
. . . . . . . . . . . . 13
        |
26 | | f1of 5819 |
. . . . . . . . . . . . 13
       
         |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
        |
28 | 27 | ffvelrni 6026 |
. . . . . . . . . . 11
   ..^    
     ..^     |
29 | 18, 28 | syl 17 |
. . . . . . . . . 10
      ..^     |
30 | | inss1 3654 |
. . . . . . . . . . . . 13
  ..^   |
31 | | sadval.b |
. . . . . . . . . . . . 13

  |
32 | 30, 31 | syl5ss 3445 |
. . . . . . . . . . . 12
   ..^    |
33 | | inss2 3655 |
. . . . . . . . . . . . 13
  ..^   ..^  |
34 | | ssfi 7797 |
. . . . . . . . . . . . 13
   ..^   ..^   ..^    ..^    |
35 | 13, 33, 34 | sylancl 669 |
. . . . . . . . . . . 12
   ..^    |
36 | | elfpw 7881 |
. . . . . . . . . . . 12
   ..^        ..^  
 ..^     |
37 | 32, 35, 36 | sylanbrc 671 |
. . . . . . . . . . 11
   ..^       |
38 | 27 | ffvelrni 6026 |
. . . . . . . . . . 11
   ..^    
     ..^     |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
      ..^     |
40 | 29, 39 | nn0addcld 10936 |
. . . . . . . . 9
     
 ..^        ..^      |
41 | 40 | nn0red 10933 |
. . . . . . . 8
     
 ..^        ..^      |
42 | 41 | ad2antrr 733 |
. . . . . . 7
               
 ..^        ..^      |
43 | | 2nn0 10893 |
. . . . . . . . . . . . 13
 |
44 | 43 | a1i 11 |
. . . . . . . . . . . 12
 
   |
45 | 5 | adantr 467 |
. . . . . . . . . . . 12
 
   |
46 | 44, 45 | nn0expcld 12445 |
. . . . . . . . . . 11
 
       |
47 | | 0nn0 10891 |
. . . . . . . . . . . 12
 |
48 | 47 | a1i 11 |
. . . . . . . . . . 11
 
   |
49 | 46, 48 | ifclda 3915 |
. . . . . . . . . 10
            |
50 | 43 | a1i 11 |
. . . . . . . . . . . 12
 
   |
51 | 5 | adantr 467 |
. . . . . . . . . . . 12
 
   |
52 | 50, 51 | nn0expcld 12445 |
. . . . . . . . . . 11
 
       |
53 | 47 | a1i 11 |
. . . . . . . . . . 11
 
   |
54 | 52, 53 | ifclda 3915 |
. . . . . . . . . 10
            |
55 | 49, 54 | nn0addcld 10936 |
. . . . . . . . 9
                       |
56 | 55 | nn0red 10933 |
. . . . . . . 8
                       |
57 | 56 | ad2antrr 733 |
. . . . . . 7
                                 |
58 | | sadcaddlem.1 |
. . . . . . . . 9
 
              ..^        ..^       |
59 | 58 | biimpa 487 |
. . . . . . . 8
 
    
        
 ..^        ..^      |
60 | 59 | adantr 467 |
. . . . . . 7
              
      ..^        ..^      |
61 | 6 | nnnn0d 10932 |
. . . . . . . . . . . . 13
       |
62 | | ifcl 3925 |
. . . . . . . . . . . . 13
     
            |
63 | 61, 47, 62 | sylancl 669 |
. . . . . . . . . . . 12
            |
64 | 63 | nn0ge0d 10935 |
. . . . . . . . . . 11

 
         |
65 | 7 | adantr 467 |
. . . . . . . . . . . . 13
 
       |
66 | | 0red 9649 |
. . . . . . . . . . . . 13
 
   |
67 | 65, 66 | ifclda 3915 |
. . . . . . . . . . . 12
            |
68 | 7, 67 | addge01d 10208 |
. . . . . . . . . . 11
   
                             |
69 | 64, 68 | mpbid 214 |
. . . . . . . . . 10
    
                 |
70 | 69 | ad2antrr 733 |
. . . . . . . . 9
                              |
71 | | iftrue 3889 |
. . . . . . . . . . 11
  
             |
72 | 71 | adantl 468 |
. . . . . . . . . 10
          
             |
73 | 72 | oveq1d 6310 |
. . . . . . . . 9
                                              |
74 | 70, 73 | breqtrrd 4432 |
. . . . . . . 8
                                   |
75 | | ifcl 3925 |
. . . . . . . . . . . . 13
     
            |
76 | 61, 47, 75 | sylancl 669 |
. . . . . . . . . . . 12
            |
77 | 76 | nn0ge0d 10935 |
. . . . . . . . . . 11

 
         |
78 | 7 | adantr 467 |
. . . . . . . . . . . . 13
 
       |
79 | | 0red 9649 |
. . . . . . . . . . . . 13
 
   |
80 | 78, 79 | ifclda 3915 |
. . . . . . . . . . . 12
            |
81 | 7, 80 | addge02d 10209 |
. . . . . . . . . . 11
   
                             |
82 | 77, 81 | mpbid 214 |
. . . . . . . . . 10
    
  
              |
83 | 82 | ad2antrr 733 |
. . . . . . . . 9
                              |
84 | | iftrue 3889 |
. . . . . . . . . . 11
  
             |
85 | 84 | adantl 468 |
. . . . . . . . . 10
          
             |
86 | 85 | oveq2d 6311 |
. . . . . . . . 9
                                              |
87 | 83, 86 | breqtrrd 4432 |
. . . . . . . 8
                                   |
88 | 74, 87 | jaodan 795 |
. . . . . . 7
              
  
                   |
89 | 8, 8, 42, 57, 60, 88 | le2addd 10239 |
. . . . . 6
                    
       ..^        ..^                           |
90 | 89 | ex 436 |
. . . . 5
 
    
 
          
       ..^        ..^                            |
91 | | ioran 493 |
. . . . . 6
 
 
   |
92 | | iffalse 3892 |
. . . . . . . . . . . . . 14
            |
93 | 92 | ad2antrl 735 |
. . . . . . . . . . . . 13
        
   
         |
94 | | iffalse 3892 |
. . . . . . . . . . . . . 14
            |
95 | 94 | ad2antll 736 |
. . . . . . . . . . . . 13
        
   
         |
96 | 93, 95 | oveq12d 6313 |
. . . . . . . . . . . 12
        
                          |
97 | | 00id 9813 |
. . . . . . . . . . . 12
   |
98 | 96, 97 | syl6eq 2503 |
. . . . . . . . . . 11
        
                        |
99 | 98 | oveq2d 6311 |
. . . . . . . . . 10
        
       
 ..^        ..^               
                ..^        ..^       |
100 | 29 | nn0red 10933 |
. . . . . . . . . . . . . 14
      ..^     |
101 | 100 | ad2antrr 733 |
. . . . . . . . . . . . 13
        
       ..^     |
102 | 39 | nn0red 10933 |
. . . . . . . . . . . . . 14
      ..^     |
103 | 102 | ad2antrr 733 |
. . . . . . . . . . . . 13
        
       ..^     |
104 | 101, 103 | readdcld 9675 |
. . . . . . . . . . . 12
        
        ..^        ..^      |
105 | 104 | recnd 9674 |
. . . . . . . . . . 11
        
        ..^        ..^      |
106 | 105 | addid1d 9838 |
. . . . . . . . . 10
        
       
 ..^        ..^           ..^        ..^      |
107 | 99, 106 | eqtrd 2487 |
. . . . . . . . 9
        
       
 ..^        ..^               
             
 ..^        ..^      |
108 | 22 | fveq1i 5871 |
. . . . . . . . . . . . . . . 16
     ..^     bits    
 ..^    |
109 | 108 | fveq2i 5873 |
. . . . . . . . . . . . . . 15
 bits         ..^     bits      bits      ..^     |
110 | | fvres 5884 |
. . . . . . . . . . . . . . . 16
      ..^    bits         ..^    bits      ..^      |
111 | 29, 110 | syl 17 |
. . . . . . . . . . . . . . 15
  bits         ..^    bits      ..^      |
112 | | f1ocnvfv2 6181 |
. . . . . . . . . . . . . . . 16
  bits           ..^       bits      bits      ..^      ..^    |
113 | 19, 18, 112 | sylancr 670 |
. . . . . . . . . . . . . . 15
  bits      bits      ..^      ..^    |
114 | 109, 111,
113 | 3eqtr3a 2511 |
. . . . . . . . . . . . . 14
 bits      ..^      ..^    |
115 | 114, 14 | syl6eqss 3484 |
. . . . . . . . . . . . 13
 bits      ..^     ..^   |
116 | 29 | nn0zd 11045 |
. . . . . . . . . . . . . 14
      ..^     |
117 | | bitsfzo 14421 |
. . . . . . . . . . . . . 14
       ..^          ..^    ..^     bits      ..^     ..^    |
118 | 116, 5, 117 | syl2anc 667 |
. . . . . . . . . . . . 13
     
 ..^    ..^    
bits      ..^     ..^    |
119 | 115, 118 | mpbird 236 |
. . . . . . . . . . . 12
      ..^    ..^       |
120 | | elfzolt2 11936 |
. . . . . . . . . . . 12
      ..^    ..^        
 ..^         |
121 | 119, 120 | syl 17 |
. . . . . . . . . . 11
      ..^         |
122 | 22 | fveq1i 5871 |
. . . . . . . . . . . . . . . 16
     ..^     bits    
 ..^    |
123 | 122 | fveq2i 5873 |
. . . . . . . . . . . . . . 15
 bits         ..^     bits      bits      ..^     |
124 | | fvres 5884 |
. . . . . . . . . . . . . . . 16
      ..^    bits         ..^    bits      ..^      |
125 | 39, 124 | syl 17 |
. . . . . . . . . . . . . . 15
  bits         ..^    bits      ..^      |
126 | | f1ocnvfv2 6181 |
. . . . . . . . . . . . . . . 16
  bits           ..^       bits      bits      ..^      ..^    |
127 | 19, 37, 126 | sylancr 670 |
. . . . . . . . . . . . . . 15
  bits      bits      ..^      ..^    |
128 | 123, 125,
127 | 3eqtr3a 2511 |
. . . . . . . . . . . . . 14
 bits      ..^      ..^    |
129 | 128, 33 | syl6eqss 3484 |
. . . . . . . . . . . . 13
 bits      ..^     ..^   |
130 | 39 | nn0zd 11045 |
. . . . . . . . . . . . . 14
      ..^     |
131 | | bitsfzo 14421 |
. . . . . . . . . . . . . 14
       ..^          ..^    ..^     bits      ..^     ..^    |
132 | 130, 5, 131 | syl2anc 667 |
. . . . . . . . . . . . 13
     
 ..^    ..^    
bits      ..^     ..^    |
133 | 129, 132 | mpbird 236 |
. . . . . . . . . . . 12
      ..^    ..^       |
134 | | elfzolt2 11936 |
. . . . . . . . . . . 12
      ..^    ..^        
 ..^         |
135 | 133, 134 | syl 17 |
. . . . . . . . . . 11
      ..^         |
136 | 100, 102,
7, 7, 121, 135 | lt2addd 10243 |
. . . . . . . . . 10
     
 ..^        ..^                |
137 | 136 | ad2antrr 733 |
. . . . . . . . 9
        
        ..^        ..^                |
138 | 107, 137 | eqbrtrd 4426 |
. . . . . . . 8
        
       
 ..^        ..^               
                     |
139 | 80 | ad2antrr 733 |
. . . . . . . . . . 11
        
   
         |
140 | 67 | ad2antrr 733 |
. . . . . . . . . . 11
        
   
         |
141 | 139, 140 | readdcld 9675 |
. . . . . . . . . 10
        
                        |
142 | 104, 141 | readdcld 9675 |
. . . . . . . . 9
        
       
 ..^        ..^               
           |
143 | 7 | ad2antrr 733 |
. . . . . . . . . 10
        
        |
144 | 143, 143 | readdcld 9675 |
. . . . . . . . 9
        
              |
145 | 142, 144 | ltnled 9787 |
. . . . . . . 8
        
          ..^        ..^               
                  
                 ..^        ..^               
            |
146 | 138, 145 | mpbid 214 |
. . . . . . 7
        
           
       ..^        ..^                           |
147 | 146 | ex 436 |
. . . . . 6
 
    
 

                 ..^        ..^                            |
148 | 91, 147 | syl5bi 221 |
. . . . 5
 
    
 

                 ..^        ..^                            |
149 | 90, 148 | impcon4bid 209 |
. . . 4
 
    
 
                  ..^        ..^                            |
150 | 2, 149 | bitrd 257 |
. . 3
 
    
cadd

     
                 ..^        ..^               
            |
151 | | cad0 1522 |
. . . . 5
     cadd

      
    |
152 | 151 | adantl 468 |
. . . 4
 
    
cadd

     

    |
153 | 40 | nn0ge0d 10935 |
. . . . . . . . 9

      ..^        ..^      |
154 | 7, 7 | readdcld 9675 |
. . . . . . . . . 10
             |
155 | 154, 41 | addge02d 10209 |
. . . . . . . . 9
        ..^        ..^             
       ..^        ..^                  |
156 | 153, 155 | mpbid 214 |
. . . . . . . 8
          
       ..^        ..^                 |
157 | 156 | ad2antrr 733 |
. . . . . . 7
        
                   ..^        ..^                 |
158 | 71, 84 | oveqan12d 6314 |
. . . . . . . . 9
 
                                 |
159 | 158 | adantl 468 |
. . . . . . . 8
        
                                  |
160 | 159 | oveq2d 6311 |
. . . . . . 7
        
       
 ..^        ..^               
                ..^        ..^                 |
161 | 157, 160 | breqtrrd 4432 |
. . . . . 6
        
                   ..^        ..^                           |
162 | 161 | ex 436 |
. . . . 5
 
    
 
          
       ..^        ..^                            |
163 | 100 | adantr 467 |
. . . . . . . . . 10
 
    
     ..^     |
164 | 102 | adantr 467 |
. . . . . . . . . 10
 
    
     ..^     |
165 | 163, 164 | readdcld 9675 |
. . . . . . . . 9
 
    
      ..^        ..^      |
166 | 7 | adantr 467 |
. . . . . . . . 9
 
    
      |
167 | 7, 41 | lenltd 9786 |
. . . . . . . . . . . 12
            ..^        ..^        
 ..^        ..^           |
168 | 58, 167 | bitrd 257 |
. . . . . . . . . . 11
 
        
 ..^        ..^           |
169 | 168 | con2bid 331 |
. . . . . . . . . 10
        ..^        ..^               |
170 | 169 | biimpar 488 |
. . . . . . . . 9
 
    
      ..^        ..^          |
171 | 165, 166,
166, 170 | ltadd1dd 10231 |
. . . . . . . 8
 
    
       ..^        ..^                     |
172 | 165, 166 | readdcld 9675 |
. . . . . . . . 9
 
    
       ..^        ..^           |
173 | 154 | adantr 467 |
. . . . . . . . 9
 
    
            |
174 | 41, 56 | readdcld 9675 |
. . . . . . . . . 10
        ..^        ..^               
           |
175 | 174 | adantr 467 |
. . . . . . . . 9
 
    
       ..^        ..^                           |
176 | | ltletr 9730 |
. . . . . . . . 9
         ..^        ..^                          ..^        ..^               
                   ..^        ..^                                    ..^        ..^               
                 ..^        ..^                ..^        ..^               
            |
177 | 172, 173,
175, 176 | syl3anc 1269 |
. . . . . . . 8
 
    
         ..^        ..^                            
       ..^        ..^                               
 ..^        ..^                ..^        ..^                            |
178 | 171, 177 | mpand 682 |
. . . . . . 7
 
    
                  ..^        ..^                        
       ..^        ..^                ..^        ..^               
            |
179 | 56 | adantr 467 |
. . . . . . . 8
 
    
  
                   |
180 | 41 | adantr 467 |
. . . . . . . 8
 
    
      ..^        ..^      |
181 | 166, 179,
180 | ltadd2d 9796 |
. . . . . . 7
 
    
                                ..^        ..^                ..^        ..^                            |
182 | 178, 181 | sylibrd 238 |
. . . . . 6
 
    
                  ..^        ..^                        
                           |
183 | 7, 56 | ltnled 9787 |
. . . . . . . 8
                         
  
                
       |
184 | 63 | nn0cnd 10934 |
. . . . . . . . . . . . 13
            |
185 | 184 | addid2d 9839 |
. . . . . . . . . . . 12
   
                   |
186 | 7 | leidd 10187 |
. . . . . . . . . . . . 13
    
      |
187 | 61 | nn0ge0d 10935 |
. . . . . . . . . . . . 13

      |
188 | | breq1 4408 |
. . . . . . . . . . . . . 14
                                       |
189 | | breq1 4408 |
. . . . . . . . . . . . . 14
                               |
190 | 188, 189 | ifboth 3919 |
. . . . . . . . . . . . 13
     
                 
      |
191 | 186, 187,
190 | syl2anc 667 |
. . . . . . . . . . . 12
                |
192 | 185, 191 | eqbrtrd 4426 |
. . . . . . . . . . 11
   
              |
193 | 92 | oveq1d 6310 |
. . . . . . . . . . . 12
                       
          |
194 | 193 | breq1d 4415 |
. . . . . . . . . . 11
                         
                  |
195 | 192, 194 | syl5ibrcom 226 |
. . . . . . . . . 10
 
  
                
       |
196 | 195 | con1d 128 |
. . . . . . . . 9
                     
   
   |
197 | 76 | nn0cnd 10934 |
. . . . . . . . . . . . 13
            |
198 | 197 | addid1d 9838 |
. . . . . . . . . . . 12
                       |
199 | | breq1 4408 |
. . . . . . . . . . . . . 14
                                       |
200 | | breq1 4408 |
. . . . . . . . . . . . . 14
                               |
201 | 199, 200 | ifboth 3919 |
. . . . . . . . . . . . 13
     
                 
      |
202 | 186, 187,
201 | syl2anc 667 |
. . . . . . . . . . . 12
                |
203 | 198, 202 | eqbrtrd 4426 |
. . . . . . . . . . 11
                  |
204 | 94 | oveq2d 6311 |
. . . . . . . . . . . 12
                                  |
205 | 204 | breq1d 4415 |
. . . . . . . . . . 11
                         
  
               |
206 | 203, 205 | syl5ibrcom 226 |
. . . . . . . . . 10
 
  
                
       |
207 | 206 | con1d 128 |
. . . . . . . . 9
                     
   
   |
208 | 196, 207 | jcad 536 |
. . . . . . . 8
                     
    
    |
209 | 183, 208 | sylbid 219 |
. . . . . . 7
                         

    |
210 | 209 | adantr 467 |
. . . . . 6
 
    
                              |
211 | 182, 210 | syld 45 |
. . . . 5
 
    
                  ..^        ..^                        

    |
212 | 162, 211 | impbid 194 |
. . . 4
 
    
 
                  ..^        ..^                            |
213 | 152, 212 | bitrd 257 |
. . 3
 
    
cadd

     
                 ..^        ..^               
            |
214 | 150, 213 | pm2.61dan 801 |
. 2
 cadd                       
 ..^        ..^               
            |
215 | | sadval.c |
. . 3
    
 cadd 
                  |
216 | 10, 31, 215, 5 | sadcp1 14441 |
. 2
 
      cadd

         |
217 | | 2cnd 10689 |
. . . . 5
   |
218 | 217, 5 | expp1d 12424 |
. . . 4
    
          |
219 | 6 | nncnd 10632 |
. . . . 5
       |
220 | 219 | times2d 10863 |
. . . 4
                   |
221 | 218, 220 | eqtrd 2487 |
. . 3
    
              |
222 | 22 | bitsinvp1 14435 |
. . . . . 6
 
      ..^           ..^               |
223 | 10, 5, 222 | syl2anc 667 |
. . . . 5
      ..^         
 ..^               |
224 | 22 | bitsinvp1 14435 |
. . . . . 6
 
      ..^           ..^               |
225 | 31, 5, 224 | syl2anc 667 |
. . . . 5
      ..^         
 ..^               |
226 | 223, 225 | oveq12d 6313 |
. . . 4
     
 ..^          ..^           
 ..^                   ..^                |
227 | 29 | nn0cnd 10934 |
. . . . 5
      ..^     |
228 | 39 | nn0cnd 10934 |
. . . . 5
      ..^     |
229 | 227, 197,
228, 184 | add4d 9863 |
. . . 4
        ..^                   ..^                     ..^        ..^                           |
230 | 226, 229 | eqtrd 2487 |
. . 3
     
 ..^          ..^           
 ..^        ..^               
           |
231 | 221, 230 | breq12d 4418 |
. 2
              ..^          ..^               
       ..^        ..^                            |
232 | 214, 216,
231 | 3bitr4d 289 |
1
 
         
 
      ..^          ..^         |