Proof of Theorem sadaddlem
Step | Hyp | Ref
| Expression |
1 | | sadaddlem.k |
. . . . . . . . . . . . 13
 bits
  |
2 | 1 | fveq1i 5866 |
. . . . . . . . . . . 12
    bits   ..^     bits     bits   ..^    |
3 | | sadaddlem.1 |
. . . . . . . . . . . . . . . 16
   |
4 | | 2nn 10767 |
. . . . . . . . . . . . . . . . . 18
 |
5 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   |
6 | | sadaddlem.3 |
. . . . . . . . . . . . . . . . 17
   |
7 | 5, 6 | nnexpcld 12437 |
. . . . . . . . . . . . . . . 16
       |
8 | 3, 7 | zmodcld 12117 |
. . . . . . . . . . . . . . 15
         |
9 | | fvres 5879 |
. . . . . . . . . . . . . . 15
      
 bits           bits          |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . 14
  bits           bits          |
11 | | bitsmod 14410 |
. . . . . . . . . . . . . . 15
 
 bits         bits 
 ..^    |
12 | 3, 6, 11 | syl2anc 667 |
. . . . . . . . . . . . . 14
 bits         bits 
 ..^    |
13 | 10, 12 | eqtrd 2485 |
. . . . . . . . . . . . 13
  bits            bits   ..^    |
14 | | bitsf1o 14419 |
. . . . . . . . . . . . . 14
bits          |
15 | | f1ocnvfv 6177 |
. . . . . . . . . . . . . 14
  bits                  bits            bits   ..^    bits     bits   ..^            |
16 | 14, 8, 15 | sylancr 669 |
. . . . . . . . . . . . 13
   bits            bits   ..^ 
  bits     bits   ..^            |
17 | 13, 16 | mpd 15 |
. . . . . . . . . . . 12
   bits     bits 
 ..^           |
18 | 2, 17 | syl5eq 2497 |
. . . . . . . . . . 11
     bits   ..^           |
19 | 18 | oveq2d 6306 |
. . . . . . . . . 10
      bits   ..^              |
20 | 19 | oveq1d 6305 |
. . . . . . . . 9
       bits   ..^                         |
21 | 3 | zred 11040 |
. . . . . . . . . 10
   |
22 | 7 | nnrpd 11339 |
. . . . . . . . . 10
       |
23 | | moddifz 12109 |
. . . . . . . . . 10
         
             |
24 | 21, 22, 23 | syl2anc 667 |
. . . . . . . . 9
   
             |
25 | 20, 24 | eqeltrd 2529 |
. . . . . . . 8
       bits   ..^           |
26 | 7 | nnzd 11039 |
. . . . . . . . 9
       |
27 | 7 | nnne0d 10654 |
. . . . . . . . 9
       |
28 | | inss1 3652 |
. . . . . . . . . . . . . 14
 bits   ..^  bits   |
29 | | bitsss 14399 |
. . . . . . . . . . . . . 14
bits   |
30 | 28, 29 | sstri 3441 |
. . . . . . . . . . . . 13
 bits   ..^   |
31 | | fzofi 12187 |
. . . . . . . . . . . . . 14
 ..^  |
32 | | inss2 3653 |
. . . . . . . . . . . . . 14
 bits   ..^   ..^  |
33 | | ssfi 7792 |
. . . . . . . . . . . . . 14
   ..^  bits   ..^ 
 ..^   bits 
 ..^    |
34 | 31, 32, 33 | mp2an 678 |
. . . . . . . . . . . . 13
 bits   ..^   |
35 | | elfpw 7876 |
. . . . . . . . . . . . 13
  bits   ..^   
   bits 
 ..^   bits   ..^     |
36 | 30, 34, 35 | mpbir2an 931 |
. . . . . . . . . . . 12
 bits   ..^      |
37 | | f1ocnv 5826 |
. . . . . . . . . . . . . . 15
 bits          bits
          |
38 | | f1of 5814 |
. . . . . . . . . . . . . . 15
  bits        
 bits           |
39 | 14, 37, 38 | mp2b 10 |
. . . . . . . . . . . . . 14
 bits          |
40 | 1 | feq1i 5720 |
. . . . . . . . . . . . . 14
       
 bits           |
41 | 39, 40 | mpbir 213 |
. . . . . . . . . . . . 13
        |
42 | 41 | ffvelrni 6021 |
. . . . . . . . . . . 12
  bits   ..^   
     bits   ..^     |
43 | 36, 42 | mp1i 13 |
. . . . . . . . . . 11
     bits   ..^     |
44 | 43 | nn0zd 11038 |
. . . . . . . . . 10
     bits   ..^     |
45 | 3, 44 | zsubcld 11045 |
. . . . . . . . 9
      bits   ..^      |
46 | | dvdsval2 14308 |
. . . . . . . . 9
               bits   ..^          
    bits   ..^   
 
    bits 
 ..^            |
47 | 26, 27, 45, 46 | syl3anc 1268 |
. . . . . . . 8
      
    bits 
 ..^          bits   ..^            |
48 | 25, 47 | mpbird 236 |
. . . . . . 7
    
     bits   ..^      |
49 | 1 | fveq1i 5866 |
. . . . . . . . . . . 12
    bits   ..^     bits     bits   ..^    |
50 | | sadaddlem.2 |
. . . . . . . . . . . . . . . 16
   |
51 | 50, 7 | zmodcld 12117 |
. . . . . . . . . . . . . . 15
         |
52 | | fvres 5879 |
. . . . . . . . . . . . . . 15
      
 bits           bits          |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . 14
  bits           bits          |
54 | | bitsmod 14410 |
. . . . . . . . . . . . . . 15
 
 bits         bits 
 ..^    |
55 | 50, 6, 54 | syl2anc 667 |
. . . . . . . . . . . . . 14
 bits         bits 
 ..^    |
56 | 53, 55 | eqtrd 2485 |
. . . . . . . . . . . . 13
  bits            bits   ..^    |
57 | | f1ocnvfv 6177 |
. . . . . . . . . . . . . 14
  bits                  bits            bits   ..^    bits     bits   ..^            |
58 | 14, 51, 57 | sylancr 669 |
. . . . . . . . . . . . 13
   bits            bits   ..^ 
  bits     bits   ..^            |
59 | 56, 58 | mpd 15 |
. . . . . . . . . . . 12
   bits     bits 
 ..^           |
60 | 49, 59 | syl5eq 2497 |
. . . . . . . . . . 11
     bits   ..^           |
61 | 60 | oveq2d 6306 |
. . . . . . . . . 10
      bits   ..^              |
62 | 61 | oveq1d 6305 |
. . . . . . . . 9
       bits   ..^                         |
63 | 50 | zred 11040 |
. . . . . . . . . 10
   |
64 | | moddifz 12109 |
. . . . . . . . . 10
         
             |
65 | 63, 22, 64 | syl2anc 667 |
. . . . . . . . 9
   
             |
66 | 62, 65 | eqeltrd 2529 |
. . . . . . . 8
       bits   ..^           |
67 | | inss1 3652 |
. . . . . . . . . . . . . 14
 bits   ..^  bits   |
68 | | bitsss 14399 |
. . . . . . . . . . . . . 14
bits   |
69 | 67, 68 | sstri 3441 |
. . . . . . . . . . . . 13
 bits   ..^   |
70 | | inss2 3653 |
. . . . . . . . . . . . . 14
 bits   ..^   ..^  |
71 | | ssfi 7792 |
. . . . . . . . . . . . . 14
   ..^  bits   ..^ 
 ..^   bits 
 ..^    |
72 | 31, 70, 71 | mp2an 678 |
. . . . . . . . . . . . 13
 bits   ..^   |
73 | | elfpw 7876 |
. . . . . . . . . . . . 13
  bits   ..^   
   bits 
 ..^   bits   ..^     |
