Step | Hyp | Ref
| Expression |
1 | | prarloclemn 7498 |
. . . 4
   

   |
2 | 1 | 3adant2 1016 |
. . 3
 
      |
3 | 2 | 3ad2ant2 1019 |
. 2
       
                |
4 | | elprnql 7480 |
. . . . . . 7
    
   |
5 | 4 | 3ad2ant1 1018 |
. . . . . 6
       
             |
6 | | simp22 1031 |
. . . . . 6
       
             |
7 | | nqnq0 7440 |
. . . . . . . . 9
Q0 |
8 | 7 | sseli 3152 |
. . . . . . . 8
 Q0 |
9 | | nq0a0 7456 |
. . . . . . . 8
 Q0 
+Q0 0Q0   |
10 | 8, 9 | syl 14 |
. . . . . . 7
  +Q0
0Q0   |
11 | 7 | sseli 3152 |
. . . . . . . . . 10
 Q0 |
12 | | nq0m0r 7455 |
. . . . . . . . . 10
 Q0 0Q0 ·Q0  0Q0 |
13 | 11, 12 | syl 14 |
. . . . . . . . 9
 0Q0
·Q0 
0Q0 |
14 | | df-0nq0 7425 |
. . . . . . . . . 10
0Q0      ~Q0 |
15 | 14 | oveq1i 5885 |
. . . . . . . . 9
0Q0
·Q0        ~Q0
·Q0   |
16 | 13, 15 | eqtr3di 2225 |
. . . . . . . 8

0Q0      
~Q0 ·Q0    |
17 | 16 | oveq2d 5891 |
. . . . . . 7
  +Q0
0Q0  +Q0       ~Q0
·Q0     |
18 | 10, 17 | sylan9req 2231 |
. . . . . 6
 
  +Q0       ~Q0
·Q0     |
19 | 5, 6, 18 | syl2anc 411 |
. . . . 5
       
           
+Q0       ~Q0 ·Q0
    |
20 | | simp1r 1022 |
. . . . 5
       
             |
21 | 19, 20 | eqeltrrd 2255 |
. . . 4
       
            +Q0       ~Q0
·Q0     |
22 | | 2onn 6522 |
. . . . . . . . . . . . . . 15
 |
23 | | nna0r 6479 |
. . . . . . . . . . . . . . 15
     |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
   |
25 | 24 | oveq1i 5885 |
. . . . . . . . . . . . 13
 
     |
26 | 25 | eqeq1i 2185 |
. . . . . . . . . . . 12
  
      |
27 | 26 | biimpri 133 |
. . . . . . . . . . 11
         |
28 | 27 | opeq1d 3785 |
. . . . . . . . . 10
         
     |
29 | 28 | eceq1d 6571 |
. . . . . . . . 9
      
           |
30 | 29 | oveq1d 5890 |
. . . . . . . 8
                       |
31 | 30 | oveq2d 5891 |
. . . . . . 7
        
                  |
32 | 31 | eleq1d 2246 |
. . . . . 6
                
            |
33 | 32 | biimprcd 160 |
. . . . 5
                             |
34 | 33 | 3ad2ant3 1020 |
. . . 4
       
                              |
35 | | peano1 4594 |
. . . . 5
 |
36 | | opeq1 3779 |
. . . . . . . . . . 11

  
     |
37 | 36 | eceq1d 6571 |
. . . . . . . . . 10

    
~Q0      ~Q0  |
38 | 37 | oveq1d 5890 |
. . . . . . . . 9

      ~Q0
·Q0        ~Q0
·Q0    |
39 | 38 | oveq2d 5891 |
. . . . . . . 8

 +Q0       ~Q0 ·Q0
   +Q0       ~Q0
·Q0     |
40 | 39 | eleq1d 2246 |
. . . . . . 7

  +Q0       ~Q0 ·Q0
 
 +Q0       ~Q0
·Q0      |
41 | | oveq1 5882 |
. . . . . . . . . . . . 13

  
   |
42 | 41 | oveq1d 5890 |
. . . . . . . . . . . 12

          |
43 | 42 | opeq1d 3785 |
. . . . . . . . . . 11

      
  
      |
44 | 43 | eceq1d 6571 |
. . . . . . . . . 10

                   |
45 | 44 | oveq1d 5890 |
. . . . . . . . 9

               
        |
46 | 45 | oveq2d 5891 |
. . . . . . . 8

                            |
47 | 46 | eleq1d 2246 |
. . . . . . 7

             
                |
48 | 40, 47 | anbi12d 473 |
. . . . . 6

  
+Q0      
~Q0 ·Q0   
               +Q0       ~Q0
·Q0        
           |
49 | 48 | rspcev 2842 |
. . . . 5
 
 
+Q0       ~Q0 ·Q0
  
             
   +Q0       ~Q0 ·Q0
  
               |
50 | 35, 49 | mpan 424 |
. . . 4
  
+Q0       ~Q0 ·Q0
  
               
+Q0      
~Q0 ·Q0   
               |
51 | 21, 34, 50 | syl6an 1434 |
. . 3
       
              
 
+Q0      
~Q0 ·Q0   
                |
52 | 51 | reximdv 2578 |
. 2
       
            

 
  
+Q0      
~Q0 ·Q0   
                |
53 | 3, 52 | mpd 13 |
1
       
               +Q0       ~Q0 ·Q0
  
               |