Step | Hyp | Ref
| Expression |
1 | | iunin2 4342 |
. . . . 5
       |
2 | 1 | fveq2i 5868 |
. . . 4
    
          |
3 | | iccssxr 11717 |
. . . . 5
    |
4 | | carsgval.2 |
. . . . . 6
           |
5 | | nnex 10615 |
. . . . . . . 8
 |
6 | 5 | a1i 11 |
. . . . . . 7
   |
7 | | carsgclctunlem2.3 |
. . . . . . . . 9
    |
8 | 7 | adantr 467 |
. . . . . . . 8
 

   |
9 | 8 | elpwincl1 28154 |
. . . . . . 7
 

     |
10 | 6, 9 | elpwiuncl 28156 |
. . . . . 6
  
    |
11 | 4, 10 | ffvelrnd 6023 |
. . . . 5
             |
12 | 3, 11 | sseldi 3430 |
. . . 4
          |
13 | 2, 12 | syl5eqelr 2534 |
. . 3
          |
14 | 4, 7 | ffvelrnd 6023 |
. . . . 5
          |
15 | 3, 14 | sseldi 3430 |
. . . 4
       |
16 | 7 | elpwdifcl 28155 |
. . . . . . 7
  
    |
17 | 4, 16 | ffvelrnd 6023 |
. . . . . 6
             |
18 | 3, 17 | sseldi 3430 |
. . . . 5
          |
19 | 18 | xnegcld 11586 |
. . . 4
       
    |
20 | 15, 19 | xaddcld 11587 |
. . 3
             
      |
21 | 4 | adantr 467 |
. . . . . . . . 9
 

          |
22 | 21, 9 | ffvelrnd 6023 |
. . . . . . . 8
 

           |
23 | 22 | ralrimiva 2802 |
. . . . . . 7
             |
24 | | nfcv 2592 |
. . . . . . . 8
   |
25 | 24 | esumcl 28851 |
. . . . . . 7
            
Σ*             |
26 | 6, 23, 25 | syl2anc 667 |
. . . . . 6
 Σ*             |
27 | 3, 26 | sseldi 3430 |
. . . . 5
 Σ*          |
28 | 9 | ralrimiva 2802 |
. . . . . . . . 9
  
    |
29 | | dfiun3g 5087 |
. . . . . . . . 9
 
        
    |
30 | 28, 29 | syl 17 |
. . . . . . . 8
  
        |
31 | 30 | fveq2d 5869 |
. . . . . . 7
             
     |
32 | | nnct 28294 |
. . . . . . . . . 10
 |
33 | | mptct 28302 |
. . . . . . . . . 10

      |
34 | | rnct 28300 |
. . . . . . . . . 10
    
      |
35 | 32, 33, 34 | mp2b 10 |
. . . . . . . . 9
     |
36 | 35 | a1i 11 |
. . . . . . . 8
       |
37 | | eqid 2451 |
. . . . . . . . . 10
         |
38 | 37 | rnmptss 6052 |
. . . . . . . . 9
 
    
 
   |
39 | 28, 38 | syl 17 |
. . . . . . . 8
        |
40 | | mptexg 6135 |
. . . . . . . . . 10
       |
41 | | rnexg 6725 |
. . . . . . . . . 10
      
    |
42 | 5, 40, 41 | mp2b 10 |
. . . . . . . . 9
     |
43 | | breq1 4405 |
. . . . . . . . . . . 12
       
     |
44 | | sseq1 3453 |
. . . . . . . . . . . 12
      
        |
45 | 43, 44 | 3anbi23d 1342 |
. . . . . . . . . . 11
      
 
      
 
     |
46 | | unieq 4206 |
. . . . . . . . . . . . 13
        
    |
47 | 46 | fveq2d 5869 |
. . . . . . . . . . . 12
               
     |
48 | | esumeq1 28855 |
. . . . . . . . . . . 12
     Σ*      Σ*            |
49 | 47, 48 | breq12d 4415 |
. . . . . . . . . . 11
           Σ*           
  
Σ*  
          |
50 | 45, 49 | imbi12d 322 |
. . . . . . . . . 10
       
      
Σ*      
         
 
        
Σ*  
           |
51 | | carsgsiga.2 |
. . . . . . . . . 10
 
      
Σ*        |
52 | 50, 51 | vtoclg 3107 |
. . . . . . . . 9
  
     
 
   
 
        
Σ*  
          |
53 | 42, 52 | ax-mp 5 |
. . . . . . . 8
 
       
 
        
Σ*  
         |
54 | 36, 39, 53 | mpd3an23 1366 |
. . . . . . 7
      
  
Σ*  
         |
