Step | Hyp | Ref
| Expression |
1 | | dfcnqs 7818 |
. 2
      |
2 | | mulcnsrec 7820 |
. 2
      
      ![] ]](rbrack.gif)
     ![] ]](rbrack.gif)       
            ![] ]](rbrack.gif)  |
3 | | mulcnsrec 7820 |
. 2
      
      ![] ]](rbrack.gif)      ![] ]](rbrack.gif)
                   ![] ]](rbrack.gif)  |
4 | | mulcnsrec 7820 |
. 2
       
      
     
                    ![] ]](rbrack.gif)      ![] ]](rbrack.gif)
        
                              
       ![] ]](rbrack.gif)  |
5 | | mulcnsrec 7820 |
. 2
         
      
   
      ![] ]](rbrack.gif)
      
            ![] ]](rbrack.gif)         
     
 
              
        
      ![] ]](rbrack.gif)
 |
6 | | mulclsr 7731 |
. . . . 5
 
     |
7 | | m1r 7729 |
. . . . . 6
 |
8 | | mulclsr 7731 |
. . . . . 6
 
     |
9 | | mulclsr 7731 |
. . . . . 6
      
    |
10 | 7, 8, 9 | sylancr 414 |
. . . . 5
 
  
    |
11 | | addclsr 7730 |
. . . . 5
                   |
12 | 6, 10, 11 | syl2an 289 |
. . . 4
      
 
  
     |
13 | 12 | an4s 588 |
. . 3
      
 
  
     |
14 | | mulclsr 7731 |
. . . . 5
 
     |
15 | | mulclsr 7731 |
. . . . 5
 
     |
16 | | addclsr 7730 |
. . . . 5
    
     
    |
17 | 14, 15, 16 | syl2anr 290 |
. . . 4
      
 
      |
18 | 17 | an42s 589 |
. . 3
      
 
      |
19 | 13, 18 | jca 306 |
. 2
      
                  |
20 | | mulclsr 7731 |
. . . . 5
 
     |
21 | | mulclsr 7731 |
. . . . . 6
 
     |
22 | | mulclsr 7731 |
. . . . . 6
  
   
    |
23 | 7, 21, 22 | sylancr 414 |
. . . . 5
 
  
    |
24 | | addclsr 7730 |
. . . . 5
                   |
25 | 20, 23, 24 | syl2an 289 |
. . . 4
      
 
  
     |
26 | 25 | an4s 588 |
. . 3
      
 
  
     |
27 | | mulclsr 7731 |
. . . . 5
 
     |
28 | | mulclsr 7731 |
. . . . 5
 
     |
29 | | addclsr 7730 |
. . . . 5
          
    |
30 | 27, 28, 29 | syl2anr 290 |
. . . 4
      
 
      |
31 | 30 | an42s 589 |
. . 3
      
 
      |
32 | 26, 31 | jca 306 |
. 2
      
                  |
33 | | simp1l 1021 |
. . . . 5
        
  |
34 | | simp2l 1023 |
. . . . . 6
        
  |
35 | | simp3l 1025 |
. . . . . 6
        
  |
36 | 34, 35, 20 | syl2anc 411 |
. . . . 5
        
    |
37 | | mulclsr 7731 |
. . . . 5
      
    |
38 | 33, 36, 37 | syl2anc 411 |
. . . 4
        
      |
39 | | simp2r 1024 |
. . . . . . 7
        
  |
40 | | simp3r 1026 |
. . . . . . 7
        
  |
41 | 39, 40, 21 | syl2anc 411 |
. . . . . 6
        
    |
42 | 7, 41, 22 | sylancr 414 |
. . . . 5
        
      |
43 | | mulclsr 7731 |
. . . . 5
               |
44 | 33, 42, 43 | syl2anc 411 |
. . . 4
        
  
     |
45 | | simp1r 1022 |
. . . . . 6
        
  |
46 | 39, 35, 27 | syl2anc 411 |
. . . . . 6
        
    |