74 | 69, 72, 73 | mpbir2an 931 |
. . . . . . . . . . . 12
 bits   ..^      |
75 | 41 | ffvelrni 6021 |
. . . . . . . . . . . 12
  bits   ..^   
     bits   ..^     |
76 | 74, 75 | mp1i 13 |
. . . . . . . . . . 11
     bits   ..^     |
77 | 76 | nn0zd 11038 |
. . . . . . . . . 10
     bits   ..^     |
78 | 50, 77 | zsubcld 11045 |
. . . . . . . . 9
      bits   ..^      |
79 | | dvdsval2 14308 |
. . . . . . . . 9
               bits   ..^          
    bits   ..^   
 
    bits 
 ..^            |
80 | 26, 27, 78, 79 | syl3anc 1268 |
. . . . . . . 8
      
    bits 
 ..^          bits   ..^            |
81 | 66, 80 | mpbird 236 |
. . . . . . 7
    
     bits   ..^      |
82 | | dvds2add 14334 |
. . . . . . . 8
      
    bits   ..^         bits   ..^                bits   ..^             bits   ..^        
 
    bits 
 ..^         bits   ..^        |
83 | 26, 45, 78, 82 | syl3anc 1268 |
. . . . . . 7
       
    bits   ..^             bits   ..^        
 
    bits 
 ..^         bits   ..^        |
84 | 48, 81, 83 | mp2and 685 |
. . . . . 6
    
 
    bits 
 ..^         bits   ..^       |
85 | 3 | zcnd 11041 |
. . . . . . 7
   |
86 | 50 | zcnd 11041 |
. . . . . . 7
   |
87 | 43 | nn0cnd 10927 |
. . . . . . 7
     bits   ..^     |
88 | 76 | nn0cnd 10927 |
. . . . . . 7
     bits   ..^     |
89 | 85, 86, 87, 88 | addsub4d 10033 |
. . . . . 6
         bits   ..^       bits   ..^           bits   ..^         bits   ..^       |
90 | 84, 89 | breqtrrd 4429 |
. . . . 5
    
 
      bits   ..^       bits   ..^       |
91 | 3, 50 | zaddcld 11044 |
. . . . . 6
     |
92 | 44, 77 | zaddcld 11044 |
. . . . . 6
      bits   ..^       bits   ..^      |
93 | | moddvds 14312 |
. . . . . 6
      
      bits   ..^       bits   ..^                    bits   ..^       bits   ..^                     bits   ..^       bits   ..^        |
94 | 7, 91, 92, 93 | syl3anc 1268 |
. . . . 5
                bits   ..^       bits   ..^                     bits   ..^       bits   ..^        |
95 | 90, 94 | mpbird 236 |
. . . 4
               bits   ..^       bits   ..^           |
96 | 29 | a1i 11 |
. . . . 5
 bits    |
97 | 68 | a1i 11 |
. . . . 5
 bits    |
98 | | sadaddlem.c |
. . . . 5
    
 cadd bits   bits                    |
99 | 96, 97, 98, 6, 1 | sadadd3 14435 |
. . . 4
       bits  sadd
bits    ..^              bits   ..^       bits   ..^           |
100 | | inss1 3652 |
. . . . . . . . 9
  bits  sadd bits    ..^   bits  sadd bits    |
101 | | sadcl 14436 |
. . . . . . . . . 10
  bits 
bits 
  bits  sadd bits  
  |
102 | 29, 68, 101 | mp2an 678 |
. . . . . . . . 9
 bits  sadd bits    |
103 | 100, 102 | sstri 3441 |
. . . . . . . 8
  bits  sadd bits    ..^   |
104 | | inss2 3653 |
. . . . . . . . 9
  bits  sadd bits    ..^   ..^  |
105 | | ssfi 7792 |
. . . . . . . . 9
   ..^   bits  sadd bits  
 ..^   ..^    bits  sadd bits    ..^    |
106 | 31, 104, 105 | mp2an 678 |
. . . . . . . 8
  bits  sadd bits    ..^   |