55 | 31, 54 | eqbrtrd 4423 |
. . . . . 6
       
Σ*  
         |
56 | | fveq2 5865 |
. . . . . . 7
  
            |
57 | | simpr 463 |
. . . . . . . . 9
      
    |
58 | 57 | fveq2d 5869 |
. . . . . . . 8
      
            |
59 | | carsgsiga.1 |
. . . . . . . . 9
       |
60 | 59 | ad2antrr 732 |
. . . . . . . 8
      
      |
61 | 58, 60 | eqtrd 2485 |
. . . . . . 7
      
        |
62 | | carsgclctunlem2.1 |
. . . . . . . . 9
 Disj
  |
63 | | disjin 28196 |
. . . . . . . . 9
Disj Disj     |
64 | 62, 63 | syl 17 |
. . . . . . . 8
 Disj
    |
65 | | incom 3625 |
. . . . . . . . . 10
     |
66 | 65 | rgenw 2749 |
. . . . . . . . 9
      |
67 | | disjeq2 4377 |
. . . . . . . . 9
 
   
Disj   Disj      |
68 | 66, 67 | ax-mp 5 |
. . . . . . . 8
Disj   Disj     |
69 | 64, 68 | sylib 200 |
. . . . . . 7
 Disj
    |
70 | 56, 6, 22, 9, 61, 69 | esumrnmpt2 28889 |
. . . . . 6
 Σ*         
Σ*          |
71 | 55, 70 | breqtrd 4427 |
. . . . 5
       
Σ*          |
72 | | carsgval.1 |
. . . . . . . 8
   |
73 | | difssd 3561 |
. . . . . . . 8
  

  |
74 | | carsgsiga.3 |
. . . . . . . 8
 
            |
75 | 72, 4, 73, 7, 74 | carsgmon 29146 |
. . . . . . 7
              |
76 | 14, 17, 75 | xrge0subcld 28345 |
. . . . . 6
             
         |
77 | 4 | adantr 467 |
. . . . . . . . . . . 12
 

          |
78 | 7 | adantr 467 |
. . . . . . . . . . . . 13
 

   |
79 | 78 | elpwincl1 28154 |
. . . . . . . . . . . 12
 

           |
80 | 77, 79 | ffvelrnd 6023 |
. . . . . . . . . . 11
 

                 |
81 | 3, 80 | sseldi 3430 |
. . . . . . . . . 10
 

              |
82 | | xrge0neqmnf 11737 |
. . . . . . . . . . 11
                   
          |
83 | 80, 82 | syl 17 |
. . . . . . . . . 10
 

              |
84 | 78 | elpwdifcl 28155 |
. . . . . . . . . . . 12
 

           |
85 | 77, 84 | ffvelrnd 6023 |
. . . . . . . . . . 11
 

    
            |
86 | 3, 85 | sseldi 3430 |
. . . . . . . . . 10
 

    
         |
87 | | xrge0neqmnf 11737 |
. . . . . . . . . . 11
                   
          |
88 | 85, 87 | syl 17 |
. . . . . . . . . 10
 

    
         |
89 | 86 | xnegcld 11586 |
. . . . . . . . . 10
 

                |
90 | | xnegneg 11507 |
. . . . . . . . . . . . . . . . 17
                               
          |
91 | 86, 90 | syl 17 |
. . . . . . . . . . . . . . . 16
 

      
           
          |
92 | 91 | adantr 467 |
. . . . . . . . . . . . . . 15
                                                |
93 | | xnegeq 11500 |
. . . . . . . . . . . . . . . . 17
     
              
           |
94 | 93 | adantl 468 |
. . . . . . . . . . . . . . . 16
                                     |
95 | | xnegmnf 11503 |
. . . . . . . . . . . . . . . 16

 |
96 | 94, 95 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
                                    |
97 | 92, 96 | eqtr3d 2487 |
. . . . . . . . . . . . . 14
                                 |
98 | 97 | oveq2d 6306 |
. . . . . . . . . . . . 13
                       
               
            
             |
99 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . 21
           |
100 | | fz1ssnn 11830 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 

      |
102 | 101 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . . 21
           |
103 | | carsgclctunlem2.2 |
. . . . . . . . . . . . . . . . . . . . 21
 

toCaraSiga    |
104 | 99, 102, 103 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
         toCaraSiga    |
105 | 104 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . . 19
 

      toCaraSiga    |
106 | | dfiun3g 5087 |
. . . . . . . . . . . . . . . . . . 19
 
     toCaraSiga  
              |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 

               |
108 | 72 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 

  |
109 | 59 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 

      |
