Step | Hyp | Ref
| Expression |
1 | | rpvmasum.a |
. . . . . . 7
   |
2 | 1 | adantr 467 |
. . . . . 6
 

  |
3 | | rpvmasum2.g |
. . . . . . 7
DChr   |
4 | | rpvmasum2.d |
. . . . . . 7
     |
5 | 3, 4 | dchrfi 24183 |
. . . . . 6
   |
6 | 2, 5 | syl 17 |
. . . . 5
 

  |
7 | | fzfid 12186 |
. . . . . 6
               |
8 | | rpvmasum.z |
. . . . . . . . . . . . 13
ℤ/nℤ   |
9 | | eqid 2451 |
. . . . . . . . . . . . 13
         |
10 | | simpr 463 |
. . . . . . . . . . . . 13
 
   |
11 | 3, 8, 4, 9, 10 | dchrf 24170 |
. . . . . . . . . . . 12
 
           |
12 | | rpvmasum2.u |
. . . . . . . . . . . . . . 15
Unit   |
13 | 9, 12 | unitss 17888 |
. . . . . . . . . . . . . 14
     |
14 | | rpvmasum2.b |
. . . . . . . . . . . . . 14
   |
15 | 13, 14 | sseldi 3430 |
. . . . . . . . . . . . 13
       |
16 | 15 | adantr 467 |
. . . . . . . . . . . 12
 
       |
17 | 11, 16 | ffvelrnd 6023 |
. . . . . . . . . . 11
 
       |
18 | 17 | cjcld 13259 |
. . . . . . . . . 10
 
           |
19 | 18 | adantlr 721 |
. . . . . . . . 9
               |
20 | 19 | adantrl 722 |
. . . . . . . 8
            
 
          |
21 | 11 | adantlr 721 |
. . . . . . . . . . . 12
               |
22 | 21 | adantlr 721 |
. . . . . . . . . . 11
   

         
          |
23 | 1 | nnnn0d 10925 |
. . . . . . . . . . . . . . 15
   |
24 | | rpvmasum.l |
. . . . . . . . . . . . . . . 16
 RHom   |
25 | 8, 9, 24 | znzrhfo 19118 |
. . . . . . . . . . . . . . 15

          |
26 | | fof 5793 |
. . . . . . . . . . . . . . 15
                   |
27 | 23, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . 14
           |
28 | 27 | adantr 467 |
. . . . . . . . . . . . 13
 

          |
29 | | elfzelz 11800 |
. . . . . . . . . . . . 13
           |
30 | | ffvelrn 6020 |
. . . . . . . . . . . . 13
                     |
31 | 28, 29, 30 | syl2an 480 |
. . . . . . . . . . . 12
            
          |
32 | 31 | adantr 467 |
. . . . . . . . . . 11
   

         
          |
33 | 22, 32 | ffvelrnd 6023 |
. . . . . . . . . 10
   

         
          |
34 | 33 | anasss 653 |
. . . . . . . . 9
            
 
          |
35 | | elfznn 11828 |
. . . . . . . . . . . . . 14
           |
36 | 35 | adantl 468 |
. . . . . . . . . . . . 13
            
  |
37 | | vmacl 24045 |
. . . . . . . . . . . . 13
 Λ    |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
            
Λ    |
39 | 38, 36 | nndivred 10658 |
. . . . . . . . . . 11
            
 Λ     |
40 | 39 | recnd 9669 |
. . . . . . . . . 10
            
 Λ     |
41 | 40 | adantrr 723 |
. . . . . . . . 9
            
 
 Λ     |
42 | 34, 41 | mulcld 9663 |
. . . . . . . 8
            
 
          Λ      |
43 | 20, 42 | mulcld 9663 |
. . . . . . 7
            
 
                   Λ       |
44 | 43 | anass1rs 816 |
. . . . . 6
   


                            Λ       |
45 | 7, 44 | fsumcl 13799 |
. . . . 5
                                  Λ       |
46 | | relogcl 23525 |
. . . . . . . . 9

      |
47 | 46 | adantl 468 |
. . . . . . . 8
 

      |
