Step | Hyp | Ref
| Expression |
1 | | mulcompi 9339 |
. . . . . . . . . . . . 13
                     |
2 | 1 | oveq1i 6318 |
. . . . . . . . . . . 12
                                             |
3 | | fvex 5889 |
. . . . . . . . . . . . 13
     |
4 | | fvex 5889 |
. . . . . . . . . . . . 13
     |
5 | | fvex 5889 |
. . . . . . . . . . . . 13
     |
6 | | mulcompi 9339 |
. . . . . . . . . . . . 13
     |
7 | | mulasspi 9340 |
. . . . . . . . . . . . 13
         |
8 | | fvex 5889 |
. . . . . . . . . . . . 13
     |
9 | 3, 4, 5, 6, 7, 8 | caov411 6520 |
. . . . . . . . . . . 12
                                             |
10 | 2, 9 | eqtri 2493 |
. . . . . . . . . . 11
                                             |
11 | | mulcompi 9339 |
. . . . . . . . . . . . 13
                     |
12 | 11 | oveq1i 6318 |
. . . . . . . . . . . 12
                                             |
13 | | fvex 5889 |
. . . . . . . . . . . . 13
     |
14 | | fvex 5889 |
. . . . . . . . . . . . 13
     |
15 | 13, 4, 5, 6, 7, 14 | caov411 6520 |
. . . . . . . . . . . 12
                                             |
16 | 12, 15 | eqtri 2493 |
. . . . . . . . . . 11
                                             |
17 | 10, 16 | oveq12i 6320 |
. . . . . . . . . 10
                                                                                             |
18 | | distrpi 9341 |
. . . . . . . . . 10
                                                                                 |
19 | | mulasspi 9340 |
. . . . . . . . . 10
                                                                     |
20 | 17, 18, 19 | 3eqtr2i 2499 |
. . . . . . . . 9
                                                                                 |
21 | | mulasspi 9340 |
. . . . . . . . . 10
                                             |
22 | 14, 5, 8, 6, 7 | caov12 6516 |
. . . . . . . . . . 11
                                 |
23 | 22 | oveq2i 6319 |
. . . . . . . . . 10
                                             |
24 | 21, 23 | eqtri 2493 |
. . . . . . . . 9
                                             |
25 | 20, 24 | opeq12i 4163 |
. . . . . . . 8
                                                                      
                                                            |
26 | | elpqn 9368 |
. . . . . . . . . . 11
     |
27 | 26 | 3ad2ant1 1051 |
. . . . . . . . . 10
 
     |
28 | | xp2nd 6843 |
. . . . . . . . . 10
  
      |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
 
       |
30 | | xp1st 6842 |
. . . . . . . . . . 11
  
      |
31 | 27, 30 | syl 17 |
. . . . . . . . . 10
 
       |
32 | | elpqn 9368 |
. . . . . . . . . . . . . 14
     |
33 | 32 | 3ad2ant2 1052 |
. . . . . . . . . . . . 13
 
     |
34 | | xp1st 6842 |
. . . . . . . . . . . . 13
  
      |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
 
       |
36 | | elpqn 9368 |
. . . . . . . . . . . . . 14
     |
37 | 36 | 3ad2ant3 1053 |
. . . . . . . . . . . . 13
 
     |
38 | | xp2nd 6843 |
. . . . . . . . . . . . 13
  
      |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
 
       |
40 | | mulclpi 9336 |
. . . . . . . . . . . 12
                       |
41 | 35, 39, 40 | syl2anc 673 |
. . . . . . . . . . 11
 
             |
42 | | xp1st 6842 |
. . . . . . . . . . . . 13
  
      |
43 | 37, 42 | syl 17 |
. . . . . . . . . . . 12
 
       |
44 | | xp2nd 6843 |
. . . . . . . . . . . . 13
  
      |
45 | 33, 44 | syl 17 |
. . . . . . . . . . . 12
 
       |
46 | | mulclpi 9336 |
. . . . . . . . . . . 12
                       |
47 | 43, 45, 46 | syl2anc 673 |
. . . . . . . . . . 11
 
             |
48 | | addclpi 9335 |
. . . . . . . . . . 11
           
                                   |
49 | 41, 47, 48 | syl2anc 673 |
. . . . . . . . . 10
 
                         |
50 | | mulclpi 9336 |
. . . . . . . . . 10
                                                           |
51 | 31, 49, 50 | syl2anc 673 |
. . . . . . . . 9
 
                               |
52 | | mulclpi 9336 |
. . . . . . . . . . 11
                       |
53 | 45, 39, 52 | syl2anc 673 |
. . . . . . . . . 10
 
             |
54 | | mulclpi 9336 |
. . . . . . . . . 10
                                   |
55 | 29, 53, 54 | syl2anc 673 |
. . . . . . . . 9
 
                   |
56 | | mulcanenq 9403 |
. . . . . . . . 9
                                                                                                                                                               |
57 | 29, 51, 55, 56 | syl3anc 1292 |
. . . . . . . 8
 
                                                                                                             |
58 | 25, 57 | syl5eqbr 4429 |
. . . . . . 7
 
                                                                                                                         |
59 | | mulpipq2 9382 |
. . . . . . . . . 10
                                  |
60 | 27, 33, 59 | syl2anc 673 |
. . . . . . . . 9
 
                            |
