Step | Hyp | Ref
| Expression |
1 | | df-nq0 7424 |
. . . 4
Q0    
~Q0  |
2 | | oveq2 5883 |
. . . . . . 7
      ~Q0 
+Q0      ~Q0
 +Q0    |
3 | 2 | oveq1d 5890 |
. . . . . 6
      ~Q0   +Q0     
~Q0 +Q0      ~Q0
  +Q0  +Q0      ~Q0   |
4 | | oveq1 5882 |
. . . . . . 7
      ~Q0      
~Q0 +Q0      ~Q0 
+Q0      ~Q0   |
5 | 4 | oveq2d 5891 |
. . . . . 6
      ~Q0 
+Q0      
~Q0 +Q0      ~Q0   +Q0  +Q0      ~Q0    |
6 | 3, 5 | eqeq12d 2192 |
. . . . 5
      ~Q0    +Q0      ~Q0 +Q0      ~Q0 
+Q0      
~Q0 +Q0      ~Q0    +Q0  +Q0      ~Q0 
+Q0 
+Q0      ~Q0     |
7 | 6 | imbi2d 230 |
. . . 4
      ~Q0   Q0  
+Q0      ~Q0 +Q0      ~Q0 
+Q0      
~Q0 +Q0      ~Q0  
 Q0  
+Q0 
+Q0      ~Q0
 +Q0  +Q0     
~Q0      |
8 | | oveq2 5883 |
. . . . . 6
      ~Q0   +Q0  +Q0      ~Q0   +Q0  +Q0    |
9 | | oveq2 5883 |
. . . . . . 7
      ~Q0 
+Q0      ~Q0
 +Q0    |
10 | 9 | oveq2d 5891 |
. . . . . 6
      ~Q0 
+Q0 
+Q0      ~Q0   +Q0 
+Q0     |
11 | 8, 10 | eqeq12d 2192 |
. . . . 5
      ~Q0    +Q0 
+Q0      ~Q0
 +Q0  +Q0     
~Q0 
  +Q0  +Q0   +Q0 
+Q0      |
12 | 11 | imbi2d 230 |
. . . 4
      ~Q0   Q0  
+Q0 
+Q0      ~Q0
 +Q0  +Q0     
~Q0  
 Q0  
+Q0 
+Q0   +Q0 
+Q0       |
13 | | oveq1 5882 |
. . . . . . . . 9
      ~Q0
      ~Q0 +Q0
    
~Q0  +Q0     
~Q0   |
14 | 13 | oveq1d 5890 |
. . . . . . . 8
      ~Q0
       ~Q0 +Q0     
~Q0 +Q0      ~Q0
  +Q0      ~Q0 +Q0     
~Q0   |
15 | | oveq1 5882 |
. . . . . . . 8
      ~Q0
      ~Q0 +Q0
      ~Q0
+Q0      ~Q0   +Q0       ~Q0 +Q0     
~Q0    |
16 | 14, 15 | eqeq12d 2192 |
. . . . . . 7
      ~Q0
       
~Q0 +Q0      ~Q0 +Q0     
~Q0       ~Q0 +Q0
      ~Q0
+Q0      ~Q0 
  +Q0      ~Q0 +Q0     
~Q0  +Q0       ~Q0 +Q0     
~Q0     |
17 | 16 | imbi2d 230 |
. . . . . 6
      ~Q0
   


 
       ~Q0 +Q0     
~Q0 +Q0      ~Q0
      ~Q0 +Q0
      ~Q0
+Q0      ~Q0  
      
  +Q0      ~Q0 +Q0     
~Q0  +Q0       ~Q0 +Q0     
~Q0      |
18 | | simp1l 1021 |
. . . . . . . . . . . 12
        
  |
19 | | simp2r 1024 |
. . . . . . . . . . . . . 14
        
  |
20 | | pinn 7308 |
. . . . . . . . . . . . . 14
   |
21 | 19, 20 | syl 14 |
. . . . . . . . . . . . 13
        
  |
22 | | simp3r 1026 |
. . . . . . . . . . . . . 14
        
  |