48 | 47 | recnd 9669 |
. . . . . . 7
 

      |
49 | 48 | adantr 467 |
. . . . . 6
           |
50 | | ax-1cn 9597 |
. . . . . . 7
 |
51 | | neg1cn 10713 |
. . . . . . . 8
  |
52 | | 0cn 9635 |
. . . . . . . 8
 |
53 | 51, 52 | keepel 3948 |
. . . . . . 7
       |
54 | 50, 53 | keepel 3948 |
. . . . . 6
           |
55 | | mulcl 9623 |
. . . . . 6
                                   |
56 | 49, 54, 55 | sylancl 668 |
. . . . 5
                       |
57 | 6, 45, 56 | fsumsub 13849 |
. . . 4
 

                               Λ                                                     Λ     
                   |
58 | 42 | anass1rs 816 |
. . . . . . . 8
   


                   Λ      |
59 | 7, 58 | fsumcl 13799 |
. . . . . . 7
                         Λ      |
60 | 19, 59, 56 | subdid 10074 |
. . . . . 6
                                   Λ                                                    Λ                                  |
61 | 7, 19, 58 | fsummulc2 13845 |
. . . . . . 7
                                  Λ     
                            Λ       |
62 | 54 | a1i 11 |
. . . . . . . . 9
                 |
63 | 19, 49, 62 | mul12d 9842 |
. . . . . . . 8
                                                           |
64 | | ovif2 6374 |
. . . . . . . . . 10
                                                   |
65 | | fveq1 5864 |
. . . . . . . . . . . . . . . . 17
    
    |
66 | | rpvmasum2.1 |
. . . . . . . . . . . . . . . . . 18
     |
67 | 1 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
       |
68 | 14 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
       |
69 | 3, 8, 66, 12, 67, 68 | dchr1 24185 |
. . . . . . . . . . . . . . . . 17
         |
70 | 65, 69 | sylan9eqr 2507 |
. . . . . . . . . . . . . . . 16
   


      |
71 | 70 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
   


              |
72 | | 1re 9642 |
. . . . . . . . . . . . . . . 16
 |
73 | | cjre 13202 |
. . . . . . . . . . . . . . . 16
       |
74 | 72, 73 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     |
75 | 71, 74 | syl6eq 2501 |
. . . . . . . . . . . . . 14
   


          |
76 | 75 | oveq1d 6305 |
. . . . . . . . . . . . 13
   


              |
77 | | 1t1e1 10757 |
. . . . . . . . . . . . 13
   |
78 | 76, 77 | syl6eq 2501 |
. . . . . . . . . . . 12
   


            |
79 | 78 | ifeq1da 3911 |
. . . . . . . . . . 11
                                                         |
80 | | df-ne 2624 |
. . . . . . . . . . . . 13

 |
81 | | ovif2 6374 |
. . . . . . . . . . . . . 14
                                           |
82 | | simplll 768 |
. . . . . . . . . . . . . . . . . . . . . 22
   


  |
83 | | rpvmasum2.z1 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
84 | 83 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
85 | 82, 84 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . 21
     

               |
86 | 3, 8, 4 | dchrmhm 24169 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 mulGrp  MndHom mulGrp ℂfld  |
87 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
88 | 86, 87 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . . 23
      mulGrp  MndHom mulGrp ℂfld   |
89 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
mulGrp  mulGrp   |
90 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
91 | 89, 90 | ringidval 17737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       mulGrp    |
92 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
mulGrp ℂfld mulGrp ℂfld |
93 | | cnfld1 18993 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  ℂfld |
94 | 92, 93 | ringidval 17737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   mulGrp ℂfld  |
95 | 91, 94 | mhm0 16590 |
. . . . . . . . . . . . . . . . . . . . . . 23
  mulGrp 
MndHom mulGrp ℂfld           |
96 | 88, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
97 | 96 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . 21
     

           |
98 | 85, 97 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . 20
     

       |
99 | 98 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
     

               |
100 | 99, 74 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . 18
     

           |
101 | 100 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
     

                 |
102 | 51 | mulid2i 9646 |
. . . . . . . . . . . . . . . . 17
     |
