Step | Hyp | Ref
| Expression |
1 | | df-nq0 7174 |
. . . 4
Q0    
~Q0  |
2 | | oveq1 5733 |
. . . . . . 7
      ~Q0      
~Q0 +Q0      ~Q0 
+Q0      ~Q0   |
3 | 2 | oveq2d 5742 |
. . . . . 6
      ~Q0 
·Q0      
~Q0 +Q0      ~Q0   ·Q0  +Q0     
~Q0    |
4 | | oveq2 5734 |
. . . . . . 7
      ~Q0 
·Q0      ~Q0
 ·Q0    |
5 | 4 | oveq1d 5741 |
. . . . . 6
      ~Q0   ·Q0     
~Q0 +Q0 
·Q0      ~Q0   
·Q0 
+Q0 
·Q0      ~Q0    |
6 | 3, 5 | eqeq12d 2127 |
. . . . 5
      ~Q0   ·Q0       ~Q0
+Q0      ~Q0   
·Q0      ~Q0 +Q0  ·Q0      ~Q0  
·Q0 
+Q0      ~Q0   
·Q0 
+Q0 
·Q0      ~Q0     |
7 | 6 | imbi2d 229 |
. . . 4
      ~Q0   Q0 
·Q0      
~Q0 +Q0      ~Q0    ·Q0      ~Q0 +Q0  ·Q0     
~Q0  
 Q0 
·Q0 
+Q0      ~Q0   
·Q0 
+Q0 
·Q0      ~Q0      |
8 | | oveq2 5734 |
. . . . . . 7
      ~Q0 
+Q0      ~Q0
 +Q0    |
9 | 8 | oveq2d 5742 |
. . . . . 6
      ~Q0 
·Q0 
+Q0      ~Q0   ·Q0  +Q0     |
10 | | oveq2 5734 |
. . . . . . 7
      ~Q0 
·Q0      ~Q0
 ·Q0    |
11 | 10 | oveq2d 5742 |
. . . . . 6
      ~Q0   ·Q0  +Q0  ·Q0      ~Q0    ·Q0  +Q0 
·Q0     |
12 | 9, 11 | eqeq12d 2127 |
. . . . 5
      ~Q0   ·Q0  +Q0     
~Q0   
·Q0 
+Q0 
·Q0      ~Q0 
 ·Q0  +Q0    
·Q0 
+Q0 
·Q0      |
13 | 12 | imbi2d 229 |
. . . 4
      ~Q0   Q0 
·Q0 
+Q0      ~Q0   
·Q0 
+Q0 
·Q0      ~Q0  
 Q0 
·Q0 
+Q0    
·Q0 
+Q0 
·Q0       |
14 | | oveq1 5733 |
. . . . . . . 8
      ~Q0
      ~Q0
·Q0      
~Q0 +Q0      ~Q0   ·Q0       ~Q0
+Q0      ~Q0    |
15 | | oveq1 5733 |
. . . . . . . . 9
      ~Q0
      ~Q0
·Q0      ~Q0
 ·Q0     
~Q0   |
16 | | oveq1 5733 |
. . . . . . . . 9
      ~Q0
      ~Q0
·Q0      ~Q0
 ·Q0     
~Q0   |
17 | 15, 16 | oveq12d 5744 |
. . . . . . . 8
      ~Q0
       ~Q0 ·Q0
    
~Q0 +Q0       ~Q0 ·Q0
    
~Q0   
·Q0      ~Q0 +Q0  ·Q0      ~Q0    |
18 | 14, 17 | eqeq12d 2127 |
. . . . . . 7
      ~Q0
       ~Q0 ·Q0
      ~Q0
+Q0      ~Q0        
~Q0 ·Q0     
~Q0 +Q0       ~Q0 ·Q0
    
~Q0 
 ·Q0       ~Q0
+Q0      ~Q0   
·Q0      ~Q0 +Q0  ·Q0      ~Q0     |
19 | 18 | imbi2d 229 |
. . . . . 6
      ~Q0
   


 
      ~Q0