61 | | mulpipq2 9382 |
. . . . . . . . . 10
                                  |
62 | 27, 37, 61 | syl2anc 673 |
. . . . . . . . 9
 
                            |
63 | 60, 62 | oveq12d 6326 |
. . . . . . . 8
 
   
                                                     |
64 | | mulclpi 9336 |
. . . . . . . . . 10
                       |
65 | 31, 35, 64 | syl2anc 673 |
. . . . . . . . 9
 
             |
66 | | mulclpi 9336 |
. . . . . . . . . 10
                       |
67 | 29, 45, 66 | syl2anc 673 |
. . . . . . . . 9
 
             |
68 | | mulclpi 9336 |
. . . . . . . . . 10
                       |
69 | 31, 43, 68 | syl2anc 673 |
. . . . . . . . 9
 
             |
70 | | mulclpi 9336 |
. . . . . . . . . 10
                       |
71 | 29, 39, 70 | syl2anc 673 |
. . . . . . . . 9
 
             |
72 | | addpipq 9380 |
. . . . . . . . 9
                                  
                                                           
                                                                         |
73 | 65, 67, 69, 71, 72 | syl22anc 1293 |
. . . . . . . 8
 
                                                
                                                                         |
74 | 63, 73 | eqtrd 2505 |
. . . . . . 7
 
   
                                                                            |
75 | | relxp 4947 |
. . . . . . . . . 10
   |
76 | | 1st2nd 6858 |
. . . . . . . . . 10
   
                |
77 | 75, 27, 76 | sylancr 676 |
. . . . . . . . 9
 
              |
78 | | addpipq2 9379 |
. . . . . . . . . 10
                                              |
79 | 33, 37, 78 | syl2anc 673 |
. . . . . . . . 9
 
                                        |
80 | 77, 79 | oveq12d 6326 |
. . . . . . . 8
 
                                                       |
81 | | mulpipq 9383 |
. . . . . . . . 9
                                                                                              
                                                 |
82 | 31, 29, 49, 53, 81 | syl22anc 1293 |
. . . . . . . 8
 
                                                
                                                 |
83 | 80, 82 | eqtrd 2505 |
. . . . . . 7
 
                                                      |
84 | 58, 74, 83 | 3brtr4d 4426 |
. . . . . 6
 
   
   
     |
85 | | mulpqf 9389 |
. . . . . . . . . 10
   
        |
86 | 85 | fovcl 6420 |
. . . . . . . . 9
             |
87 | 27, 33, 86 | syl2anc 673 |
. . . . . . . 8
 
       |
88 | 85 | fovcl 6420 |
. . . . . . . . 9
             |
89 | 27, 37, 88 | syl2anc 673 |
. . . . . . . 8
 
       |
90 | | addpqf 9387 |
. . . . . . . . 9
   
        |
91 | 90 | fovcl 6420 |
. . . . . . . 8
             
       |
92 | 87, 89, 91 | syl2anc 673 |
. . . . . . 7
 
   
       |
93 | 90 | fovcl 6420 |
. . . . . . . . 9
             |
94 | 33, 37, 93 | syl2anc 673 |
. . . . . . . 8
 
       |
95 | 85 | fovcl 6420 |
. . . . . . . 8
                 |
96 | 27, 94, 95 | syl2anc 673 |
. . . . . . 7
 
         |
97 | | nqereq 9378 |
. . . . . . 7
         
      
   
   
        
       
       |
98 | 92, 96, 97 | syl2anc 673 |
. . . . . 6
 
         
                
      |
99 | 84, 98 | mpbid 215 |
. . . . 5
 
       
             |
100 | 99 | eqcomd 2477 |
. . . 4
 
     
               |
101 | | mulerpq 9400 |
. . . 4
        
            |
102 | | adderpq 9399 |
. . . 4
          
              |
103 | 100, 101,
102 | 3eqtr4g 2530 |
. . 3
 
                 
           |
104 | | nqerid 9376 |
. . . . . 6
       |
105 | 104 | eqcomd 2477 |
. . . . 5
       |
106 | 105 | 3ad2ant1 1051 |
. . . 4
 
       |
107 | | addpqnq 9381 |
. . . . 5
 
           |
108 | 107 | 3adant1 1048 |
. . . 4
 
           |
109 | 106, 108 | oveq12d 6326 |
. . 3
 
                   |
110 | | mulpqnq 9384 |
. . . . 5
 
           |
111 | 110 | 3adant3 1050 |
. . . 4
 
           |
112 | | mulpqnq 9384 |
. . . . 5
 
           |
113 | 112 | 3adant2 1049 |
. . . 4
 
           |
114 | 111, 113 | oveq12d 6326 |
. . 3
 
                       |
115 | 103, 109,
114 | 3eqtr4d 2515 |
. 2
 
             |
116 | | addnqf 9391 |
. . . 4
      |
117 | 116 | fdmi 5746 |
. . 3
   |
118 | | 0nnq 9367 |
. . 3
 |
119 | | mulnqf 9392 |
. . . 4
      |
120 | 119 | fdmi 5746 |
. . 3
   |
121 | 117, 118,
120 | ndmovdistr 6477 |
. 2
 
             |
122 | 115, 121 | pm2.61i 169 |
1
           |