103 | 101, 102 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
     

               |
104 | 103 | ifeq1da 3911 |
. . . . . . . . . . . . . . 15
   


                                            |
105 | 19 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   


          |
106 | 105 | mul01d 9832 |
. . . . . . . . . . . . . . . 16
   


            |
107 | 106 | ifeq2d 3900 |
. . . . . . . . . . . . . . 15
   


                        |
108 | 104, 107 | eqtrd 2485 |
. . . . . . . . . . . . . 14
   


                                  |
109 | 81, 108 | syl5eq 2497 |
. . . . . . . . . . . . 13
   


                        |
110 | 80, 109 | sylan2br 479 |
. . . . . . . . . . . 12
   


                        |
111 | 110 | ifeq2da 3912 |
. . . . . . . . . . 11
                                     |
112 | 79, 111 | eqtrd 2485 |
. . . . . . . . . 10
                                               |
113 | 64, 112 | syl5eq 2497 |
. . . . . . . . 9
                                     |
114 | 113 | oveq2d 6306 |
. . . . . . . 8
                                                 |
115 | 63, 114 | eqtrd 2485 |
. . . . . . 7
                                                 |
116 | 61, 115 | oveq12d 6308 |
. . . . . 6
                                   Λ                                                              Λ                        |
117 | 60, 116 | eqtrd 2485 |
. . . . 5
                                   Λ                                                    Λ                        |
118 | 117 | sumeq2dv 13769 |
. . . 4
 

                               Λ                                                     Λ                        |
119 | | fzfid 12186 |
. . . . . . . . 9
 

          |
120 | | inss1 3652 |
. . . . . . . . 9
                   |
121 | | ssfi 7792 |
. . . . . . . . 9
                            
            |
122 | 119, 120,
121 | sylancl 668 |
. . . . . . . 8
 

            |
123 | 2 | phicld 14720 |
. . . . . . . . 9
 

      |
124 | 123 | nncnd 10625 |
. . . . . . . 8
 

      |
125 | 120 | a1i 11 |
. . . . . . . . . 10
 

                    |
126 | 125 | sselda 3432 |
. . . . . . . . 9
                         |
127 | 126, 40 | syldan 473 |
. . . . . . . 8
                Λ     |
128 | 122, 124,
127 | fsummulc2 13845 |
. . . . . . 7
 

     
            Λ    
                 Λ      |
129 | 124 | adantr 467 |
. . . . . . . . . . 11
            
      |
130 | 129, 40 | mulcld 9663 |
. . . . . . . . . 10
            
      Λ      |
131 | 126, 130 | syldan 473 |
. . . . . . . . 9
                     Λ      |
132 | 131 | ralrimiva 2802 |
. . . . . . . 8
 

                  Λ      |
133 | 119 | olcd 395 |
. . . . . . . 8
 

                        |
134 | | sumss2 13792 |
. . . . . . . 8
                                       Λ                                              Λ                                 Λ        |
135 | 125, 132,
133, 134 | syl21anc 1267 |
. . . . . . 7
 

                  Λ    
                            Λ        |
136 | | elin 3617 |
. . . . . . . . . . . . 13
          
            |
137 | 136 | baib 914 |
. . . . . . . . . . . 12
                   
   |
138 | 137 | adantl 468 |
. . . . . . . . . . 11
            
          
   |
139 | | rpvmasum2.t |
. . . . . . . . . . . . 13
        |
140 | 139 | eleq2i 2521 |
. . . . . . . . . . . 12

         |
141 | | ffn 5728 |
. . . . . . . . . . . . . 14
           |
142 | 28, 141 | syl 17 |
. . . . . . . . . . . . 13
 

  |
143 | | fniniseg 6003 |
. . . . . . . . . . . . . 14
        
         |
144 | 143 | baibd 920 |
. . . . . . . . . . . . 13
 
        
       |
145 | 142, 29, 144 | syl2an 480 |
. . . . . . . . . . . 12
            
       
       |
146 | 140, 145 | syl5bb 261 |
. . . . . . . . . . 11
            

       |
147 | 138, 146 | bitr2d 258 |
. . . . . . . . . 10
            
    
             |