·Q0      
~Q0 +Q0      ~Q0         ~Q0 ·Q0
    
~Q0 +Q0       ~Q0 ·Q0
    
~Q0  
      
 ·Q0       ~Q0
+Q0      ~Q0   
·Q0      ~Q0 +Q0  ·Q0      ~Q0      |
20 | | an42 559 |
. . . . . . . . . . . 12
          
    |
21 | 20 | anbi2i 450 |
. . . . . . . . . . 11
     


  
 
  


     |
22 | | 3anass 947 |
. . . . . . . . . . 11
                     |
23 | | 3anass 947 |
. . . . . . . . . . 11
                     |
24 | 21, 22, 23 | 3bitr4i 211 |
. . . . . . . . . 10
            
      |
25 | | pinn 7058 |
. . . . . . . . . . . . . 14
   |
26 | | nnmcl 6328 |
. . . . . . . . . . . . . 14
 
     |
27 | 25, 26 | sylan 279 |
. . . . . . . . . . . . 13
 
     |
28 | 27 | ancoms 266 |
. . . . . . . . . . . 12
 
     |
29 | | pinn 7058 |
. . . . . . . . . . . . 13
   |
30 | | nnmcl 6328 |
. . . . . . . . . . . . 13
 
     |
31 | 29, 30 | sylan2 282 |
. . . . . . . . . . . 12
 
     |
32 | | pinn 7058 |
. . . . . . . . . . . . 13
   |
33 | | nnmcl 6328 |
. . . . . . . . . . . . 13
 
     |
34 | 32, 33 | sylan 279 |
. . . . . . . . . . . 12
 
     |
35 | | nndi 6333 |
. . . . . . . . . . . 12
      
                            |
36 | 28, 31, 34, 35 | syl3an 1239 |
. . . . . . . . . . 11
        
                          |
37 | | simp1r 987 |
. . . . . . . . . . . 12
        
  |
38 | | simp1l 986 |
. . . . . . . . . . . 12
        
  |
39 | 31 | 3ad2ant2 984 |
. . . . . . . . . . . . 13
        
    |
40 | 34 | 3ad2ant3 985 |
. . . . . . . . . . . . 13
        
    |
41 | | nnacl 6327 |
. . . . . . . . . . . . 13
    
          |
42 | 39, 40, 41 | syl2anc 406 |
. . . . . . . . . . . 12
        
        |
43 | | nnmass 6334 |
. . . . . . . . . . . . 13
 
                             |
44 | 25, 43 | syl3an1 1230 |
. . . . . . . . . . . 12
 
                             |
45 | 37, 38, 42, 44 | syl3anc 1197 |
. . . . . . . . . . 11
        
                      |
46 | | nnmcom 6336 |
. . . . . . . . . . . . . . . . 17
 
       |
47 | 25, 46 | sylan2 282 |
. . . . . . . . . . . . . . . 16
 
       |
48 | 47 | oveq1d 5741 |
. . . . . . . . . . . . . . 15
 
               |
49 | 48 | adantr 272 |
. . . . . . . . . . . . . 14
      
              |
50 | | simpll 501 |
. . . . . . . . . . . . . . 15
      
  |
51 | 25 | ad2antlr 478 |
. . . . . . . . . . . . . . 15
      
  |
52 | | simprl 503 |
. . . . . . . . . . . . . . 15
      
  |
53 | | nnmcom 6336 |
. . . . . . . . . . . . . . . 16
 
       |
54 | 53 | adantl 273 |
. . . . . . . . . . . . . . 15
   


 
         |
55 | | nnmass 6334 |
. . . . . . . . . . . . . . . 16
 
           |
56 | 55 | adantl 273 |
. . . . . . . . . . . . . . 15
   


 

            |
57 | | simprr 504 |
. . . . . . . . . . . . . . . 16
      
  |
58 | 57, 29 | syl 14 |
. . . . . . . . . . . . . . 15
      
  |
59 | | nnmcl 6328 |
. . . . . . . . . . . . . . . 16
 
     |
60 | 59 | adantl 273 |
. . . . . . . . . . . . . . 15
   


 
       |
61 | 50, 51, 52, 54, 56, 58, 60 | caov4d 5907 |
. . . . . . . . . . . . . 14
      
              |
62 | 49, 61 | eqtr3d 2147 |
. . . . . . . . . . . . 13
      
              |
63 | 62 | 3adant3 982 |
. . . . . . . . . . . 12
        
              |
64 | 25 | ad2antlr 478 |
. . . . . . . . . . . . . 14
      
  |
65 | | simpll 501 |
. . . . . . . . . . . . . 14
      
  |
66 | | simprl 503 |
. . . . . . . . . . . . . . 15
      
  |
67 | 66, 32 | syl 14 |
. . . . . . . . . . . . . 14
      
  |
68 | 53 | adantl 273 |
. . . . . . . . . . . . . 14
   


 
         |
69 | 55 | adantl 273 |
. . . . . . . . . . . . . 14
   


 

            |
70 | | simprr 504 |
. . . . . . . . . . . . . 14
      
  |
71 | 59 | adantl 273 |
. . . . . . . . . . . . . 14
   


 
       |
72 | 64, 65, 67, 68, 69, 70, 71 | caov4d 5907 |
. . . . . . . . . . . . 13
      
              |
73 | 72 | 3adant2 981 |
. . . . . . . . . . . 12
        
              |
74 | 63, 73 | oveq12d 5744 |
. . . . . . . . . . 11
        
                              |
75 | 36, 45, 74 | 3eqtr3d 2153 |
. . . . . . . . . 10
        
                          |
76 | 24, 75 | sylbir 134 |
. . . . . . . . 9
        
                          |
77 | 37, 25 | syl 14 |
. . . . . . . . . . . 12
        
  |
78 | | mulpiord 7066 |
. . . . . . . . . . . . . . . 16
 
       |
79 | 78 | ancoms 266 |
. . . . . . . . . . . . . . 15
 
       |
80 | 79 | ad2ant2lr 499 |
. . . . . . . . . . . . . 14
      
      |
81 | 80 | 3adant1 980 |
. . . . . . . . . . . . 13
        
      |
82 | 66 | 3adant2 981 |
. . . . . . . . . . . . . . 15
        
  |
83 | 57 | 3adant3 982 |
. . . . . . . . . . . . . . 15
        
  |
84 | | mulclpi 7077 |
. . . . . . . . . . . . . . 15
 
     |
85 | 82, 83, 84 | syl2anc 406 |
. . . . . . . . . . . . . 14
        
    |
86 | | pinn 7058 |
. . . . . . . . . . . . . 14
       |
87 | 85, 86 | syl 14 |
. . . . . . . . . . . . 13
        
    |
88 | 81, 87 | eqeltrrd 2190 |
. . . . . . . . . . . 12
        
    |
89 | | nnmass 6334 |
. . . . . . . . . . . 12
 
                 |
90 | 77, 77, 88, 89 | syl3anc 1197 |
. . . . . . . . . . 11
        
              |
91 | 82, 32 | syl 14 |
. . . . . . . . . . . 12
        
  |
92 | 53 | adantl 273 |
. . . . . . . . . . . 12
   


   
         |
93 | 55 | adantl 273 |
. . . . . . . . . . . 12
   


   

            |
94 | 83, 29 | syl 14 |
. . . . . . . . . . . 12
        
  |
95 | 59 | adantl 273 |
. . . . . . . . . . . 12
   


   
       |
96 | 77, 77, 91, 92, 93, 94, 95 | caov4d 5907 |
. . . . . . . . . . 11
        
              |
97 | 90, 96 | eqtr3d 2147 |
. . . . . . . . . 10
        
              |
