Step | Hyp | Ref
| Expression |
1 | | inss1 3529 |
. . . . . . . . 9
  sadd   ..^ 
 sadd   |
2 | | sadval.a |
. . . . . . . . . . 11

  |
3 | | sadval.b |
. . . . . . . . . . 11

  |
4 | | sadval.c |
. . . . . . . . . . 11
   
 cadd 
                  |
5 | 2, 3, 4 | sadfval 12927 |
. . . . . . . . . 10
  sadd  
hadd           |
6 | | ssrab2 3396 |
. . . . . . . . . 10

hadd          |
7 | 5, 6 | syl6eqss 3366 |
. . . . . . . . 9
  sadd    |
8 | 1, 7 | syl5ss 3327 |
. . . . . . . 8
   sadd 
 ..^    |
9 | | fzofi 11276 |
. . . . . . . . . 10
 ..^  |
10 | 9 | a1i 11 |
. . . . . . . . 9
  ..^   |
11 | | inss2 3530 |
. . . . . . . . 9
  sadd   ..^ 
 ..^  |
12 | | ssfi 7296 |
. . . . . . . . 9
   ..^   sadd
  ..^ 
 ..^    sadd 
 ..^    |
13 | 10, 11, 12 | sylancl 644 |
. . . . . . . 8
   sadd 
 ..^    |
14 | | elfpw 7374 |
. . . . . . . 8
   sadd   ..^        sadd   ..^ 
  sadd
  ..^     |
15 | 8, 13, 14 | sylanbrc 646 |
. . . . . . 7
   sadd 
 ..^       |
16 | | bitsf1o 12920 |
. . . . . . . . . 10
bits          |
17 | | f1ocnv 5654 |
. . . . . . . . . 10
 bits          bits
          |
18 | | f1of 5641 |
. . . . . . . . . 10
  bits        
 bits           |
19 | 16, 17, 18 | mp2b 10 |
. . . . . . . . 9
 bits          |
20 | | sadcadd.k |
. . . . . . . . . 10
 bits
  |
21 | 20 | feq1i 5552 |
. . . . . . . . 9
       
 bits           |
22 | 19, 21 | mpbir 201 |
. . . . . . . 8
        |
23 | 22 | ffvelrni 5836 |
. . . . . . 7
   sadd   ..^          sadd 
 ..^     |
24 | 15, 23 | syl 16 |
. . . . . 6
      sadd
  ..^     |
25 | 24 | nn0cnd 10240 |
. . . . 5
      sadd
  ..^     |
26 | | 2nn0 10202 |
. . . . . . . . . 10
 |
27 | 26 | a1i 11 |
. . . . . . . . 9
   |
28 | | sadcp1.n |
. . . . . . . . 9
   |
29 | 27, 28 | nn0expcld 11508 |
. . . . . . . 8
       |
30 | | 0nn0 10200 |
. . . . . . . 8
 |
31 | | ifcl 3743 |
. . . . . . . 8
     
    sadd           |
32 | 29, 30, 31 | sylancl 644 |
. . . . . . 7
    sadd           |
33 | 32 | nn0cnd 10240 |
. . . . . 6
    sadd           |
34 | | 1nn0 10201 |
. . . . . . . . . . 11
 |
35 | 34 | a1i 11 |
. . . . . . . . . 10
   |
36 | 28, 35 | nn0addcld 10242 |
. . . . . . . . 9
     |
37 | 27, 36 | nn0expcld 11508 |
. . . . . . . 8
    
    |
38 | | ifcl 3743 |
. . . . . . . 8
     
 
  
                 |
39 | 37, 30, 38 | sylancl 644 |
. . . . . . 7
                    |
40 | 39 | nn0cnd 10240 |
. . . . . 6
                    |
41 | 33, 40 | addcld 9071 |
. . . . 5
     sadd                     
       |
42 | 25, 41 | addcld 9071 |
. . . 4
       sadd 
 ..^       sadd                              |
43 | | inss1 3529 |
. . . . . . . . . 10
  ..^   |
44 | 43, 2 | syl5ss 3327 |
. . . . . . . . 9
   ..^    |
45 | | inss2 3530 |
. . . . . . . . . 10
  ..^   ..^  |
46 | | ssfi 7296 |
. . . . . . . . . 10
   ..^   ..^   ..^    ..^    |
47 | 10, 45, 46 | sylancl 644 |
. . . . . . . . 9
   ..^    |
48 | | elfpw 7374 |
. . . . . . . . 9
   ..^        ..^  
 ..^     |
49 | 44, 47, 48 | sylanbrc 646 |
. . . . . . . 8
   ..^       |
50 | 22 | ffvelrni 5836 |
. . . . . . . 8
   ..^    
     ..^     |
51 | 49, 50 | syl 16 |
. . . . . . 7
      ..^     |
52 | 51 | nn0cnd 10240 |
. . . . . 6
      ..^     |
53 | | inss1 3529 |
. . . . . . . . . 10
  ..^   |
54 | 53, 3 | syl5ss 3327 |
. . . . . . . . 9
   ..^    |
55 | | inss2 3530 |
. . . . . . . . . 10
  ..^   ..^  |
56 | | ssfi 7296 |
. . . . . . . . . 10
   ..^   ..^   ..^    ..^    |
57 | 10, 55, 56 | sylancl 644 |
. . . . . . . . 9
   ..^    |
