Proof of Theorem prarloclem5
Step | Hyp | Ref
| Expression |
1 | | prarloclemn 6482 |
. . . 4
   


  |
2 | 1 | 3adant2 922 |
. . 3
 
 
    |
3 | 2 | 3ad2ant2 925 |
. 2
       
           
    |
4 | | elprnql 6464 |
. . . . . . 7
    

  |
5 | 4 | 3ad2ant1 924 |
. . . . . 6
       
             |
6 | | simp22 937 |
. . . . . 6
       
             |
7 | | nqnq0 6424 |
. . . . . . . . 9
Q0 |
8 | 7 | sseli 2935 |
. . . . . . . 8
 Q0 |
9 | | nq0a0 6440 |
. . . . . . . 8
 Q0 
+Q0 0Q0   |
10 | 8, 9 | syl 14 |
. . . . . . 7
  +Q0
0Q0   |
11 | | df-0nq0 6409 |
. . . . . . . . . 10
0Q0      ~Q0 |
12 | 11 | oveq1i 5465 |
. . . . . . . . 9
0Q0
·Q0        ~Q0
·Q0   |
13 | 7 | sseli 2935 |
. . . . . . . . . 10
 Q0 |
14 | | nq0m0r 6439 |
. . . . . . . . . 10
 Q0 0Q0 ·Q0  0Q0 |
15 | 13, 14 | syl 14 |
. . . . . . . . 9
 0Q0
·Q0 
0Q0 |
16 | 12, 15 | syl5reqr 2084 |
. . . . . . . 8

0Q0      
~Q0 ·Q0    |
17 | 16 | oveq2d 5471 |
. . . . . . 7
  +Q0
0Q0  +Q0       ~Q0
·Q0     |
18 | 10, 17 | sylan9req 2090 |
. . . . . 6
 
  +Q0       ~Q0
·Q0     |
19 | 5, 6, 18 | syl2anc 391 |
. . . . 5
       
           
+Q0       ~Q0 ·Q0
    |
20 | | simp1r 928 |
. . . . 5
       
             |
21 | 19, 20 | eqeltrrd 2112 |
. . . 4
       
            +Q0       ~Q0
·Q0     |
22 | | 2onn 6030 |
. . . . . . . . . . . . . . 15
 |
23 | | nna0r 5996 |
. . . . . . . . . . . . . . 15
     |
24 | 22, 23 | ax-mp 7 |
. . . . . . . . . . . . . 14
   |
25 | 24 | oveq1i 5465 |
. . . . . . . . . . . . 13
   
   |
26 | 25 | eqeq1i 2044 |
. . . . . . . . . . . 12
  
   
  |
27 | 26 | biimpri 124 |
. . . . . . . . . . 11
         |
28 | 27 | opeq1d 3546 |
. . . . . . . . . 10
     
   
     |
29 | 28 | eceq1d 6078 |
. . . . . . . . 9
                  |
30 | 29 | oveq1d 5470 |
. . . . . . . 8
          
            |
31 | 30 | oveq2d 5471 |
. . . . . . 7
        
                  |
32 | 31 | eleq1d 2103 |
. . . . . 6
    
       
            
   |
33 | 32 | biimprcd 149 |
. . . . 5
       
 
  

       
       |
34 | 33 | 3ad2ant3 926 |
. . . 4
       
            


       
       |
35 | | peano1 4260 |
. . . . 5
 |
36 | | opeq1 3540 |
. . . . . . . . . . 11

  
     |
37 | 36 | eceq1d 6078 |
. . . . . . . . . 10

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

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

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

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

  
   |
42 | 41 | oveq1d 5470 |
. . . . . . . . . . . 12

 
        |
43 | 42 | opeq1d 3546 |
. . . . . . . . . . 11

  
   
  
      |
44 | 43 | eceq1d 6078 |
. . . . . . . . . 10

               
   |
45 | 44 | oveq1d 5470 |
. . . . . . . . 9

         
              |
46 | 45 | oveq2d 5471 |
. . . . . . . 8

                     
      |
47 | 46 | eleq1d 2103 |
. . . . . . 7

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

  
+Q0      
~Q0 ·Q0   
         
 
  
+Q0       ~Q0 ·Q0
 

       
        |
49 | 48 | rspcev 2650 |
. . . . 5
   
+Q0       ~Q0 ·Q0
 

       
      
 
+Q0      
~Q0 ·Q0   
         
 
   |
50 | 35, 49 | mpan 400 |
. . . 4
  
+Q0       ~Q0 ·Q0
 

       
     
 
+Q0      
~Q0 ·Q0   
         
 
   |
51 | 21, 34, 50 | syl6an 1320 |
. . 3
       
            

  
+Q0      
~Q0 ·Q0   
         
 
    |
52 | 51 | reximdv 2414 |
. 2
       
            


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

         
 
   |