107 | | elfpw 7876 |
. . . . . . . 8
   bits  sadd bits  
 ..^        bits  sadd bits    ..^    bits  sadd
bits    ..^     |
108 | 103, 106,
107 | mpbir2an 931 |
. . . . . . 7
  bits  sadd bits    ..^      |
109 | 41 | ffvelrni 6021 |
. . . . . . 7
   bits  sadd bits  
 ..^    
     bits  sadd
bits    ..^     |
110 | 108, 109 | mp1i 13 |
. . . . . 6
      bits  sadd bits  
 ..^     |
111 | 110 | nn0red 10926 |
. . . . 5
      bits  sadd bits  
 ..^     |
112 | 110 | nn0ge0d 10928 |
. . . . 5

     bits  sadd
bits    ..^     |
113 | 1 | fveq1i 5866 |
. . . . . . . . . 10
     bits  sadd bits    ..^     bits
     bits  sadd
bits    ..^    |
114 | 113 | fveq2i 5868 |
. . . . . . . . 9
 bits         bits  sadd bits    ..^     bits      bits      bits  sadd
bits    ..^     |
115 | | fvres 5879 |
. . . . . . . . . 10
      bits  sadd bits    ..^    bits         bits  sadd bits  
 ..^    bits      bits  sadd bits    ..^      |
116 | 110, 115 | syl 17 |
. . . . . . . . 9
  bits         bits  sadd bits  
 ..^    bits      bits  sadd bits    ..^      |
117 | 108 | a1i 11 |
. . . . . . . . . 10
   bits  sadd
bits    ..^       |
118 | | f1ocnvfv2 6176 |
. . . . . . . . . 10
  bits           bits  sadd bits    ..^   
 
 bits      bits
     bits  sadd
bits    ..^      bits  sadd bits  
 ..^    |
119 | 14, 117, 118 | sylancr 669 |
. . . . . . . . 9
  bits      bits      bits  sadd
bits    ..^      bits  sadd bits  
 ..^    |
120 | 114, 116,
119 | 3eqtr3a 2509 |
. . . . . . . 8
 bits      bits  sadd
bits    ..^      bits  sadd bits  
 ..^    |
121 | 120, 104 | syl6eqss 3482 |
. . . . . . 7
 bits      bits  sadd
bits    ..^     ..^   |
122 | 110 | nn0zd 11038 |
. . . . . . . 8
      bits  sadd bits  
 ..^     |
123 | | bitsfzo 14409 |
. . . . . . . 8
       bits  sadd bits  
 ..^          bits  sadd bits  
 ..^    ..^     bits      bits  sadd
bits    ..^     ..^    |
124 | 122, 6, 123 | syl2anc 667 |
. . . . . . 7
       bits  sadd
bits    ..^    ..^    
bits      bits  sadd bits    ..^     ..^    |
125 | 121, 124 | mpbird 236 |
. . . . . 6
      bits  sadd bits  
 ..^    ..^       |
126 | | elfzolt2 11929 |
. . . . . 6
      bits  sadd bits    ..^    ..^          bits  sadd
bits    ..^         |
127 | 125, 126 | syl 17 |
. . . . 5
      bits  sadd bits  
 ..^         |
128 | | modid 12121 |
. . . . 5
        bits  sadd
bits    ..^              bits  sadd bits    ..^        bits  sadd bits    ..^               bits  sadd
bits    ..^             bits  sadd
bits    ..^     |
129 | 111, 22, 112, 127, 128 | syl22anc 1269 |
. . . 4
       bits  sadd
bits    ..^             bits  sadd
bits    ..^     |
130 | 95, 99, 129 | 3eqtr2d 2491 |
. . 3
              bits  sadd bits    ..^     |
131 | 130 | fveq2d 5869 |
. 2
 bits  
       bits      bits  sadd
bits    ..^      |
132 | 131, 120 | eqtr2d 2486 |
1
   bits  sadd
bits    ..^  bits   
        |