Step | Hyp | Ref
| Expression |
1 | | nqpi 7379 |
. . . 4
               |
2 | | nq0nn 7443 |
. . . 4
 Q0      

     ~Q0   |
3 | 1, 2 | anim12i 338 |
. . 3
 
Q0
      

          

     ~Q0    |
4 | | ee4anv 1934 |
. . 3
           

      

     ~Q0 
      

          

     ~Q0    |
5 | 3, 4 | sylibr 134 |
. 2
 
Q0
          

       
     ~Q0    |
6 | | oveq12 5886 |
. . . . . . 7
           
~Q0
 +Q0        +Q0     
~Q0   |
7 | 6 | ad2ant2l 508 |
. . . . . 6
   

      

     ~Q0   +Q0        +Q0      ~Q0   |
8 | | nqnq0pi 7439 |
. . . . . . . . . 10
 
      ~Q0       |
9 | 8 | oveq1d 5892 |
. . . . . . . . 9
 
      
~Q0 +Q0      ~Q0       +Q0     
~Q0   |
10 | 9 | adantr 276 |
. . . . . . . 8
      
      ~Q0 +Q0
    
~Q0       +Q0      ~Q0   |
11 | | pinn 7310 |
. . . . . . . . 9
   |
12 | | addnnnq0 7450 |
. . . . . . . . 9
      
      ~Q0 +Q0
    
~Q0             
~Q0  |
13 | 11, 12 | sylanl1 402 |
. . . . . . . 8
      
      ~Q0 +Q0
    
~Q0             
~Q0  |
14 | 10, 13 | eqtr3d 2212 |
. . . . . . 7
      
      +Q0      ~Q0              ~Q0  |
15 | 14 | ad2ant2r 509 |
. . . . . 6
   

      

     ~Q0       
+Q0      ~Q0
            
~Q0  |
16 | 7, 15 | eqtrd 2210 |
. . . . 5
   

      

     ~Q0   +Q0              
~Q0  |
17 | | pinn 7310 |
. . . . . . . . . . . . . 14
   |
18 | | nnmcl 6484 |
. . . . . . . . . . . . . 14
 
     |
19 | 17, 18 | sylan 283 |
. . . . . . . . . . . . 13
 
     |
20 | 19 | ad2ant2lr 510 |
. . . . . . . . . . . 12
      
    |
21 | | mulpiord 7318 |
. . . . . . . . . . . . . 14
 
       |
22 | | mulclpi 7329 |
. . . . . . . . . . . . . 14
 
     |
23 | 21, 22 | eqeltrrd 2255 |
. . . . . . . . . . . . 13
 
     |
24 | 23 | ad2ant2rl 511 |
. . . . . . . . . . . 12
      
    |
25 | | pinn 7310 |
. . . . . . . . . . . . 13
       |
26 | | nnacom 6487 |
. . . . . . . . . . . . 13
    
                |
27 | 25, 26 | sylan2 286 |
. . . . . . . . . . . 12
    
                |
28 | 20, 24, 27 | syl2anc 411 |
. . . . . . . . . . 11
      
              |
29 | | nnppipi 7344 |
. . . . . . . . . . . 12
    
          |
30 | 20, 24, 29 | syl2anc 411 |
. . . . . . . . . . 11
      
        |
31 | 28, 30 | eqeltrrd 2255 |
. . . . . . . . . 10
      
        |
32 | | mulpiord 7318 |
. . . . . . . . . . . 12
 
       |
33 | | mulclpi 7329 |
. . . . . . . . . . . 12
 
     |
34 | 32, 33 | eqeltrrd 2255 |
. . . . . . . . . . 11
 
     |
35 | 34 | ad2ant2l 508 |
. . . . . . . . . 10
      
    |
36 | | opelxpi 4660 |
. . . . . . . . . 10
                          |
37 | 31, 35, 36 | syl2anc 411 |
. . . . . . . . 9
      
               |
38 | | enqex 7361 |
. . . . . . . . . 10
 |
39 | 38 | ecelqsi 6591 |
. . . . . . . . 9
                                 |
40 | 37, 39 | syl 14 |
. . . . . . . 8
      
                   |
41 | | df-nqqs 7349 |
. . . . . . . 8
     |
42 | 40, 41 | eleqtrrdi 2271 |
. . . . . . 7
      
               |
43 | | nqnq0pi 7439 |
. . . . . . . . 9
                        ~Q0               |
44 | 43 | eleq1d 2246 |
. . . . . . . 8
                        
~Q0
                |
45 | 31, 35, 44 | syl2anc 411 |
. . . . . . 7
      
              ~Q0                 |
46 | 42, 45 | mpbird 167 |
. . . . . 6
      
            
~Q0   |
47 | 46 | ad2ant2r 509 |
. . . . 5
   

      

     ~Q0              
~Q0   |
48 | 16, 47 | eqeltrd 2254 |
. . . 4
   

      

     ~Q0   +Q0    |
49 | 48 | exlimivv 1896 |
. . 3
       

      

     ~Q0   +Q0    |
50 | 49 | exlimivv 1896 |
. 2
           

      

     ~Q0   +Q0    |
51 | 5, 50 | syl 14 |
1
 
Q0
 +Q0    |