Proof of Theorem superpos
| Step | Hyp | Ref
| Expression |
| 1 | | reeanv 1825 |
. . . 4
                                           |
| 2 | | neeq1 1637 |
. . . . . . . . . . 11
                 |
| 3 | | neeq2 1638 |
. . . . . . . . . . 11
                             |
| 4 | 2, 3 | sylan9bb 551 |
. . . . . . . . . 10
                               |
| 5 | 4 | adantl 397 |
. . . . . . . . 9
     
                                 |
| 6 | | neeq1 1637 |
. . . . . . . . . . . . 13
                     |
| 7 | | neeq1 1637 |
. . . . . . . . . . . . 13
                     |
| 8 | | sseq1 2133 |
. . . . . . . . . . . . 13
                         |
| 9 | 6, 7, 8 | 3anbi123d 905 |
. . . . . . . . . . . 12
          
                            
     |
| 10 | 9 | rcla4ev 1924 |
. . . . . . . . . . 11
                                   
   

     |
| 11 | | spansna 10361 |
. . . . . . . . . . . . . 14
      
          |
| 12 | | hvaddcl 8965 |
. . . . . . . . . . . . . . 15
  
    |
| 13 | 12 | adantr 398 |
. . . . . . . . . . . . . 14
                     |
| 14 | | hvaddeq0 9019 |
. . . . . . . . . . . . . . . . 17
  
         |
| 15 | | sneq 2469 |
. . . . . . . . . . . . . . . . . . . . 21
             |
| 16 | 15 | fveq2d 3785 |
. . . . . . . . . . . . . . . . . . . 20
                     |
| 17 | | ax1cn 5334 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
| 18 | 17 | negcli 5434 |
. . . . . . . . . . . . . . . . . . . . 21
  |
| 19 | | ax1ne0 5345 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
| 20 | 17, 19 | negn0i 5866 |
. . . . . . . . . . . . . . . . . . . . 21
  |
| 21 | | spansncol 9574 |
. . . . . . . . . . . . . . . . . . . . 21
                      |
| 22 | 18, 20, 21 | mp3an23 920 |
. . . . . . . . . . . . . . . . . . . 20
                  |
| 23 | 16, 22 | sylan9eqr 1576 |
. . . . . . . . . . . . . . . . . . 19
                    |
| 24 | 23 | ex 380 |
. . . . . . . . . . . . . . . . . 18
                    |
| 25 | 24 | adantl 397 |
. . . . . . . . . . . . . . . . 17
  
                   |
| 26 | 14, 25 | sylbid 210 |
. . . . . . . . . . . . . . . 16
  
                  |
| 27 | 26 | necon3d 1651 |
. . . . . . . . . . . . . . 15
  
                  |
| 28 | 27 | imp 357 |
. . . . . . . . . . . . . 14
                     |
| 29 | 11, 13, 28 | sylanc 482 |
. . . . . . . . . . . . 13
                           |
| 30 | 29 | adantlr 402 |
. . . . . . . . . . . 12
     
                         |
| 31 | 30 | adantlr 402 |
. . . . . . . . . . 11
    
                                          |
| 32 | | eqeq2 1531 |
. . . . . . . . . . . . . . . . . 18
                                 |
| 33 | 32 | biimpd 160 |
. . . . . . . . . . . . . . . . 17
                                 |
| 34 | | spansneleqi 9575 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
| 35 | 12, 34 | syl 10 |
. . . . . . . . . . . . . . . . . . . . 21
  
                          |
| 36 | | elspansn 9572 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  |
| 37 | 36 | adantr 398 |
. . . . . . . . . . . . . . . . . . . . . 22
  
                 |
| 38 | | opreq1 4026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             |
| 39 | 38 | eqeq2d 1533 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
| 40 | 39 | rcla4ev 1924 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                |
| 41 | | addcl 5366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
| 42 | 18, 41 | mpan2 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      |
| 43 | 42 | ad2antlr 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                |
| 44 | | hvsubadd 9027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
            |
| 45 | | hvmulcl 8966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  
    |
| 46 | 45 | ancoms 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
| 47 | 46 | adantlr 402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
| 48 | | simpll 421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
| 49 | | simplr 422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
| 50 | 44, 47, 48, 49 | syl3anc 870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 |
| 51 | 50 | biimpar 426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
| 52 | | hvsubval 8969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
             |
| 53 | 45, 52 | sylancom 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |