Step | Hyp | Ref
| Expression |
1 | | hoidmvlelem2.a |
. . . . . . 7
       |
2 | | hoidmvlelem2.z |
. . . . . . . . . 10
     |
3 | | snidg 3996 |
. . . . . . . . . 10
       |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
     |
5 | | elun2 3604 |
. . . . . . . . 9
         |
6 | 4, 5 | syl 17 |
. . . . . . . 8
       |
7 | | hoidmvlelem2.w |
. . . . . . . 8
     |
8 | 6, 7 | syl6eleqr 2542 |
. . . . . . 7
   |
9 | 1, 8 | ffvelrnd 6028 |
. . . . . 6
       |
10 | | hoidmvlelem2.b |
. . . . . . 7
       |
11 | 10, 8 | ffvelrnd 6028 |
. . . . . 6
       |
12 | | hoidmvlelem2.v |
. . . . . . . 8
         |
13 | 11 | snssd 4120 |
. . . . . . . . 9
         |
14 | | hoidmvlelem2.O |
. . . . . . . . . 10
                                     |
15 | | nfv 1763 |
. . . . . . . . . . 11
   |
16 | | eqid 2453 |
. . . . . . . . . . 11
                                                                         |
17 | | simpl 459 |
. . . . . . . . . . . 12
 
                             |
18 | | fz1ssnn 11837 |
. . . . . . . . . . . . . 14
     |
19 | | elrabi 3195 |
. . . . . . . . . . . . . 14
                                 |
20 | 18, 19 | sseldi 3432 |
. . . . . . . . . . . . 13
                             |
21 | 20 | adantl 468 |
. . . . . . . . . . . 12
 
                             |
22 | | eleq1 2519 |
. . . . . . . . . . . . . . 15
 
   |
23 | 22 | anbi2d 711 |
. . . . . . . . . . . . . 14
  

     |
24 | | fveq2 5870 |
. . . . . . . . . . . . . . . 16
           |
25 | 24 | fveq1d 5872 |
. . . . . . . . . . . . . . 15
                   |
26 | 25 | eleq1d 2515 |
. . . . . . . . . . . . . 14
         
           |
27 | 23, 26 | imbi12d 322 |
. . . . . . . . . . . . 13
   
           
             |
28 | | hoidmvlelem2.d |
. . . . . . . . . . . . . . . 16
         |
29 | 28 | ffvelrnda 6027 |
. . . . . . . . . . . . . . 15
 

        |
30 | | elmapi 7498 |
. . . . . . . . . . . . . . 15
                 |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
 

          |
32 | 8 | adantr 467 |
. . . . . . . . . . . . . 14
 

  |
33 | 31, 32 | ffvelrnd 6028 |
. . . . . . . . . . . . 13
 

          |
34 | 27, 33 | chvarv 2109 |
. . . . . . . . . . . 12
 

          |
35 | 17, 21, 34 | syl2anc 667 |
. . . . . . . . . . 11
 
                                     |
36 | 15, 16, 35 | rnmptssd 37483 |
. . . . . . . . . 10
                                       |
37 | 14, 36 | syl5eqss 3478 |
. . . . . . . . 9

  |
38 | 13, 37 | unssd 3612 |
. . . . . . . 8
           |
39 | 12, 38 | syl5eqss 3478 |
. . . . . . 7

  |
40 | | hoidmvlelem2.q |
. . . . . . . 8
inf    |
41 | | ltso 9719 |
. . . . . . . . . 10
 |
42 | 41 | a1i 11 |
. . . . . . . . 9
   |
43 | | snfi 7655 |
. . . . . . . . . . . 12
       |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
         |
45 | | fzfi 12192 |
. . . . . . . . . . . . . . 15
     |
46 | | rabfi 7801 |
. . . . . . . . . . . . . . 15
                                 |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . . . 14
                           |
48 | 47 | a1i 11 |
. . . . . . . . . . . . 13
                             |
49 | 16 | rnmptfi 37445 |
. . . . . . . . . . . . 13
                          
                                      |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
                                       |
51 | 14, 50 | syl5eqel 2535 |
. . . . . . . . . . 11
   |
52 | | unfi 7843 |
. . . . . . . . . . 11
                   |
53 | 44, 51, 52 | syl2anc 667 |
. . . . . . . . . 10
           |
54 | 12, 53 | syl5eqel 2535 |
. . . . . . . . 9
   |
55 | | fvex 5880 |
. . . . . . . . . . . . . 14
     |
56 | 55 | snid 3998 |
. . . . . . . . . . . . 13
           |
57 | | elun1 3603 |
. . . . . . . . . . . . 13
                         |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . 12
             |
59 | 12 | eqcomi 2462 |
. . . . . . . . . . . 12
         |
60 | 58, 59 | eleqtri 2529 |
. . . . . . . . . . 11
     |
61 | 60 | a1i 11 |
. . . . . . . . . 10
       |
62 | | ne0i 3739 |
. . . . . . . . . 10
       |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
   |
64 | | fiinfcl 8022 |
. . . . . . . . 9
 
  inf     |
65 | 42, 54, 63, 39, 64 | syl13anc 1271 |
. . . . . . . 8
 inf     |
66 | 40, 65 | syl5eqel 2535 |
. . . . . . 7
   |
67 | 39, 66 | sseldd 3435 |
. . . . . 6
   |
68 | | hoidmvlelem2.u |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)                 Σ^                               |
69 | | ssrab2 3516 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)                 Σ^                                    ![[,] [,]](_icc.gif)       |
70 | 68, 69 | eqsstri 3464 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)       |
71 | 70 | a1i 11 |
. . . . . . . . . 10

      ![[,] [,]](_icc.gif)        |
72 | 9, 11 | iccssred 37612 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)     
  |
73 | 71, 72 | sstrd 3444 |
. . . . . . . . 9

  |
74 | | hoidmvlelem2.su |
. . . . . . . . 9
   |
75 | 73, 74 | sseldd 3435 |
. . . . . . . 8
   |
76 | 9 | rexrd 9695 |
. . . . . . . . 9
       |
77 | 11 | rexrd 9695 |
. . . . . . . . 9
       |
78 | 70, 74 | sseldi 3432 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)        |
79 | | iccgelb 11698 |
. . . . . . . . 9
                ![[,] [,]](_icc.gif)             |
80 | 76, 77, 78, 79 | syl3anc 1269 |
. . . . . . . 8
    
  |
81 | | hoidmvlelem2.sb |
. . . . . . . . . . . . . . 15
       |
82 | 81 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
      |
83 | | id 22 |
. . . . . . . . . . . . . . . 16
           |
84 | 83 | eqcomd 2459 |
. . . . . . . . . . . . . . 15
           |
85 | 84 | adantl 468 |
. . . . . . . . . . . . . 14
 
    
      |
86 | 82, 85 | breqtrd 4430 |
. . . . . . . . . . . . 13
 
    
  |
87 | 86 | adantlr 722 |
. . . . . . . . . . . 12
           |
88 | | simpll 761 |
. . . . . . . . . . . . 13
   
       |
89 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
90 | 89, 12 | syl6eleq 2541 |
. . . . . . . . . . . . . . . 16
           |
91 | 90 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
          |
92 | | elsni 3995 |
. . . . . . . . . . . . . . . . 17
             |
93 | 92 | con3i 141 |
. . . . . . . . . . . . . . . 16
    
        |
94 | 93 | adantl 468 |
. . . . . . . . . . . . . . 15
 
    
        |
95 | | elunnel1 3577 |
. . . . . . . . . . . . . . 15
         
         |
96 | 91, 94, 95 | syl2anc 667 |
. . . . . . . . . . . . . 14
 
    
  |
97 | 96 | adantll 721 |
. . . . . . . . . . . . 13
   
    
  |
98 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
99 | 98, 14 | syl6eleq 2541 |
. . . . . . . . . . . . . . . 16
                                       |
100 | | vex 3050 |
. . . . . . . . . . . . . . . . 17
 |
101 | 16 | elrnmpt 5084 |
. . . . . . . . . . . . . . . . 17
                                      
                                      |
102 | 100, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
                                     
                                     |
103 | 99, 102 | sylib 200 |
. . . . . . . . . . . . . . 15
                                       |
104 | 103 | adantl 468 |
. . . . . . . . . . . . . 14
 
                                       |
105 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
106 | 105 | fveq1d 5872 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
107 | 106 | eleq1d 2515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
           |
108 | 23, 107 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
           
             |
109 | | hoidmvlelem2.c |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
110 | 109 | ffvelrnda 6027 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

        |
111 | | elmapi 7498 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

          |
113 | 112, 32 | ffvelrnd 6028 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

          |
114 | 108, 113 | chvarv 2109 |
. . . . . . . . . . . . . . . . . . . . . 22
 

          |
115 | 114 | rexrd 9695 |
. . . . . . . . . . . . . . . . . . . . 21
 

          |
116 | 17, 21, 115 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
 
                                     |
117 | 34 | rexrd 9695 |
. . . . . . . . . . . . . . . . . . . . 21
 

          |
118 | 17, 21, 117 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
 
                                     |
119 | 106, 25 | oveq12d 6313 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                           |
120 | 119 | eleq2d 2516 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                   
                       |
121 | 120 | elrab 3198 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          
    
                       |
122 | 121 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . . 22
                               
                       |
123 | 122 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . 21
                                                 |
124 | 123 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
                                                 |
125 | | icoltub 37617 |
. . . . . . . . . . . . . . . . . . . 20
                                                 |
126 | 116, 118,
124, 125 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . . 19
 
                                     |
127 | 126 | 3adant3 1029 |
. . . . . . . . . . . . . . . . . 18
 
                         
                   |
128 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
                   |
129 | 128 | eqcomd 2459 |
. . . . . . . . . . . . . . . . . . 19
                   |
130 | 129 | 3ad2ant3 1032 |
. . . . . . . . . . . . . . . . . 18
 
                         
                   |
131 | 127, 130 | breqtrd 4430 |
. . . . . . . . . . . . . . . . 17
 
                         
           |
132 | 131 | 3exp 1208 |
. . . . . . . . . . . . . . . 16
                                         |
133 | 132 | adantr 467 |
. . . . . . . . . . . . . . 15
 
                                         |
134 | 133 | rexlimdv 2879 |
. . . . . . . . . . . . . 14
 
  
                                  
   |
135 | 104, 134 | mpd 15 |
. . . . . . . . . . . . 13
 
   |
136 | 88, 97, 135 | syl2anc 667 |
. . . . . . . . . . . 12
   
       |
137 | 87, 136 | pm2.61dan 801 |
. . . . . . . . . . 11
 
   |
138 | 137 | ralrimiva 2804 |
. . . . . . . . . 10
    |
139 | | breq2 4409 |
. . . . . . . . . . 11
 inf  
 inf  
   |
140 | 139 | rspcva 3150 |
. . . . . . . . . 10
 inf     inf  
  |
141 | 65, 138, 140 | syl2anc 667 |
. . . . . . . . 9

inf     |
142 | 40 | eqcomi 2462 |
. . . . . . . . . 10
inf    |
143 | 142 | a1i 11 |
. . . . . . . . 9
 inf     |
144 | 141, 143 | breqtrd 4430 |
. . . . . . . 8
   |
145 | 9, 75, 67, 80, 144 | lelttrd 9798 |
. . . . . . 7
    
  |
146 | 9, 67, 145 | ltled 9788 |
. . . . . 6
    
  |
147 | | fiminre 10562 |
. . . . . . . . 9
 



  |
148 | 39, 54, 63, 147 | syl3anc 1269 |
. . . . . . . 8
  
  |
149 | | lbinfle 10570 |
. . . . . . . 8
 


     inf         |
150 | 39, 148, 61, 149 | syl3anc 1269 |
. . . . . . 7
 inf         |
151 | 40, 150 | syl5eqbr 4439 |
. . . . . 6

      |
152 | 9, 11, 67, 146, 151 | eliccd 37611 |
. . . . 5
       ![[,] [,]](_icc.gif)        |
153 | 67 | recnd 9674 |
. . . . . . . . . 10
   |
154 | 75 | recnd 9674 |
. . . . . . . . . 10
   |
155 | 9 | recnd 9674 |
. . . . . . . . . 10
       |
156 | 153, 154,
155 | npncand 10015 |
. . . . . . . . 9
                   |
157 | 156 | eqcomd 2459 |
. . . . . . . 8
                   |
158 | 157 | oveq2d 6311 |
. . . . . . 7
  
                    |
159 | | rge0ssre 11747 |
. . . . . . . . . 10
    |
160 | | hoidmvlelem2.g |
. . . . . . . . . . 11
         
   |
161 | | hoidmvlelem2.l |
. . . . . . . . . . . 12
                                |
162 | | hoidmvlelem2.x |
. . . . . . . . . . . . 13
   |
163 | | hoidmvlelem2.y |
. . . . . . . . . . . . 13

  |
164 | 162, 163 | ssfid 37424 |
. . . . . . . . . . . 12
   |
165 | | ssun1 3599 |
. . . . . . . . . . . . . . 15

    |
166 | 165, 7 | sseqtr4i 3467 |
. . . . . . . . . . . . . 14
 |
167 | 166 | a1i 11 |
. . . . . . . . . . . . 13

  |
168 | 1, 167 | fssresd 5755 |
. . . . . . . . . . . 12
         |
169 | 10, 167 | fssresd 5755 |
. . . . . . . . . . . 12
         |
170 | 161, 164,
168, 169 | hoidmvcl 38414 |
. . . . . . . . . . 11
          
       |
171 | 160, 170 | syl5eqel 2535 |
. . . . . . . . . 10
      |
172 | 159, 171 | sseldi 3432 |
. . . . . . . . 9
   |
173 | 172 | recnd 9674 |
. . . . . . . 8
   |
174 | 153, 154 | subcld 9991 |
. . . . . . . 8
     |
175 | 154, 155 | subcld 9991 |
. . . . . . . 8
         |
176 | 173, 174,
175 | adddid 9672 |
. . . . . . 7
                   
         |
177 | 173, 174 | mulcld 9668 |
. . . . . . . 8
  
    |
178 | 173, 175 | mulcld 9668 |
. . . . . . . 8
  
        |
179 | 177, 178 | addcomd 9840 |
. . . . . . 7
   
                     
     |
180 | 158, 176,
179 | 3eqtrd 2491 |
. . . . . 6
  
                      |
181 | 67, 75 | jca 535 |
. . . . . . . . . . . . 13
     |
182 | | resubcl 9943 |
. . . . . . . . . . . . 13
 
     |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . 12
     |
184 | 172, 183 | jca 535 |
. . . . . . . . . . 11
       |
185 | | remulcl 9629 |
. . . . . . . . . . 11
  
   
    |
186 | 184, 185 | syl 17 |
. . . . . . . . . 10
  
    |
187 | 75, 9 | jca 535 |
. . . . . . . . . . . . 13
         |
188 | | resubcl 9943 |
. . . . . . . . . . . . 13
               |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . 12
         |
190 | 172, 189 | jca 535 |
. . . . . . . . . . 11
           |
191 | | remulcl 9629 |
. . . . . . . . . . 11
  
       
        |
192 | 190, 191 | syl 17 |
. . . . . . . . . 10
  
        |
193 | 186, 192 | jca 535 |
. . . . . . . . 9
   
   
         |
194 | | readdcl 9627 |
. . . . . . . . 9
   
  

         
             |
195 | 193, 194 | syl 17 |
. . . . . . . 8
   
             |
196 | 179, 195 | eqeltrrd 2532 |
. . . . . . 7
   
             |
197 | | 1red 9663 |
. . . . . . . . . 10
   |
198 | | hoidmvlelem2.e |
. . . . . . . . . . 11
   |
199 | 198 | rpred 11348 |
. . . . . . . . . 10
   |
200 | 197, 199 | readdcld 9675 |
. . . . . . . . 9
     |
201 | 2 | eldifbd 3419 |
. . . . . . . . . . 11
   |
202 | 8, 201 | eldifd 3417 |
. . . . . . . . . 10
     |
203 | | hoidmvlelem2.r |
. . . . . . . . . 10
 Σ^                      |
204 | | hoidmvlelem2.h |
. . . . . . . . . 10
                   
           |
205 | 161, 164,
202, 7, 109, 28, 203, 204, 75 | sge0hsphoire 38421 |
. . . . . . . . 9
 Σ^                              |
206 | 200, 205 | remulcld 9676 |
. . . . . . . 8
    Σ^                               |
207 | | fzfid 12193 |
. . . . . . . . . 10
       |
208 | 183 | adantr 467 |
. . . . . . . . . . 11
 
     
   |
209 | | simpl 459 |
. . . . . . . . . . . 12
 
       |
210 | | elfznn 11835 |
. . . . . . . . . . . . 13
       |
211 | 210 | adantl 468 |
. . . . . . . . . . . 12
 
       |
212 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
213 | | ovex 6323 |
. . . . . . . . . . . . . . . . 17
                 |
214 | 213 | a1i 11 |
. . . . . . . . . . . . . . . 16
                   |
215 | | hoidmvlelem2.p |
. . . . . . . . . . . . . . . . 17
                   |
216 | 215 | fvmpt2 5962 |
. . . . . . . . . . . . . . . 16
                                         |
217 | 212, 214,
216 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                       |
218 | 217 | adantl 468 |
. . . . . . . . . . . . . 14
 

                      |
219 | 164 | adantr 467 |
. . . . . . . . . . . . . . 15
 

  |
220 | 166 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
221 | 112, 220 | fssresd 5755 |
. . . . . . . . . . . . . . . . . . 19
 

            |
222 | 221 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                                     |
223 | | iftrue 3889 |
. . . . . . . . . . . . . . . . . . . 20
                      
                                     |
224 | 223 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
                          
                                     |
225 | 224 | feq1d 5719 |
. . . . . . . . . . . . . . . . . 18
                                                            
             |
226 | 222, 225 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
                          
                                   |
227 | | 0red 9649 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
228 | | hoidmvlelem2.f |
. . . . . . . . . . . . . . . . . . . 20
   |
229 | 227, 228 | fmptd 6051 |
. . . . . . . . . . . . . . . . . . 19
       |
230 | 229 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . 18
   
                           |
231 | | iffalse 3892 |
. . . . . . . . . . . . . . . . . . . 20
                      
                               |
232 | 231 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
   
                                                      |
233 | 232 | feq1d 5719 |
. . . . . . . . . . . . . . . . . 18
   
                                                                |
234 | 230, 233 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
   
                                                          |
235 | 226, 234 | pm2.61dan 801 |
. . . . . . . . . . . . . . . 16
 

                                     |
236 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
 

  |
237 | | fvex 5880 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
238 | 237 | resex 5151 |
. . . . . . . . . . . . . . . . . . . . 21
       |
239 | 238 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
         |
240 | 162, 163 | ssexd 4553 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
241 | | mptexg 6140 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
     |
243 | 228, 242 | syl5eqel 2535 |
. . . . . . . . . . . . . . . . . . . 20
   |
244 | 239, 243 | ifcld 3926 |
. . . . . . . . . . . . . . . . . . 19
                                  |
245 | 244 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 

                                 |
246 | | hoidmvlelem2.j |
. . . . . . . . . . . . . . . . . . 19
                                  |
247 | 246 | fvmpt2 5962 |
. . . . . . . . . . . . . . . . . 18
                                                                       |
248 | 236, 245,
247 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 

                                     |
249 | 248 | feq1d 5719 |
. . . . . . . . . . . . . . . 16
 

        
 
                                    |
250 | 235, 249 | mpbird 236 |
. . . . . . . . . . . . . . 15
 

          |
251 | 31, 220 | fssresd 5755 |
. . . . . . . . . . . . . . . . . . 19
 

            |
252 | 251 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                                     |
253 | | iftrue 3889 |
. . . . . . . . . . . . . . . . . . . 20
                      
                                     |
254 | 253 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
                          
                                     |
255 | 254 | feq1d 5719 |
. . . . . . . . . . . . . . . . . 18
                                                            
             |
256 | 252, 255 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
                          
                                   |
257 | | iffalse 3892 |
. . . . . . . . . . . . . . . . . . . 20
                      
                               |
258 | 257 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
   
                                                      |
259 | 258 | feq1d 5719 |
. . . . . . . . . . . . . . . . . 18
   
                                                                |
260 | 230, 259 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
   
                                                          |
261 | 256, 260 | pm2.61dan 801 |
. . . . . . . . . . . . . . . 16
 

                                     |
262 | | fvex 5880 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
263 | 262 | resex 5151 |
. . . . . . . . . . . . . . . . . . . . 21
       |
264 | 263 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
         |
265 | 264, 243 | ifcld 3926 |
. . . . . . . . . . . . . . . . . . 19
                                  |
266 | 265 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 

                                 |
267 | | hoidmvlelem2.k |
. . . . . . . . . . . . . . . . . . 19
                                  |
268 | 267 | fvmpt2 5962 |
. . . . . . . . . . . . . . . . . 18
                                                                       |
269 | 236, 266,
268 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 

                                     |
270 | 269 | feq1d 5719 |
. . . . . . . . . . . . . . . 16
 

        
 
                                    |
271 | 261, 270 | mpbird 236 |
. . . . . . . . . . . . . . 15
 

          |
272 | 161, 219,
250, 271 | hoidmvcl 38414 |
. . . . . . . . . . . . . 14
 

                     |
273 | 218, 272 | eqeltrd 2531 |
. . . . . . . . . . . . 13
 

         |
274 | 159, 273 | sseldi 3432 |
. . . . . . . . . . . 12
 

      |
275 | 209, 211,
274 | syl2anc 667 |
. . . . . . . . . . 11
 
           |
276 | 208, 275 | remulcld 9676 |
. . . . . . . . . 10
 
               |
277 | 207, 276 | fsumrecl 13812 |
. . . . . . . . 9
                 |
278 | 200, 277 | remulcld 9676 |
. . . . . . . 8
    
                |
279 | 206, 278 | readdcld 9675 |
. . . . . . 7
     Σ^                                
                 |
280 | 161, 164,
202, 7, 109, 28, 203, 204, 67 | sge0hsphoire 38421 |
. . . . . . . 8
 Σ^                              |
281 | 200, 280 | remulcld 9676 |
. . . . . . 7
    Σ^                               |
282 | 74, 68 | syl6eleq 2541 |
. . . . . . . . . 10
        ![[,] [,]](_icc.gif)                 Σ^                                |
283 | | oveq1 6302 |
. . . . . . . . . . . . 13
               |
284 | 283 | oveq2d 6311 |
. . . . . . . . . . . 12
 
        
        |
285 | | fveq2 5870 |
. . . . . . . . . . . . . . . . 17
           |
286 | 285 | fveq1d 5872 |
. . . . . . . . . . . . . . . 16
                           |
287 | 286 | oveq2d 6311 |
. . . . . . . . . . . . . . 15
                                                   |
288 | 287 | mpteq2dv 4493 |
. . . . . . . . . . . . . 14
                                                       |
289 | 288 | fveq2d 5874 |
. . . . . . . . . . . . 13
 Σ^                            Σ^                              |
290 | 289 | oveq2d 6311 |
. . . . . . . . . . . 12
    Σ^                                Σ^                               |
291 | 284, 290 | breq12d 4418 |
. . . . . . . . . . 11
         
   Σ^                            
           Σ^                                |
292 | 291 | elrab 3198 |
. . . . . . . . . 10
        ![[,] [,]](_icc.gif)                 Σ^                                     ![[,] [,]](_icc.gif)       
         Σ^                                |
293 | 282, 292 | sylib 200 |
. . . . . . . . 9
        ![[,] [,]](_icc.gif)       
         Σ^                                |
294 | 293 | simprd 465 |
. . . . . . . 8
  
         Σ^                               |
295 | 207, 275 | fsumrecl 13812 |
. . . . . . . . . . 11
             |
296 | 200, 295 | remulcld 9676 |
. . . . . . . . . 10
    
            |
297 | | 0red 9649 |
. . . . . . . . . . 11
   |
298 | 75, 67 | posdifd 10207 |
. . . . . . . . . . . 12
       |
299 | 144, 298 | mpbid 214 |
. . . . . . . . . . 11
     |
300 | 297, 183,
299 | ltled 9788 |
. . . . . . . . . 10

    |
301 | | hoidmvlelem2.le |
. . . . . . . . . 10

                |
302 | 172, 296,
183, 300, 301 | lemul1ad 10553 |
. . . . . . . . 9
  
 
                    |
303 | 200 | recnd 9674 |
. . . . . . . . . . 11
     |
304 | 295 | recnd 9674 |
. . . . . . . . . . 11
             |
305 | 303, 304,
174 | mulassd 9671 |
. . . . . . . . . 10
                
                
     |
306 | 275 | recnd 9674 |
. . . . . . . . . . . . 13
 
           |
307 | 207, 174,
306 | fsummulc1 13858 |
. . . . . . . . . . . 12
                          
    |
308 | 174 | adantr 467 |
. . . . . . . . . . . . . 14
 
     
   |
309 | 306, 308 | mulcomd 9669 |
. . . . . . . . . . . . 13
 
                       |
310 | 309 | sumeq2dv 13781 |
. . . . . . . . . . . 12
            
                  |
311 | 307, 310 | eqtrd 2487 |
. . . . . . . . . . 11
                               |