98 | 24, 97 | sylbir 134 |
. . . . . . . . 9
        
              |
99 | | opeq12 3671 |
. . . . . . . . . 10
                                                         
                         |
100 | 99 | eceq1d 6416 |
. . . . . . . . 9
                                                           
~Q0                         
~Q0  |
101 | 76, 98, 100 | syl2anc 406 |
. . . . . . . 8
        
                    
~Q0                         
~Q0  |
102 | | addnnnq0 7198 |
. . . . . . . . . . . 12
      
      ~Q0
+Q0      ~Q0
            
~Q0  |
103 | 102 | oveq2d 5742 |
. . . . . . . . . . 11
      
      ~Q0
·Q0      
~Q0 +Q0      ~Q0        ~Q0
·Q0              ~Q0   |
104 | 103 | adantl 273 |
. . . . . . . . . 10
     


         ~Q0 ·Q0
      ~Q0
+Q0      ~Q0        ~Q0 ·Q0
            
~Q0   |
105 | 31, 34, 41 | syl2an 285 |
. . . . . . . . . . . . 13
      
        |
106 | 105 | an42s 561 |
. . . . . . . . . . . 12
      
        |
107 | 84 | ad2ant2l 497 |
. . . . . . . . . . . . 13
      
    |
108 | 78 | eleq1d 2181 |
. . . . . . . . . . . . . 14
 
         |
109 | 108 | ad2ant2l 497 |
. . . . . . . . . . . . 13
      
  
     |
110 | 107, 109 | mpbid 146 |
. . . . . . . . . . . 12
      
    |
111 | 106, 110 | jca 302 |
. . . . . . . . . . 11
      
            |
112 | | mulnnnq0 7199 |
. . . . . . . . . . . 12
              
      ~Q0
·Q0              ~Q0
                
~Q0  |
113 | | nnmcl 6328 |
. . . . . . . . . . . . . . . 16
                   |
114 | | simpl 108 |
. . . . . . . . . . . . . . . . 17
  
    |
115 | | mulpiord 7066 |
. . . . . . . . . . . . . . . . . 18
  
            |
116 | | mulclpi 7077 |
. . . . . . . . . . . . . . . . . 18
  
        |
117 | 115, 116 | eqeltrrd 2190 |
. . . . . . . . . . . . . . . . 17
  
        |
118 | 114, 117 | jca 302 |
. . . . . . . . . . . . . . . 16
  
          |
119 | 113, 118 | anim12i 334 |
. . . . . . . . . . . . . . 15
              
                  |
120 | | an12 533 |
. . . . . . . . . . . . . . . 16
                 
                 |
121 | | 3anass 947 |
. . . . . . . . . . . . . . . 16
  
                              |
122 | 120, 121 | bitr4i 186 |
. . . . . . . . . . . . . . 15
                 
               |
123 | 119, 122 | sylib 121 |
. . . . . . . . . . . . . 14
              
        
       |
124 | 123 | an4s 560 |
. . . . . . . . . . . . 13
              
        
       |
125 | | mulcanenq0ec 7194 |
. . . . . . . . . . . . 13
  
                                 ~Q0                  ~Q0  |
126 | 124, 125 | syl 14 |
. . . . . . . . . . . 12
              
                    
~Q0                 
~Q0  |
127 | 112, 126 | eqtr4d 2148 |
. . . . . . . . . . 11
              
      ~Q0
·Q0              ~Q0
                    
~Q0  |
128 | 111, 127 | sylan2 282 |
. . . . . . . . . 10
     


         ~Q0 ·Q0
            
~Q0                     
~Q0  |
129 | 104, 128 | eqtrd 2145 |
. . . . . . . . 9
     


         ~Q0 ·Q0
      ~Q0
+Q0      ~Q0                       ~Q0  |
130 | 129 | 3impb 1158 |
. . . . . . . 8
        
      ~Q0