148 | 40 | mul02d 9831 |
. . . . . . . . . 10
            
  Λ      |
149 | 147, 148 | ifbieq2d 3906 |
. . . . . . . . 9
            
             Λ       Λ                        Λ        |
150 | | ovif 6373 |
. . . . . . . . . 10
               Λ                 Λ       Λ      |
151 | 1 | ad2antrr 732 |
. . . . . . . . . . . . 13
            
  |
152 | 151, 5 | syl 17 |
. . . . . . . . . . . 12
            
  |
153 | 19 | adantlr 721 |
. . . . . . . . . . . . 13
   

         
          |
154 | 33, 153 | mulcld 9663 |
. . . . . . . . . . . 12
   

         
                    |
155 | 152, 40, 154 | fsummulc1 13846 |
. . . . . . . . . . 11
            
 
                   Λ    
                    Λ      |
156 | 14 | ad2antrr 732 |
. . . . . . . . . . . . 13
            
  |
157 | 3, 4, 8, 9, 12, 151, 31, 156 | sum2dchr 24202 |
. . . . . . . . . . . 12
            
                                  |
158 | 157 | oveq1d 6305 |
. . . . . . . . . . 11
            
 
                   Λ                   Λ      |
159 | 40 | adantr 467 |
. . . . . . . . . . . . 13
   

         
 Λ     |
160 | | mulass 9627 |
. . . . . . . . . . . . . 14
                   Λ                        Λ                       Λ       |
161 | | mul12 9799 |
. . . . . . . . . . . . . 14
                   Λ                       Λ                        Λ       |
162 | 160, 161 | eqtrd 2485 |
. . . . . . . . . . . . 13
                   Λ                        Λ                       Λ       |
163 | 33, 153, 159, 162 | syl3anc 1268 |
. . . . . . . . . . . 12
   

         
                    Λ                       Λ       |
164 | 163 | sumeq2dv 13769 |
. . . . . . . . . . 11
            
                     Λ    
                   Λ       |
165 | 155, 158,
164 | 3eqtr3d 2493 |
. . . . . . . . . 10
            
               Λ    
                   Λ       |
166 | 150, 165 | syl5eqr 2499 |
. . . . . . . . 9
            
             Λ       Λ                         Λ       |
167 | 149, 166 | eqtr3d 2487 |
. . . . . . . 8
            
                   Λ      
                   Λ       |
168 | 167 | sumeq2dv 13769 |
. . . . . . 7
 

                             Λ                                    Λ       |
169 | 128, 135,
168 | 3eqtrd 2489 |
. . . . . 6
 

     
            Λ    
         
                   Λ       |
170 | 119, 6, 43 | fsumcom 13836 |
. . . . . 6
 

                              Λ                                   Λ       |
171 | 169, 170 | eqtrd 2485 |
. . . . 5
 

     
            Λ                                  Λ       |
172 | 3 | dchrabl 24182 |
. . . . . . . . . 10
   |
173 | | ablgrp 17435 |
. . . . . . . . . 10

  |
174 | 4, 66 | grpidcl 16694 |
. . . . . . . . . 10
   |
175 | 2, 172, 173, 174 | 4syl 19 |
. . . . . . . . 9
 

  |
176 | 48 | mulid1d 9660 |
. . . . . . . . . 10
 

            |
177 | 176, 48 | eqeltrd 2529 |
. . . . . . . . 9
 

        |
178 | | iftrue 3887 |
. . . . . . . . . . 11
             |
179 | 178 | oveq2d 6306 |
. . . . . . . . . 10
                         |
180 | 179 | sumsn 13807 |
. . . . . . . . 9
                                 |
181 | 175, 177,
180 | syl2anc 667 |
. . . . . . . 8
 

                         |
182 | | eldifsn 4097 |
. . . . . . . . . . 11
  

  |
183 | | ifnefalse 3893 |
. . . . . . . . . . . . . . 15
                   |
184 | 183 | ad2antll 735 |
. . . . . . . . . . . . . 14
                        |
185 | | negeq 9867 |
. . . . . . . . . . . . . . 15
               |