312 | 311 | oveq2d 6311 |
. . . . . . . . . 10
                                       |
313 | 305, 312 | eqtrd 2487 |
. . . . . . . . 9
                
                      |
314 | 302, 313 | breqtrd 4430 |
. . . . . . . 8
  
 
                    |
315 | 192, 186,
206, 278, 294, 314 | leadd12dd 37548 |
. . . . . . 7
   
          
    Σ^                                
                 |
316 | | hoidmvlelem2.m |
. . . . . . . . . . . . . . . . 17
   |
317 | | nnsplit 37591 |
. . . . . . . . . . . . . . . . 17
               |
318 | 316, 317 | syl 17 |
. . . . . . . . . . . . . . . 16
         
     |
319 | | uncom 3580 |
. . . . . . . . . . . . . . . . 17
        
                |
320 | 319 | a1i 11 |
. . . . . . . . . . . . . . . 16
                 
         |
321 | 318, 320 | eqtr2d 2488 |
. . . . . . . . . . . . . . 15
     
         |
322 | 321 | eqcomd 2459 |
. . . . . . . . . . . . . 14
               |
323 | 322 | mpteq1d 4487 |
. . . . . . . . . . . . 13
                                
                                  |
324 | 323 | fveq2d 5874 |
. . . . . . . . . . . 12
 Σ^                            Σ^                                          |
325 | | nfv 1763 |
. . . . . . . . . . . . 13
   |
326 | | fvex 5880 |
. . . . . . . . . . . . . 14
   
   |
327 | 326 | a1i 11 |
. . . . . . . . . . . . 13
         |
328 | | ovex 6323 |
. . . . . . . . . . . . . 14
     |
329 | 328 | a1i 11 |
. . . . . . . . . . . . 13
       |
330 | | incom 3627 |
. . . . . . . . . . . . . . 15
                
   
    |
331 | | nnuzdisj 37588 |
. . . . . . . . . . . . . . 15
        
    |
332 | 330, 331 | eqtri 2475 |
. . . . . . . . . . . . . 14
             |
333 | 332 | a1i 11 |
. . . . . . . . . . . . 13
     
         |
334 | | icossicc 11728 |
. . . . . . . . . . . . . 14
       |
335 | | ssid 3453 |
. . . . . . . . . . . . . . 15
       |
336 | | simpl 459 |
. . . . . . . . . . . . . . . 16
 
      
  |
337 | 316 | peano2nnd 10633 |
. . . . . . . . . . . . . . . . . . 19
     |
338 | | uznnssnn 11213 |
. . . . . . . . . . . . . . . . . . 19
           |
339 | 337, 338 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
340 | 339 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
      
   
    |
341 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
      
        |
342 | 340, 341 | sseldd 3435 |
. . . . . . . . . . . . . . . 16
 
      
  |
343 | | snfi 7655 |
. . . . . . . . . . . . . . . . . . . . 21
 
 |
344 | 343 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
     |
345 | | unfi 7843 |
. . . . . . . . . . . . . . . . . . . 20
           |
346 | 164, 344,
345 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
       |
347 | 7, 346 | syl5eqel 2535 |
. . . . . . . . . . . . . . . . . 18
   |
348 | 347 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 

  |
349 | | eleq1 2519 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
350 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
351 | 350 | breq1d 4415 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       |
352 | 351, 350 | ifbieq1d 3906 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
         |
353 | 349, 350,
352 | ifbieq12d 3910 |
. . . . . . . . . . . . . . . . . . . . . 22
                                               |
354 | 353 | cbvmptv 4498 |
. . . . . . . . . . . . . . . . . . . . 21
              
                                  |
355 | 354 | mpteq2i 4489 |
. . . . . . . . . . . . . . . . . . . 20
                 
                            
          |
356 | 355 | mpteq2i 4489 |
. . . . . . . . . . . . . . . . . . 19
                  
                                          |
357 | 204, 356 | eqtri 2475 |
. . . . . . . . . . . . . . . . . 18
                   
           |
358 | 75 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 

  |
359 | 357, 358,
348, 31 | hsphoif 38408 |
. . . . . . . . . . . . . . . . 17
 

                  |
360 | 161, 348,
112, 359 | hoidmvcl 38414 |
. . . . . . . . . . . . . . . 16
 

                             |
361 | 336, 342,
360 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
      
                             |