47 | | mulclsr 7731 |
. . . . . 6
  
   
    |
48 | 45, 46, 47 | syl2anc 411 |
. . . . 5
        
      |
49 | | mulclsr 7731 |
. . . . 5
   
    
      |
50 | 7, 48, 49 | sylancr 414 |
. . . 4
        
  
     |
51 | | addcomsrg 7732 |
. . . . 5
 
       |
52 | 51 | adantl 277 |
. . . 4
   


   
         |
53 | | addasssrg 7733 |
. . . . 5
 
           |
54 | 53 | adantl 277 |
. . . 4
   


   

            |
55 | 34, 40, 28 | syl2anc 411 |
. . . . . 6
        
    |
56 | | mulclsr 7731 |
. . . . . 6
      
    |
57 | 45, 55, 56 | syl2anc 411 |
. . . . 5
        
      |
58 | | mulclsr 7731 |
. . . . 5
   
    
      |
59 | 7, 57, 58 | sylancr 414 |
. . . 4
        
  
     |
60 | | addclsr 7730 |
. . . . 5
 
     |
61 | 60 | adantl 277 |
. . . 4
   


   
       |
62 | 38, 44, 50, 52, 54, 59, 61 | caov42d 6054 |
. . 3
        
   
    
       
    
              
                     |
63 | | distrsrg 7736 |
. . . . 5
                                 |
64 | 33, 36, 42, 63 | syl3anc 1238 |
. . . 4
        
                        |
65 | | distrsrg 7736 |
. . . . . . 7
  
                        |
66 | 45, 46, 55, 65 | syl3anc 1238 |
. . . . . 6
        
    
     
         |
67 | 66 | oveq2d 5884 |
. . . . 5
        
                        |
68 | 7 | a1i 9 |
. . . . . 6
        
  |
69 | | distrsrg 7736 |
. . . . . 6
   
   
      
                 
      |
70 | 68, 48, 57, 69 | syl3anc 1238 |
. . . . 5
        
   
  
              
      |
71 | 67, 70 | eqtrd 2210 |
. . . 4
        
            
      
      |
72 | 64, 71 | oveq12d 5886 |
. . 3
        
 
 
  
     
 
          
    
       
    
        |
73 | | mulcomsrg 7734 |
. . . . . . 7
 
       |
74 | 73 | adantl 277 |
. . . . . 6
   


   
         |
75 | | distrsrg 7736 |
. . . . . . . . 9
 
 
      
    |
76 | 75 | 3coml 1210 |
. . . . . . . 8
 
 
      
    |
77 | | simp3 999 |
. . . . . . . . 9
 
   |
78 | 60 | 3adant3 1017 |
. . . . . . . . 9
 
     |
79 | | mulcomsrg 7734 |
. . . . . . . . 9
               |
80 | 77, 78, 79 | syl2anc 411 |
. . . . . . . 8
 
 
         |
81 | | simp1 997 |
. . . . . . . . . 10
 
   |
82 | | mulcomsrg 7734 |
. . . . . . . . . 10
 
       |
83 | 77, 81, 82 | syl2anc 411 |
. . . . . . . . 9
 
 
     |
84 | | simp2 998 |
. . . . . . . . . 10
 
   |
85 | | mulcomsrg 7734 |
. . . . . . . . . 10
 
       |
86 | 77, 84, 85 | syl2anc 411 |
. . . . . . . . 9
 
 
     |
87 | 83, 86 | oveq12d 5886 |
. . . . . . . 8
 
               |
88 | 76, 80, 87 | 3eqtr3d 2218 |
. . . . . . 7
 
   
         |
89 | 88 | adantl 277 |
. . . . . 6
   


   

    
         |
90 | | mulasssrg 7735 |
. . . . . . 7
 
   
       |
91 | 90 | adantl 277 |
. . . . . 6
   


   

    
       |
92 | | mulclsr 7731 |
. . . . . . 7
 
     |
93 | 92 | adantl 277 |
. . . . . 6
   


   
       |