110 | 51 | 3adant1r 1261 |
. . . . . . . . . . . . . . . . . . 19
           Σ*        |
111 | | fzfi 12185 |
. . . . . . . . . . . . . . . . . . . . 21
     |
112 | | mptfi 7873 |
. . . . . . . . . . . . . . . . . . . . 21
             |
113 | | rnfi 7857 |
. . . . . . . . . . . . . . . . . . . . 21
               |
114 | 111, 112,
113 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
       |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 

        |
116 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . 21
             |
117 | 116 | rnmptss 6052 |
. . . . . . . . . . . . . . . . . . . 20
 
     toCaraSiga        toCaraSiga    |
118 | 105, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 

     
toCaraSiga    |
119 | 108, 77, 109, 110, 115, 118 | fiunelcarsg 29148 |
. . . . . . . . . . . . . . . . . 18
 

       toCaraSiga    |
120 | 107, 119 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . 17
 

      toCaraSiga    |
121 | 108, 77 | elcarsg 29137 |
. . . . . . . . . . . . . . . . 17
 

 
     toCaraSiga 
 
     
      
             
                 |
122 | 120, 121 | mpbid 214 |
. . . . . . . . . . . . . . . 16
 

 
     
      
             
                |
123 | 122 | simprd 465 |
. . . . . . . . . . . . . . 15
 

                      
              |
124 | | ineq1 3627 |
. . . . . . . . . . . . . . . . . . 19
 
        
        |
125 | 124 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
                           |
126 | | difeq1 3544 |
. . . . . . . . . . . . . . . . . . 19
 
        
        |
127 | 126 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
                           |
128 | 125, 127 | oveq12d 6308 |
. . . . . . . . . . . . . . . . 17
     
               
            
               
          |
129 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
130 | 128, 129 | eqeq12d 2466 |
. . . . . . . . . . . . . . . 16
       
             
            
                   
                |
131 | 130 | rspcv 3146 |
. . . . . . . . . . . . . . 15
                         
           
                   
                |
132 | 78, 123, 131 | sylc 62 |
. . . . . . . . . . . . . 14
 

                   
               |
133 | 132 | adantr 467 |
. . . . . . . . . . . . 13
                       
               
              |
134 | | xaddpnf1 11519 |
. . . . . . . . . . . . . . 15
             
    
                       
  |
135 | 81, 83, 134 | syl2anc 667 |
. . . . . . . . . . . . . 14
 

                  |
136 | 135 | adantr 467 |
. . . . . . . . . . . . 13
                       
             |
137 | 98, 133, 136 | 3eqtr3d 2493 |
. . . . . . . . . . . 12
                         |
138 | | carsgclctunlem2.4 |
. . . . . . . . . . . . . 14
       |
139 | 138 | ad2antrr 732 |
. . . . . . . . . . . . 13
                         |
140 | 139 | neneqd 2629 |
. . . . . . . . . . . 12
                         |
141 | 137, 140 | pm2.65da 580 |
. . . . . . . . . . 11
 

                |
142 | 141 | neqned 2631 |
. . . . . . . . . 10
 

                |
143 | | xaddass 11535 |
. . . . . . . . . 10
      
       
            
            
            
     
       
                                    
                
                              
              
            |
144 | 81, 83, 86, 88, 89, 142, 143 | syl222anc 1284 |
. . . . . . . . 9
 

                    
                
                              
              
            |
145 | | xnegid 11529 |
. . . . . . . . . . 11
                  
              
           |
146 | 86, 145 | syl 17 |
. . . . . . . . . 10
 

                                |
147 | 146 | oveq2d 6306 |
. . . . . . . . 9
 

                     
              
                             |
148 | | xaddid1 11532 |
. . . . . . . . . 10
                                            |
149 | 81, 148 | syl 17 |
. . . . . . . . 9
 

                               |
150 | 144, 147,
149 | 3eqtrd 2489 |
. . . . . . . 8
 

                    
                
                       |
151 | 132 | oveq1d 6305 |
. . . . . . . 8
 

                    
                
                                 |
152 | 107 | ineq2d 3634 |
. . . . . . . . . 10
 

                   |
153 | 152 | fveq2d 5869 |
. . . . . . . . 9
 

                           |
154 | | fmptss 28277 |
. . . . . . . . . . . . 13
    
          |
155 | | rnss 5063 |
. . . . . . . . . . . . 13
      
            |
156 | 100, 154,
155 | mp2b 10 |
. . . . . . . . . . . 12
     
   |
157 | 156 | a1i 11 |
. . . . . . . . . . 11
 

     
    |