186 | | negeq 9867 |
. . . . . . . . . . . . . . . 16
               |
187 | | neg0 9920 |
. . . . . . . . . . . . . . . 16
  |
188 | 186, 187 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
              |
189 | 185, 188 | ifsb 3894 |
. . . . . . . . . . . . . 14
             |
190 | 184, 189 | syl6eqr 2503 |
. . . . . . . . . . . . 13
                        |
191 | 190 | oveq2d 6306 |
. . . . . . . . . . . 12
                                    |
192 | 48 | adantr 467 |
. . . . . . . . . . . . 13
            |
193 | 50, 52 | keepel 3948 |
. . . . . . . . . . . . 13
      |
194 | | mulneg2 10056 |
. . . . . . . . . . . . 13
                                      |
195 | 192, 193,
194 | sylancl 668 |
. . . . . . . . . . . 12
                                |
196 | 191, 195 | eqtrd 2485 |
. . . . . . . . . . 11
                                    |
197 | 182, 196 | sylan2b 478 |
. . . . . . . . . 10
                                     |
198 | 197 | sumeq2dv 13769 |
. . . . . . . . 9
 

                    
                 |
199 | | diffi 7803 |
. . . . . . . . . . 11
     |
200 | 6, 199 | syl 17 |
. . . . . . . . . 10
 

    |
201 | 48 | adantr 467 |
. . . . . . . . . . 11
             |
202 | | mulcl 9623 |
. . . . . . . . . . 11
                         |
203 | 201, 193,
202 | sylancl 668 |
. . . . . . . . . 10
                    |
204 | 200, 203 | fsumneg 13848 |
. . . . . . . . 9
 

                                  |
205 | 193 | a1i 11 |
. . . . . . . . . . . 12
              |
206 | 200, 48, 205 | fsummulc2 13845 |
. . . . . . . . . . 11
 

                                |
207 | | rpvmasum2.w |
. . . . . . . . . . . . . . . . 17
                |
208 | | ssrab2 3514 |
. . . . . . . . . . . . . . . . 17
   
           
  |
209 | 207, 208 | eqsstri 3462 |
. . . . . . . . . . . . . . . 16

  |
210 | | difss 3560 |
. . . . . . . . . . . . . . . 16
 
 |
211 | 209, 210 | sstri 3441 |
. . . . . . . . . . . . . . 15
 |
212 | | ssfi 7792 |
. . . . . . . . . . . . . . 15
  
  |
213 | 6, 211, 212 | sylancl 668 |
. . . . . . . . . . . . . 14
 

  |
214 | | fsumconst 13851 |
. . . . . . . . . . . . . 14
 
          |
215 | 213, 50, 214 | sylancl 668 |
. . . . . . . . . . . . 13
 

         |
216 | 209 | a1i 11 |
. . . . . . . . . . . . . 14
 

    |
217 | 50 | a1i 11 |
. . . . . . . . . . . . . . 15
 

  |
218 | 217 | ralrimivw 2803 |
. . . . . . . . . . . . . 14
 


  |
219 | 200 | olcd 395 |
. . . . . . . . . . . . . 14
 

  
         |
220 | | sumss2 13792 |
. . . . . . . . . . . . . 14
    


           
           |
221 | 216, 218,
219, 220 | syl21anc 1267 |
. . . . . . . . . . . . 13
 

 
          |
222 | | hashcl 12538 |
. . . . . . . . . . . . . . . 16
       |
223 | 213, 222 | syl 17 |
. . . . . . . . . . . . . . 15
 

      |
224 | 223 | nn0cnd 10927 |
. . . . . . . . . . . . . 14
 

      |
225 | 224 | mulid1d 9660 |
. . . . . . . . . . . . 13
 

            |
226 | 215, 221,
225 | 3eqtr3d 2493 |
. . . . . . . . . . . 12
 

               |
227 | 226 | oveq2d 6306 |
. . . . . . . . . . 11
 

                           |
228 | 206, 227 | eqtr3d 2487 |
. . . . . . . . . 10
 

                           |
229 | 228 | negeqd 9869 |
. . . . . . . . 9
 

                             |