362 | 335, 361 | sseldi 3432 |
. . . . . . . . . . . . . 14
 
      
                             |
363 | 334, 362 | sseldi 3432 |
. . . . . . . . . . . . 13
 
      
                             |
364 | 209, 211,
360 | syl2anc 667 |
. . . . . . . . . . . . . 14
 
                                  |
365 | 334, 364 | sseldi 3432 |
. . . . . . . . . . . . 13
 
                                  |
366 | 325, 327,
329, 333, 363, 365 | sge0splitmpt 38263 |
. . . . . . . . . . . 12
 Σ^                                         Σ^                                     Σ^                                   |
367 | | nnex 10622 |
. . . . . . . . . . . . . . 15
 |
368 | 367 | a1i 11 |
. . . . . . . . . . . . . 14
   |
369 | 334, 360 | sseldi 3432 |
. . . . . . . . . . . . . 14
 

                             |
370 | 325, 368,
369, 205, 339 | sge0ssrempt 38257 |
. . . . . . . . . . . . 13
 Σ^                                    |
371 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
    
  |
372 | 325, 368,
369, 205, 371 | sge0ssrempt 38257 |
. . . . . . . . . . . . 13
 Σ^                                  |
373 | | rexadd 11532 |
. . . . . . . . . . . . 13
  Σ^                                  Σ^                                  Σ^                                     Σ^                                  Σ^                                  Σ^                                   |
374 | 370, 372,
373 | syl2anc 667 |
. . . . . . . . . . . 12
  Σ^                                     Σ^                                  Σ^                                  Σ^                                   |
375 | 324, 366,
374 | 3eqtrd 2491 |
. . . . . . . . . . 11
 Σ^                             Σ^                                  Σ^                                   |
376 | 375 | oveq2d 6311 |
. . . . . . . . . 10
    Σ^                                 Σ^                                  Σ^                                    |
377 | 376 | oveq1d 6310 |
. . . . . . . . 9
     Σ^                                
                    Σ^                                  Σ^                                                       |
378 | 375, 205 | eqeltrrd 2532 |
. . . . . . . . . . . 12
  Σ^                                  Σ^                                   |
379 | 378 | recnd 9674 |
. . . . . . . . . . 11
  Σ^                                  Σ^                                   |
380 | 277 | recnd 9674 |
. . . . . . . . . . 11
                 |
381 | 303, 379,
380 | adddid 9672 |
. . . . . . . . . 10
      Σ^                                  Σ^                                                      Σ^                                  Σ^                                                       |
382 | 381 | eqcomd 2459 |
. . . . . . . . 9
      Σ^                                  Σ^                                                          Σ^                                  Σ^                                                   |
383 | 370 | recnd 9674 |
. . . . . . . . . . . 12
 Σ^                                    |
384 | 372 | recnd 9674 |
. . . . . . . . . . . 12
 Σ^                                  |
385 | 383, 384,
380 | addassd 9670 |
. . . . . . . . . . 11
   Σ^                                  Σ^                                                 Σ^                                   Σ^                                
                 |
386 | 207, 364 | sge0fsummpt 38242 |
. . . . . . . . . . . . . 14
 Σ^                                
                               |
387 | 386 | oveq1d 6310 |
. . . . . . . . . . . . 13
  Σ^                                
               
                                              |
388 | | ax-resscn 9601 |
. . . . . . . . . . . . . . . . . 18
 |
389 | 159, 388 | sstri 3443 |
. . . . . . . . . . . . . . . . 17
    |
390 | 389, 360 | sseldi 3432 |
. . . . . . . . . . . . . . . 16
 

                          |
391 | 209, 211,
390 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
                               |
392 | 183 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 

    |
393 | 392, 274 | remulcld 9676 |
. . . . . . . . . . . . . . . . 17
 

          |
394 | 393 | recnd 9674 |
. . . . . . . . . . . . . . . 16
 

          |
395 | 211, 394 | syldan 473 |
. . . . . . . . . . . . . . 15
 
               |
396 | 207, 391,
395 | fsumadd 13817 |
. . . . . . . . . . . . . 14
                                          
                                              |
397 | 396 | eqcomd 2459 |
. . . . . . . . . . . . 13
                                               
                                         |
398 | 387, 397 | eqtrd 2487 |
. . . . . . . . . . . 12
  Σ^                  ![]() |