158 | | disjrnmpt 28195 |
. . . . . . . . . . . . 13
Disj Disj      |
159 | 62, 158 | syl 17 |
. . . . . . . . . . . 12
 Disj
     |
160 | 159 | adantr 467 |
. . . . . . . . . . 11
 

Disj
     |
161 | | disjss1 4379 |
. . . . . . . . . . 11
         Disj   
Disj           |
162 | 157, 160,
161 | sylc 62 |
. . . . . . . . . 10
 

Disj
         |
163 | 108, 77, 109, 110, 115, 118, 162, 78 | carsgclctunlem1 29149 |
. . . . . . . . 9
 

            
Σ*                |
164 | | ineq2 3628 |
. . . . . . . . . . 11
       |
165 | 164 | fveq2d 5869 |
. . . . . . . . . 10
               |
166 | 111 | elexi 3055 |
. . . . . . . . . . 11
     |
167 | 166 | a1i 11 |
. . . . . . . . . 10
 

      |
168 | 99, 102, 22 | syl2anc 667 |
. . . . . . . . . 10
                    |
169 | | inss2 3653 |
. . . . . . . . . . . . . . 15
   |
170 | | sseq2 3454 |
. . . . . . . . . . . . . . 15

  
     |
171 | 169, 170 | mpbii 215 |
. . . . . . . . . . . . . 14

    |
172 | | ss0 3765 |
. . . . . . . . . . . . . 14
  
    |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . 13

    |
174 | 173 | adantl 468 |
. . . . . . . . . . . 12
   

          |
175 | 174 | fveq2d 5869 |
. . . . . . . . . . 11
   

         
        |
176 | 109 | ad2antrr 732 |
. . . . . . . . . . 11
   

            |
177 | 175, 176 | eqtrd 2485 |
. . . . . . . . . 10
   

         
    |
178 | 62 | adantr 467 |
. . . . . . . . . . 11
 

Disj
  |
179 | | disjss1 4379 |
. . . . . . . . . . 11
    
Disj Disj         |
180 | 101, 178,
179 | sylc 62 |
. . . . . . . . . 10
 

Disj
       |
181 | 165, 167,
168, 104, 177, 180 | esumrnmpt2 28889 |
. . . . . . . . 9
 

Σ*              Σ*              |
182 | 153, 163,
181 | 3eqtrd 2489 |
. . . . . . . 8
 

            Σ*         
    |
183 | 150, 151,
182 | 3eqtr3rd 2494 |
. . . . . . 7
 

Σ*                                    |
184 | 17 | adantr 467 |
. . . . . . . . . 10
 

    
       |
185 | 3, 184 | sseldi 3430 |
. . . . . . . . 9
 

    
    |
186 | 185 | xnegcld 11586 |
. . . . . . . 8
 

           |
187 | 15 | adantr 467 |
. . . . . . . 8
 

      |
188 | | iunss1 4290 |
. . . . . . . . . . . 12
    
         |
189 | 100, 188 | mp1i 13 |
. . . . . . . . . . 11
 

         |
190 | 189 | sscond 3570 |
. . . . . . . . . 10
 

             |
191 | 74 | 3adant1r 1261 |
. . . . . . . . . 10
         
      |
192 | 108, 77, 190, 84, 191 | carsgmon 29146 |
. . . . . . . . 9
 

    
                |
193 | | xleneg 11511 |
. . . . . . . . . 10
        
                        
              
                   |
194 | 193 | biimpa 487 |
. . . . . . . . 9
      
  
                                
                   
     |
195 | 185, 86, 192, 194 | syl21anc 1267 |
. . . . . . . 8
 

                    
    |
196 | | xleadd2a 11540 |
. . . . . . . 8
               
        
                        
   
      
                                  |
197 | 89, 186, 187, 195, 196 | syl31anc 1271 |
. . . . . . 7
 

                     
      
            |
198 | 183, 197 | eqbrtrd 4423 |
. . . . . 6
 

Σ*                               |
199 | 76, 22, 198 | esumgect 28911 |
. . . . 5
 Σ*                    
      |
200 | 12, 27, 20, 71, 199 | xrletrd 11459 |
. . . 4
                    
      |
201 | 2, 200 | syl5eqbrr 4437 |
. . 3
                    
      |
202 | | xleadd1a 11539 |
. . 3
      
  
            
                               
                   
   
             
                 |
203 | 13, 20, 18, 201, 202 | syl31anc 1271 |
. 2
     
          
                                  |
204 | | xrge0npcan 28457 |
. . 3
                      
                                 
         |
205 | 14, 17, 75, 204 | syl3anc 1268 |
. 2
                          
         |
206 | 203, 205 | breqtrd 4427 |
1
     
          
         |