230 | 198, 204,
229 | 3eqtrd 2489 |
. . . . . . . 8
 

                                 |
231 | 181, 230 | oveq12d 6308 |
. . . . . . 7
 

 
                
                                         |
232 | 48, 224 | mulcld 9663 |
. . . . . . . 8
 

            |
233 | 177, 232 | negsubd 9992 |
. . . . . . 7
 

                                       |
234 | 231, 233 | eqtrd 2485 |
. . . . . 6
 

 
                
                                        |
235 | | disjdif 3839 |
. . . . . . . 8
     |
236 | 235 | a1i 11 |
. . . . . . 7
 

      |
237 | | undif2 3843 |
. . . . . . . 8
       |
238 | 175 | snssd 4117 |
. . . . . . . . 9
 

  |
239 | | ssequn1 3604 |
. . . . . . . . 9
     |
240 | 238, 239 | sylib 200 |
. . . . . . . 8
 

    |
241 | 237, 240 | syl5req 2498 |
. . . . . . 7
 



    |
242 | 236, 241,
6, 56 | fsumsplit 13806 |
. . . . . 6
 

                                                          |
243 | 48, 217, 224 | subdid 10074 |
. . . . . 6
 

                                |
244 | 234, 242,
243 | 3eqtr4rd 2496 |
. . . . 5
 

            
                  |
245 | 171, 244 | oveq12d 6308 |
. . . 4
 

                   Λ                  
                             Λ                         |
246 | 57, 118, 245 | 3eqtr4d 2495 |
. . 3
 

                               Λ                                         Λ                   |
247 | 246 | mpteq2dva 4489 |
. 2
                                 Λ                       
                   Λ                    |
248 | | rpssre 11312 |
. . . 4
 |
249 | 248 | a1i 11 |
. . 3
   |
250 | 1, 5 | syl 17 |
. . 3
   |
251 | 17 | adantlr 721 |
. . . . . 6
           |
252 | 251 | cjcld 13259 |
. . . . 5
               |
253 | 59, 56 | subcld 9986 |
. . . . 5
                          Λ                       |
254 | 252, 253 | mulcld 9663 |
. . . 4
                                   Λ                        |
255 | 254 | anasss 653 |
. . 3
 
                                 Λ                        |
256 | 18 | adantr 467 |
. . . 4
               |
257 | 253 | an32s 813 |
. . . 4
                          Λ                       |
258 | | o1const 13683 |
. . . . 5
                          |
259 | 248, 18, 258 | sylancr 669 |
. . . 4
 
                |
260 | | fveq1 5864 |
. . . . . . . . . . . 12
                 |
261 | 260 | oveq1d 6305 |
. . . . . . . . . . 11
           Λ            Λ      |
262 | 261 | sumeq2sdv 13770 |
. . . . . . . . . 10
                     Λ                      Λ      |
263 | 262, 179 | oveq12d 6308 |
. . . . . . . . 9
                      Λ                                        Λ             |
264 | 263 | adantl 468 |
. . . . . . . 8
                         Λ                                        Λ             |
265 | 46 | recnd 9669 |
. . . . . . . . . 10

      |
266 | 265 | mulid1d 9660 |
. . . . . . . . 9

            |
267 | 266 | oveq2d 6306 |
. . . . . . . 8

                   Λ                              Λ           |
268 | 264, 267 | sylan9eq 2505 |
. . . . . . 7
   

                      Λ                                        Λ           |
269 | 268 | mpteq2dva 4489 |
. . . . . 6
                          Λ                                          Λ            |
270 | 8, 24, 1, 3, 4, 66 | rpvmasumlem 24325 |
. . . . . . 7
                     Λ               |
271 | 270 | ad2antrr 732 |
. . . . . 6
                        Λ               |
272 | 269, 271 | eqeltrd 2529 |
. . . . 5
                          Λ                           |
273 | 183 | oveq2d 6306 |
. . . . . . . . . 10
                               |
274 | 273 | oveq2d 6306 |
. . . . . . . . 9
                      Λ                                          Λ                   |
275 | 48 | adantlr 721 |
. . . . . . . . . . . . . . 15
           |