·Q0      
~Q0 +Q0      ~Q0                      
~Q0  |
131 | | mulnnnq0 7199 |
. . . . . . . . . . 11
      
      ~Q0
·Q0      ~Q0
        
~Q0  |
132 | | mulnnnq0 7199 |
. . . . . . . . . . 11
      
      ~Q0
·Q0      ~Q0
        
~Q0  |
133 | 131, 132 | oveqan12d 5745 |
. . . . . . . . . 10
   


 
 
           
~Q0 ·Q0     
~Q0 +Q0       ~Q0 ·Q0
    
~Q0            ~Q0 +Q0         
~Q0   |
134 | | nnmcl 6328 |
. . . . . . . . . . . . 13
 
     |
135 | | mulpiord 7066 |
. . . . . . . . . . . . . 14
 
       |
136 | | mulclpi 7077 |
. . . . . . . . . . . . . 14
 
     |
137 | 135, 136 | eqeltrrd 2190 |
. . . . . . . . . . . . 13
 
     |
138 | 134, 137 | anim12i 334 |
. . . . . . . . . . . 12
      
        |
139 | 138 | an4s 560 |
. . . . . . . . . . 11
      
        |
140 | | nnmcl 6328 |
. . . . . . . . . . . . 13
 
     |
141 | | mulpiord 7066 |
. . . . . . . . . . . . . 14
 
       |
142 | | mulclpi 7077 |
. . . . . . . . . . . . . 14
 
     |
143 | 141, 142 | eqeltrrd 2190 |
. . . . . . . . . . . . 13
 
     |
144 | 140, 143 | anim12i 334 |
. . . . . . . . . . . 12
      
        |
145 | 144 | an4s 560 |
. . . . . . . . . . 11
      
        |
146 | | addnnnq0 7198 |
. . . . . . . . . . 11
              
          ~Q0 +Q0
        
~Q0                         
~Q0  |
147 | 139, 145,
146 | syl2an 285 |
. . . . . . . . . 10
   


 
 
               ~Q0 +Q0         
~Q0                         
~Q0  |
148 | 133, 147 | eqtrd 2145 |
. . . . . . . . 9
   


 
 
           
~Q0 ·Q0     
~Q0 +Q0       ~Q0 ·Q0
    
~Q0                           ~Q0  |
149 | 148 | 3impdi 1252 |
. . . . . . . 8
        
       ~Q0 ·Q0
    
~Q0 +Q0       ~Q0 ·Q0
    
~Q0                           ~Q0  |
150 | 101, 130,
149 | 3eqtr4d 2155 |
. . . . . . 7
        
      ~Q0
·Q0      
~Q0 +Q0      ~Q0         ~Q0 ·Q0
    
~Q0 +Q0       ~Q0 ·Q0
    
~Q0    |
151 | 150 | 3expib 1165 |
. . . . . 6
 
     
 
      ~Q0
·Q0      
~Q0 +Q0      ~Q0         ~Q0 ·Q0
    
~Q0 +Q0       ~Q0 ·Q0
    
~Q0     |
152 | 1, 19, 151 | ecoptocl 6467 |
. . . . 5
 Q0     
 
 ·Q0       ~Q0
+Q0      ~Q0   
·Q0      ~Q0 +Q0  ·Q0      ~Q0     |
153 | 152 | com12 30 |
. . . 4
      
 Q0 
·Q0      
~Q0 +Q0      ~Q0    ·Q0      ~Q0 +Q0  ·Q0     
~Q0     |
154 | 1, 7, 13, 153 | 2ecoptocl 6468 |
. . 3
 
Q0
Q0
 Q0 
·Q0 
+Q0    
·Q0 
+Q0 
·Q0      |
155 | 154 | com12 30 |
. 2
 Q0   Q0 Q0 
·Q0 
+Q0    
·Q0 
+Q0 
·Q0      |
156 | 155 | 3impib 1160 |
1
 
Q0
Q0
Q0
 ·Q0  +Q0    
·Q0 
+Q0 
·Q0     |