94 | 45, 39, 8 | syl2anc 411 |
. . . . . 6
        
    |
95 | 74, 89, 91, 93, 33, 68, 34, 94, 35 | caovdilemd 6059 |
. . . . 5
        
                        |
96 | | mulasssrg 7735 |
. . . . . . . 8
 
   
  
    |
97 | 45, 39, 35, 96 | syl3anc 1238 |
. . . . . . 7
        
 
        |
98 | 97 | oveq2d 5884 |
. . . . . 6
        
              |
99 | 98 | oveq2d 5884 |
. . . . 5
        
 
      
     
    
      |
100 | 95, 99 | eqtrd 2210 |
. . . 4
        
                 
      |
101 | 74, 89, 91, 93, 45, 33, 34, 39, 40 | caovdilemd 6059 |
. . . . . 6
        
             
      |
102 | 101 | oveq2d 5884 |
. . . . 5
        
                 
      |
103 | 93, 33, 41 | caovcld 6021 |
. . . . . 6
        
      |
104 | | distrsrg 7736 |
. . . . . 6
   
  

      
                

      |
105 | 68, 57, 103, 104 | syl3anc 1238 |
. . . . 5
        
      
             

      |
106 | 68, 33, 41, 74, 91 | caov12d 6049 |
. . . . . 6
        
  
           |
107 | 106 | oveq2d 5884 |
. . . . 5
        
        
                     |
108 | 102, 105,
107 | 3eqtrd 2214 |
. . . 4
        
            
             |
109 | 100, 108 | oveq12d 5886 |
. . 3
        
                
 
           
                     |
110 | 62, 72, 109 | 3eqtr4rd 2221 |
. 2
        
                
 
                   
       |
111 | 93, 45, 36 | caovcld 6021 |
. . . 4
        
      |
112 | 93, 45, 42 | caovcld 6021 |
. . . 4
        
  
     |
113 | 93, 33, 46 | caovcld 6021 |
. . . 4
        
      |
114 | 93, 33, 55 | caovcld 6021 |
. . . 4
        
      |
115 | 111, 112,
113, 52, 54, 114, 61 | caov42d 6054 |
. . 3
        
   
    
          
           
     
    
       |
116 | | distrsrg 7736 |
. . . . 5
                                 |
117 | 45, 36, 42, 116 | syl3anc 1238 |
. . . 4
        
                        |
118 | | distrsrg 7736 |
. . . . 5
  
                        |
119 | 33, 46, 55, 118 | syl3anc 1238 |
. . . 4
        
    
     
         |
120 | 117, 119 | oveq12d 5886 |
. . 3
        
 
 
  
                   
            
      |
121 | 74, 89, 91, 93, 45, 33, 34, 39, 35 | caovdilemd 6059 |
. . . 4
        
             
      |
122 | 74, 89, 91, 93, 33, 68, 34, 94, 40 | caovdilemd 6059 |
. . . . 5
        
                        |
123 | | mulasssrg 7735 |
. . . . . . . . 9
 
   
  
    |
124 | 45, 39, 40, 123 | syl3anc 1238 |
. . . . . . . 8
        
 
        |
125 | 124 | oveq2d 5884 |
. . . . . . 7
        
              |
126 | 68, 45, 41, 74, 91 | caov12d 6049 |
. . . . . . 7
        
  
           |
127 | 125, 126 | eqtrd 2210 |
. . . . . 6
        
              |
128 | 127 | oveq2d 5884 |
. . . . 5
        
 
      
     
    
      |
129 | 122, 128 | eqtrd 2210 |
. . . 4
        
               
        |
130 | 121, 129 | oveq12d 5886 |
. . 3
        
     
 
      
           
                   |
131 | 115, 120,
130 | 3eqtr4rd 2221 |
. 2
        
     
 
      
                           |
132 | 1, 2, 3, 4, 5, 19,
32, 110, 131 | ecoviass 6638 |
1
 
      
    |