Proof of Theorem prarloclemcalc
Step | Hyp | Ref
| Expression |
1 | | simprll 537 |
. . . . 5
    +Q0       ~Q0 ·Q0
 

                
     |
2 | | nqnq0a 7431 |
. . . . 5
 
    +Q0    |
3 | 1, 1, 2 | syl2anc 411 |
. . . 4
    +Q0       ~Q0 ·Q0
 

                
     
+Q0    |
4 | 3 | oveq2d 5884 |
. . 3
    +Q0       ~Q0 ·Q0
 

                
    +Q0     +Q0  +Q0     |
5 | | simpll 527 |
. . . . 5
    +Q0       ~Q0 ·Q0
 

                
   
+Q0      
~Q0 ·Q0     |
6 | | simprrl 539 |
. . . . . 6
    +Q0       ~Q0 ·Q0
 

                
     |
7 | | simprrr 540 |
. . . . . . . 8
    +Q0       ~Q0 ·Q0
 

                
     |
8 | | 1pi 7292 |
. . . . . . . . . . 11
 |
9 | | opelxpi 4654 |
. . . . . . . . . . 11
          |
10 | 8, 9 | mpan2 425 |
. . . . . . . . . 10
        |
11 | | enq0ex 7416 |
. . . . . . . . . . 11
~Q0  |
12 | 11 | ecelqsi 6582 |
. . . . . . . . . 10
  
        ~Q0    
~Q0   |
13 | 10, 12 | syl 14 |
. . . . . . . . 9
     
~Q0    
~Q0   |
14 | | df-nq0 7402 |
. . . . . . . . 9
Q0    
~Q0  |
15 | 13, 14 | eleqtrrdi 2271 |
. . . . . . . 8
     
~Q0 Q0 |
16 | 7, 15 | syl 14 |
. . . . . . 7
    +Q0       ~Q0 ·Q0
 

                
       
~Q0 Q0 |
17 | | nqnq0 7418 |
. . . . . . . 8
Q0 |
18 | 17, 1 | sselid 3153 |
. . . . . . 7
    +Q0       ~Q0 ·Q0
 

                
   Q0 |
19 | | mulclnq0 7429 |
. . . . . . 7
       ~Q0 Q0
Q0
      ~Q0
·Q0 
Q0 |
20 | 16, 18, 19 | syl2anc 411 |
. . . . . 6
    +Q0       ~Q0 ·Q0
 

                
         ~Q0 ·Q0
 Q0 |
21 | | nqpnq0nq 7430 |
. . . . . 6
        ~Q0 ·Q0
 Q0 
+Q0      
~Q0 ·Q0     |
22 | 6, 20, 21 | syl2anc 411 |
. . . . 5
    +Q0       ~Q0 ·Q0
 

                
    +Q0       ~Q0 ·Q0
    |
23 | 5, 22 | eqeltrd 2254 |
. . . 4
    +Q0       ~Q0 ·Q0
 

                
     |
24 | | addclnq 7352 |
. . . . 5
 
     |
25 | 1, 1, 24 | syl2anc 411 |
. . . 4
    +Q0       ~Q0 ·Q0
 

                
       |
26 | | nqnq0a 7431 |
. . . 4
  
      
+Q0      |
27 | 23, 25, 26 | syl2anc 411 |
. . 3
    +Q0       ~Q0 ·Q0
 

                
       
+Q0      |
28 | | simplr 528 |
. . . . . 6
    +Q0       ~Q0 ·Q0
 

                
                |
29 | | 2onn 6515 |
. . . . . . . . . . . . . 14
 |
30 | | 2on0 6420 |
. . . . . . . . . . . . . 14
 |
31 | | elni 7285 |
. . . . . . . . . . . . . 14

    |
32 | 29, 30, 31 | mpbir2an 942 |
. . . . . . . . . . . . 13
 |
33 | | nnppipi 7320 |
. . . . . . . . . . . . 13
    
  |
34 | 32, 33 | mpan2 425 |
. . . . . . . . . . . 12
     |
35 | | opelxpi 4654 |
. . . . . . . . . . . 12
   
     
    |
36 | 34, 8, 35 | sylancl 413 |
. . . . . . . . . . 11
     
    |
37 | | enqex 7337 |
. . . . . . . . . . . 12
 |
38 | 37 | ecelqsi 6582 |
. . . . . . . . . . 11
    
                |
39 | 36, 38 | syl 14 |
. . . . . . . . . 10
              |