276 | | mulcom 9625 |
. . . . . . . . . . . . . . 15
                        |
277 | 275, 51, 276 | sylancl 668 |
. . . . . . . . . . . . . 14
                     |
278 | 275 | mulm1d 10070 |
. . . . . . . . . . . . . 14
                   |
279 | 277, 278 | eqtrd 2485 |
. . . . . . . . . . . . 13
                   |
280 | 275 | mul01d 9832 |
. . . . . . . . . . . . 13
             |
281 | 279, 280 | ifeq12d 3901 |
. . . . . . . . . . . 12
                                   |
282 | | ovif2 6374 |
. . . . . . . . . . . 12
                               |
283 | | negeq 9867 |
. . . . . . . . . . . . 13
             
                 |
284 | | negeq 9867 |
. . . . . . . . . . . . . 14
                       |
285 | 284, 187 | syl6eq 2501 |
. . . . . . . . . . . . 13
                      |
286 | 283, 285 | ifsb 3894 |
. . . . . . . . . . . 12
                     |
287 | 281, 282,
286 | 3eqtr4g 2510 |
. . . . . . . . . . 11
                             |
288 | 287 | oveq2d 6306 |
. . . . . . . . . 10
                          Λ                  
                   Λ                 |
289 | 59 | an32s 813 |
. . . . . . . . . . 11
                         Λ      |
290 | | ifcl 3923 |
. . . . . . . . . . . 12
     
            |
291 | 275, 52, 290 | sylancl 668 |
. . . . . . . . . . 11
                |
292 | 289, 291 | subnegd 9993 |
. . . . . . . . . 10
                          Λ                                    Λ                |
293 | 288, 292 | eqtrd 2485 |
. . . . . . . . 9
                          Λ                  
                   Λ                |
294 | 274, 293 | sylan9eqr 2507 |
. . . . . . . 8
   


                     Λ                                          Λ                |
295 | 294 | an32s 813 |
. . . . . . 7
   

                      Λ                                          Λ                |
296 | 295 | mpteq2dva 4489 |
. . . . . 6
                          Λ                                            Λ                 |
297 | 1 | ad2antrr 732 |
. . . . . . . 8
      |
298 | | simplr 762 |
. . . . . . . 8
      |
299 | | simpr 463 |
. . . . . . . 8
     |
300 | | eqid 2451 |
. . . . . . . 8
                         |
301 | 8, 24, 297, 3, 4, 66, 298, 299, 300 | dchrmusumlema 24331 |
. . . . . . 7
      
 
                                                       |
302 | 1 | adantr 467 |
. . . . . . . . . . . . 13
 
   |
303 | 302 | ad2antrr 732 |
. . . . . . . . . . . 12
   

                                                           |
304 | 298 | adantr 467 |
. . . . . . . . . . . 12
   

                                                           |
305 | | simplr 762 |
. . . . . . . . . . . 12
   

                                                          |
306 | | simprl 764 |
. . . . . . . . . . . 12
   

                                                              |
307 | | simprrl 774 |
. . . . . . . . . . . 12
   

                                                                          |
308 | | simprrr 775 |
. . . . . . . . . . . 12
   

                                                                                              |
309 | 8, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308, 207 | dchrvmaeq0 24342 |
. . . . . . . . . . 11
   

                                                             |
310 | | ifbi 3902 |
. . . . . . . . . . . . 13
 
                     |
311 | 310 | oveq2d 6306 |
. . . . . . . . . . . 12
 
                      Λ                                   Λ                |
312 | 311 | mpteq2dv 4490 |
. . . . . . . . . . 11
 
                       Λ                                     Λ                 |
313 | 309, 312 | syl 17 |
. . . . . . . . . 10
   

                                                                               Λ                                     Λ                 |
314 | 8, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308 | dchrvmasumif 24341 |
. . . . . . . . . 10
   

                                                                               Λ                    |
315 | 313, 314 | eqeltrd 2529 |
. . . . . . . . 9
   

                                                                               Λ                    |
316 | 315 | rexlimdvaa 2880 |
. . . . . . . 8
     
 
   |