23 | | pinn 7308 |
. . . . . . . . . . . . . 14
   |
24 | 22, 23 | syl 14 |
. . . . . . . . . . . . 13
        
  |
25 | | nnmcl 6482 |
. . . . . . . . . . . . 13
 
     |
26 | 21, 24, 25 | syl2anc 411 |
. . . . . . . . . . . 12
        
    |
27 | | nnmcl 6482 |
. . . . . . . . . . . 12
  
        |
28 | 18, 26, 27 | syl2anc 411 |
. . . . . . . . . . 11
        
      |
29 | | simp1r 1022 |
. . . . . . . . . . . . 13
        
  |
30 | | pinn 7308 |
. . . . . . . . . . . . 13
   |
31 | 29, 30 | syl 14 |
. . . . . . . . . . . 12
        
  |
32 | | simp2l 1023 |
. . . . . . . . . . . . 13
        
  |
33 | | nnmcl 6482 |
. . . . . . . . . . . . 13
 
     |
34 | 32, 24, 33 | syl2anc 411 |
. . . . . . . . . . . 12
        
    |
35 | | nnmcl 6482 |
. . . . . . . . . . . 12
           |
36 | 31, 34, 35 | syl2anc 411 |
. . . . . . . . . . 11
        
      |
37 | | simp3l 1025 |
. . . . . . . . . . . . 13
        
  |
38 | | nnmcl 6482 |
. . . . . . . . . . . . 13
 
     |
39 | 21, 37, 38 | syl2anc 411 |
. . . . . . . . . . . 12
        
    |
40 | | nnmcl 6482 |
. . . . . . . . . . . 12
  
        |
41 | 31, 39, 40 | syl2anc 411 |
. . . . . . . . . . 11
        
      |
42 | | nnaass 6486 |
. . . . . . . . . . 11
                                                 |
43 | 28, 36, 41, 42 | syl3anc 1238 |
. . . . . . . . . 10
        
                  
               |
44 | | nnmcom 6490 |
. . . . . . . . . . . . 13
 
       |
45 | 44 | adantl 277 |
. . . . . . . . . . . 12
   


   
         |
46 | | nndir 6491 |
. . . . . . . . . . . . 13
 
             |
47 | 46 | adantl 277 |
. . . . . . . . . . . 12
   


   

              |
48 | | nnmass 6488 |
. . . . . . . . . . . . 13
 
           |
49 | 48 | adantl 277 |
. . . . . . . . . . . 12
   


   

            |
50 | | nnmcl 6482 |
. . . . . . . . . . . . 13
 
     |
51 | 50 | adantl 277 |
. . . . . . . . . . . 12
   


   
       |
52 | 45, 47, 49, 51, 18, 31, 21, 32, 24 | caovdilemd 6066 |
. . . . . . . . . . 11
        
          
         |
53 | | nnmass 6488 |
. . . . . . . . . . . 12
 
           |
54 | 31, 21, 37, 53 | syl3anc 1238 |
. . . . . . . . . . 11
        
          |
55 | 52, 54 | oveq12d 5893 |
. . . . . . . . . 10
        
                                |
56 | | nndi 6487 |
. . . . . . . . . . . 12
    
                      |
57 | 31, 34, 39, 56 | syl3anc 1238 |
. . . . . . . . . . 11
        
                    |
58 | 57 | oveq2d 5891 |
. . . . . . . . . 10
        
                
               |
59 | 43, 55, 58 | 3eqtr4d 2220 |
. . . . . . . . 9
        
                
             |
60 | | nnmass 6488 |
. . . . . . . . . 10
 
           |
61 | 31, 21, 24, 60 | syl3anc 1238 |
. . . . . . . . 9
        
          |
62 | | opeq12 3781 |
. . . . . . . . . 10
                                                           
                       |
63 | 62 | eceq1d 6571 |
. . . . . . . . 9
                                                             