40 | | df-nqqs 7325 |
. . . . . . . . . 10
     |
41 | 39, 40 | eleqtrrdi 2271 |
. . . . . . . . 9
          |
42 | 7, 41 | syl 14 |
. . . . . . . 8
    +Q0       ~Q0 ·Q0
 

                
            |
43 | | mulclnq 7353 |
. . . . . . . 8
        
            |
44 | 42, 1, 43 | syl2anc 411 |
. . . . . . 7
    +Q0       ~Q0 ·Q0
 

                
              |
45 | | nqnq0a 7431 |
. . . . . . 7
                        +Q0             |
46 | 6, 44, 45 | syl2anc 411 |
. . . . . 6
    +Q0       ~Q0 ·Q0
 

                
              
+Q0             |
47 | | nqnq0m 7432 |
. . . . . . . . 9
        
                  ·Q0    |
48 | 42, 1, 47 | syl2anc 411 |
. . . . . . . 8
    +Q0       ~Q0 ·Q0
 

                
                    ·Q0
   |
49 | | nqnq0pi 7415 |
. . . . . . . . . . 11
   
       
~Q0         |
50 | 34, 8, 49 | sylancl 413 |
. . . . . . . . . 10
       
~Q0         |
51 | 7, 50 | syl 14 |
. . . . . . . . 9
    +Q0       ~Q0 ·Q0
 

                
         
~Q0         |
52 | 51 | oveq1d 5883 |
. . . . . . . 8
    +Q0       ~Q0 ·Q0
 

                
           ~Q0
·Q0          ·Q0    |
53 | 48, 52 | eqtr4d 2213 |
. . . . . . 7
    +Q0       ~Q0 ·Q0
 

                
                   
~Q0 ·Q0    |
54 | 53 | oveq2d 5884 |
. . . . . 6
    +Q0       ~Q0 ·Q0
 

                
    +Q0            +Q0         ~Q0
·Q0     |
55 | 28, 46, 54 | 3eqtrd 2214 |
. . . . 5
    +Q0       ~Q0 ·Q0
 

                
   
+Q0        
~Q0 ·Q0     |
56 | | nnanq0 7435 |
. . . . . . . . . 10
         
~Q0      
~Q0 +Q0      ~Q0   |
57 | 8, 56 | mp3an3 1326 |
. . . . . . . . 9
          ~Q0       ~Q0 +Q0     
~Q0   |
58 | 7, 29, 57 | sylancl 413 |
. . . . . . . 8
    +Q0       ~Q0 ·Q0
 

                
         
~Q0      
~Q0 +Q0      ~Q0   |
59 | 58 | oveq1d 5883 |
. . . . . . 7
    +Q0       ~Q0 ·Q0
 

                
           ~Q0
·Q0        
~Q0 +Q0      ~Q0 ·Q0    |
60 | | opelxpi 4654 |
. . . . . . . . . . . 12
          |
61 | 29, 8, 60 | mp2an 426 |
. . . . . . . . . . 11
      |
62 | 11 | ecelqsi 6582 |
. . . . . . . . . . 11
  
        ~Q0    
~Q0   |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . 10
    
~Q0    
~Q0  |
64 | 63, 14 | eleqtrri 2253 |
. . . . . . . . 9
    
~Q0 Q0 |
65 | | distnq0r 7440 |
. . . . . . . . 9
 
Q0     
~Q0 Q0      ~Q0 Q0        ~Q0
+Q0      ~Q0 ·Q0         ~Q0 ·Q0
 +Q0       ~Q0
·Q0     |
66 | 64, 65 | mp3an3 1326 |
. . . . . . . 8
 
Q0     
~Q0 Q0        ~Q0
+Q0      ~Q0 ·Q0         ~Q0 ·Q0
 +Q0       ~Q0
·Q0     |
67 | 18, 16, 66 | syl2anc 411 |
. . . . . . 7
    +Q0       ~Q0 ·Q0
 

                
         
~Q0 +Q0      ~Q0 ·Q0         ~Q0
·Q0 
+Q0      
~Q0 ·Q0     |
68 | 59, 67 | eqtrd 2210 |
. . . . . 6
    +Q0       ~Q0 ·Q0
 

                
           ~Q0
·Q0        
~Q0 ·Q0  +Q0       ~Q0 ·Q0
    |
69 | 68 | oveq2d 5884 |
. . . . 5
    +Q0       ~Q0 ·Q0
 

                
    +Q0         ~Q0