58 | | elfpw 7374 |
. . . . . . . . 9
   ..^        ..^  
 ..^     |
59 | 54, 57, 58 | sylanbrc 646 |
. . . . . . . 8
   ..^       |
60 | 22 | ffvelrni 5836 |
. . . . . . . 8
   ..^    
     ..^     |
61 | 59, 60 | syl 16 |
. . . . . . 7
      ..^     |
62 | 61 | nn0cnd 10240 |
. . . . . 6
      ..^     |
63 | 52, 62 | addcld 9071 |
. . . . 5
     
 ..^        ..^      |
64 | | ifcl 3743 |
. . . . . . . 8
     
            |
65 | 29, 30, 64 | sylancl 644 |
. . . . . . 7
            |
66 | 65 | nn0cnd 10240 |
. . . . . 6
            |
67 | | ifcl 3743 |
. . . . . . . 8
     
            |
68 | 29, 30, 67 | sylancl 644 |
. . . . . . 7
            |
69 | 68 | nn0cnd 10240 |
. . . . . 6
            |
70 | 66, 69 | addcld 9071 |
. . . . 5
                       |
71 | 63, 70 | addcld 9071 |
. . . 4
        ..^        ..^               
           |
72 | 29 | nn0cnd 10240 |
. . . . . 6
       |
73 | 72 | adantr 452 |
. . . . 5
 
    
      |
74 | | 0cn 9048 |
. . . . . 6
 |
75 | 74 | a1i 11 |
. . . . 5
 
    
  |
76 | 73, 75 | ifclda 3734 |
. . . 4
                |
77 | | sadadd2lem.1 |
. . . . . 6
       sadd 
 ..^                     
 ..^        ..^      |
78 | 2, 3, 4, 28 | sadval 12931 |
. . . . . . . . 9
   sadd 
hadd           |
79 | 78 | ifbid 3725 |
. . . . . . . 8
    sadd          hadd 
               |
80 | 2, 3, 4, 28 | sadcp1 12930 |
. . . . . . . . 9
 
      cadd

         |
81 | 27 | nn0cnd 10240 |
. . . . . . . . . . 11
   |
82 | 81, 28 | expp1d 11487 |
. . . . . . . . . 10
    
          |
83 | 72, 81 | mulcomd 9073 |
. . . . . . . . . 10
               |
84 | 82, 83 | eqtrd 2444 |
. . . . . . . . 9
    
          |
85 | | eqidd 2413 |
. . . . . . . . 9
   |
86 | 80, 84, 85 | ifbieq12d 3729 |
. . . . . . . 8
                   cadd 
                 |
87 | 79, 86 | oveq12d 6066 |
. . . . . . 7
     sadd                     
       hadd                cadd 
                  |
88 | | sadadd2lem2 12925 |
. . . . . . . 8
       hadd                cadd 
                                                     |
89 | 72, 88 | syl 16 |
. . . . . . 7
   hadd 
              cadd 
                            
                        |
90 | 87, 89 | eqtrd 2444 |
. . . . . 6
     sadd                     
                 
                        |
91 | 77, 90 | oveq12d 6066 |
. . . . 5
        sadd   ..^    
                sadd                                   ..^        ..^                                          |
92 | 25, 41, 76 | add32d 9252 |
. . . . 5
        sadd   ..^       sadd              
                                  sadd   ..^    
                sadd                              |
93 | 63, 70, 76 | addassd 9074 |
. . . . 5
         ..^        ..^                          
                   ..^        ..^                          
               |
94 | 91, 92, 93 | 3eqtr4d 2454 |
. . . 4
        sadd   ..^       sadd              
                                   ..^        ..^                          
              |
95 | 42, 71, 76, 94 | addcan2ad 9236 |
. . 3
       sadd 
 ..^       sadd                                   ..^        ..^               
           |
96 | 25, 33, 40 | addassd 9074 |
. . 3
        sadd   ..^      sadd               
                  sadd 
 ..^       sadd                              |
97 | 52, 66, 62, 69 | add4d 9253 |
. . 3
        ..^                   ..^                     ..^        ..^                           |
98 | 95, 96, 97 | 3eqtr4d 2454 |
. 2
        sadd   ..^      sadd               
                   ..^                   ..^                |
99 | 20 | bitsinvp1 12924 |
. . . 4
   sadd 
      sadd   ..^           sadd   ..^    
 sadd            |
100 | 7, 28, 99 | syl2anc 643 |
. . 3
      sadd
  ..^           sadd
  ..^    
 sadd            |
101 | 100 | oveq1d 6063 |
. 2
       sadd 
 ..^          
                   sadd   ..^      sadd               
              |
102 | 20 | bitsinvp1 12924 |
. . . 4
 
      ..^           ..^               |
103 | 2, 28, 102 | syl2anc 643 |
. . 3
      ..^         
 ..^               |
104 | 20 | bitsinvp1 12924 |
. . . 4
 
      ..^           ..^               |
105 | 3, 28, 104 | syl2anc 643 |
. . 3
      ..^         
 ..^               |
106 | 103, 105 | oveq12d 6066 |
. 2
     
 ..^          ..^           
 ..^                   ..^                |
107 | 98, 101, 106 | 3eqtr4d 2454 |
1
       sadd 
 ..^          
                
 ..^          ..^        |