~Q0                       
~Q0  |
64 | 59, 61, 63 | syl2anc 411 |
. . . . . . . 8
        
                      
~Q0                       
~Q0  |
65 | | addnnnq0 7448 |
. . . . . . . . . . . 12
      
      ~Q0 +Q0
    
~Q0             
~Q0  |
66 | 65 | oveq1d 5890 |
. . . . . . . . . . 11
      
       ~Q0 +Q0     
~Q0 +Q0      ~Q0
              ~Q0 +Q0
    
~Q0   |
67 | 66 | adantr 276 |
. . . . . . . . . 10
   


 
         
~Q0 +Q0      ~Q0 +Q0     
~Q0               ~Q0 +Q0
    
~Q0   |
68 | | addassnq0lemcl 7460 |
. . . . . . . . . . 11
      
            |
69 | | addnnnq0 7448 |
. . . . . . . . . . 11
              
              ~Q0 +Q0
    
~Q0                       
~Q0  |
70 | 68, 69 | sylan 283 |
. . . . . . . . . 10
   


 
                
~Q0 +Q0      ~Q0                        ~Q0  |
71 | 67, 70 | eqtrd 2210 |
. . . . . . . . 9
   


 
         
~Q0 +Q0      ~Q0 +Q0     
~Q0                       
~Q0  |
72 | 71 | 3impa 1194 |
. . . . . . . 8
        
       ~Q0 +Q0     
~Q0 +Q0      ~Q0
                      
~Q0  |
73 | | addnnnq0 7448 |
. . . . . . . . . . . 12
      
      ~Q0
+Q0      ~Q0
            
~Q0  |
74 | 73 | oveq2d 5891 |
. . . . . . . . . . 11
      
      ~Q0 +Q0
      ~Q0
+Q0      ~Q0        ~Q0 +Q0             
~Q0   |
75 | 74 | adantl 277 |
. . . . . . . . . 10
     


         ~Q0 +Q0       ~Q0
+Q0      ~Q0        ~Q0 +Q0             
~Q0   |
76 | | addassnq0lemcl 7460 |
. . . . . . . . . . 11
      
            |
77 | | addnnnq0 7448 |
. . . . . . . . . . 11
              
      ~Q0 +Q0
            
~Q0                       
~Q0  |
78 | 76, 77 | sylan2 286 |
. . . . . . . . . 10
     


         ~Q0 +Q0             
~Q0                       
~Q0  |
79 | 75, 78 | eqtrd 2210 |
. . . . . . . . 9
     


         ~Q0 +Q0       ~Q0
+Q0      ~Q0      
                  ~Q0  |
80 | 79 | 3impb 1199 |
. . . . . . . 8
        
      ~Q0 +Q0
      ~Q0
+Q0      ~Q0      
                  ~Q0  |
81 | 64, 72, 80 | 3eqtr4d 2220 |
. . . . . . 7
        
       ~Q0 +Q0     
~Q0 +Q0      ~Q0
      ~Q0 +Q0
      ~Q0
+Q0      ~Q0    |
82 | 81 | 3expib 1206 |
. . . . . 6
 
     
 
       ~Q0 +Q0     
~Q0 +Q0      ~Q0
      ~Q0 +Q0
      ~Q0
+Q0      ~Q0     |
83 | 1, 17, 82 | ecoptocl 6622 |
. . . . 5
 Q0     
 
  +Q0      ~Q0 +Q0     
~Q0  +Q0       ~Q0 +Q0     
~Q0     |
84 | 83 | com12 30 |
. . . 4
      
 Q0  
+Q0      ~Q0 +Q0      ~Q0 
+Q0      
~Q0 +Q0      ~Q0     |
85 | 1, 7, 12, 84 | 2ecoptocl 6623 |
. . 3
 
Q0
Q0
 Q0  
+Q0 
+Q0   +Q0 
+Q0      |
86 | 85 | com12 30 |
. 2
 Q0   Q0 Q0   +Q0  +Q0   +Q0  +Q0      |
87 | 86 | 3impib 1201 |
1
 
Q0
Q0
Q0
  +Q0  +Q0   +Q0 
+Q0     |