·Q0   
+Q0       
~Q0 ·Q0  +Q0       ~Q0 ·Q0
     |
70 | | nq02m 7442 |
. . . . . . . . 9
 Q0      
~Q0 ·Q0  
+Q0    |
71 | 70 | oveq2d 5884 |
. . . . . . . 8
 Q0       
~Q0 ·Q0  +Q0       ~Q0 ·Q0
         ~Q0 ·Q0
 +Q0  +Q0     |
72 | 71 | oveq2d 5884 |
. . . . . . 7
 Q0 
+Q0       
~Q0 ·Q0  +Q0       ~Q0 ·Q0
    +Q0       
~Q0 ·Q0  +Q0  +Q0      |
73 | 18, 72 | syl 14 |
. . . . . 6
    +Q0       ~Q0 ·Q0
 

                
    +Q0       
~Q0 ·Q0  +Q0       ~Q0 ·Q0
    +Q0       
~Q0 ·Q0  +Q0  +Q0      |
74 | 17, 6 | sselid 3153 |
. . . . . . 7
    +Q0       ~Q0 ·Q0
 

                
   Q0 |
75 | | addclnq0 7428 |
. . . . . . . 8
 
Q0
Q0
 +Q0  Q0 |
76 | 18, 18, 75 | syl2anc 411 |
. . . . . . 7
    +Q0       ~Q0 ·Q0
 

                
    +Q0 
Q0 |
77 | | addassnq0 7439 |
. . . . . . 7
 
Q0      
~Q0 ·Q0  Q0 
+Q0 
Q0
  +Q0       ~Q0 ·Q0
  +Q0 
+Q0   
+Q0       
~Q0 ·Q0  +Q0  +Q0      |
78 | 74, 20, 76, 77 | syl3anc 1238 |
. . . . . 6
    +Q0       ~Q0 ·Q0
 

                
    
+Q0      
~Q0 ·Q0   +Q0 
+Q0   
+Q0       
~Q0 ·Q0  +Q0  +Q0      |
79 | 73, 78 | eqtr4d 2213 |
. . . . 5
    +Q0       ~Q0 ·Q0
 

                
    +Q0       
~Q0 ·Q0  +Q0       ~Q0 ·Q0
    
+Q0      
~Q0 ·Q0   +Q0 
+Q0     |
80 | 55, 69, 79 | 3eqtrd 2214 |
. . . 4
    +Q0       ~Q0 ·Q0
 

                
     +Q0       ~Q0 ·Q0
  +Q0 
+Q0     |
81 | | oveq1 5875 |
. . . . . 6
 
+Q0      
~Q0 ·Q0  
 +Q0  +Q0    
+Q0      
~Q0 ·Q0   +Q0 
+Q0     |
82 | 81 | eqeq2d 2189 |
. . . . 5
 
+Q0      
~Q0 ·Q0  
 
+Q0 
+Q0  
 
+Q0      
~Q0 ·Q0   +Q0 
+Q0      |
83 | 5, 82 | syl 14 |
. . . 4
    +Q0       ~Q0 ·Q0
 

                
   
 +Q0  +Q0  
 
+Q0      
~Q0 ·Q0   +Q0 
+Q0      |
84 | 80, 83 | mpbird 167 |
. . 3
    +Q0       ~Q0 ·Q0
 

                
   
+Q0 
+Q0     |
85 | 4, 27, 84 | 3eqtr4rd 2221 |
. 2
    +Q0       ~Q0 ·Q0
 

                
    
    |
86 | | simprlr 538 |
. . 3
    +Q0       ~Q0 ·Q0
 

                
       |
87 | | ltrelnq 7342 |
. . . . . 6
   |
88 | 87 | brel 4674 |
. . . . 5
  
      |
89 | 86, 88 | syl 14 |
. . . 4
    +Q0       ~Q0 ·Q0
 

                
     
   |
90 | | ltanqg 7377 |
. . . . 5
   
   
         |
91 | 90 | 3expa 1203 |
. . . 4
     
             |
92 | 89, 23, 91 | syl2anc 411 |
. . 3
    +Q0       ~Q0 ·Q0
 

                
     
         |
93 | 86, 92 | mpbid 147 |
. 2
    +Q0       ~Q0 ·Q0
 

                
           |
94 | 85, 93 | eqbrtrd 4022 |
1
    +Q0       ~Q0 ·Q0
 

                
       |