Step | Hyp | Ref
| Expression |
1 | | hoidmvlelem1.s |
. . . . . 6
   
 |
2 | 1 | a1i 11 |
. . . . 5
   
   |
3 | | hoidmvlelem1.a |
. . . . . . 7
       |
4 | | hoidmvlelem1.z |
. . . . . . . . . 10
     |
5 | | snidg 3986 |
. . . . . . . . . 10
       |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
     |
7 | | elun2 3593 |
. . . . . . . . 9
         |
8 | 6, 7 | syl 17 |
. . . . . . . 8
       |
9 | | hoidmvlelem1.w |
. . . . . . . 8
     |
10 | 8, 9 | syl6eleqr 2560 |
. . . . . . 7
   |
11 | 3, 10 | ffvelrnd 6038 |
. . . . . 6
       |
12 | | hoidmvlelem1.b |
. . . . . . 7
       |
13 | 12, 10 | ffvelrnd 6038 |
. . . . . 6
       |
14 | | hoidmvlelem1.u |
. . . . . . . 8
       ![[,] [,]](_icc.gif)                 Σ^                               |
15 | | ssrab2 3500 |
. . . . . . . 8
       ![[,] [,]](_icc.gif)                 Σ^                                    ![[,] [,]](_icc.gif)       |
16 | 14, 15 | eqsstri 3448 |
. . . . . . 7
      ![[,] [,]](_icc.gif)       |
17 | 16 | a1i 11 |
. . . . . 6

      ![[,] [,]](_icc.gif)        |
18 | 11 | leidd 10201 |
. . . . . . . . . . 11
    
      |
19 | | hoidmvlelem1.ab |
. . . . . . . . . . . 12
    
      |
20 | 11, 13, 19 | ltled 9800 |
. . . . . . . . . . 11
    
      |
21 | 11, 13, 11, 18, 20 | eliccd 37697 |
. . . . . . . . . 10
           ![[,] [,]](_icc.gif)        |
22 | 11 | recnd 9687 |
. . . . . . . . . . . . . 14
       |
23 | 22 | subidd 9993 |
. . . . . . . . . . . . 13
             |
24 | 23 | oveq2d 6324 |
. . . . . . . . . . . 12
                 |
25 | | rge0ssre 11766 |
. . . . . . . . . . . . . . 15
    |
26 | | hoidmvlelem1.g |
. . . . . . . . . . . . . . . 16
         
   |
27 | | hoidmvlelem1.l |
. . . . . . . . . . . . . . . . 17
                                |
28 | | hoidmvlelem1.x |
. . . . . . . . . . . . . . . . . 18
   |
29 | | hoidmvlelem1.y |
. . . . . . . . . . . . . . . . . 18

  |
30 | 28, 29 | ssfid 37473 |
. . . . . . . . . . . . . . . . 17
   |
31 | | ssun1 3588 |
. . . . . . . . . . . . . . . . . . . 20

    |
32 | 31, 9 | sseqtr4i 3451 |
. . . . . . . . . . . . . . . . . . 19
 |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . 18

  |
34 | 3, 33 | fssresd 5762 |
. . . . . . . . . . . . . . . . 17
         |
35 | 12, 33 | fssresd 5762 |
. . . . . . . . . . . . . . . . 17
         |
36 | 27, 30, 34, 35 | hoidmvcl 38522 |
. . . . . . . . . . . . . . . 16
          
       |
37 | 26, 36 | syl5eqel 2553 |
. . . . . . . . . . . . . . 15
      |
38 | 25, 37 | sseldi 3416 |
. . . . . . . . . . . . . 14
   |
39 | 38 | recnd 9687 |
. . . . . . . . . . . . 13
   |
40 | 39 | mul01d 9850 |
. . . . . . . . . . . 12
     |
41 | 24, 40 | eqtrd 2505 |
. . . . . . . . . . 11
               |
42 | | 1red 9676 |
. . . . . . . . . . . . 13
   |
43 | | hoidmvlelem1.e |
. . . . . . . . . . . . . 14
   |
44 | 43 | rpred 11364 |
. . . . . . . . . . . . 13
   |
45 | 42, 44 | readdcld 9688 |
. . . . . . . . . . . 12
     |
46 | | 0red 9662 |
. . . . . . . . . . . . 13
   |
47 | | 0lt1 10157 |
. . . . . . . . . . . . . . 15
 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
   |
49 | 42, 43 | ltaddrpd 11394 |
. . . . . . . . . . . . . 14
     |
50 | 46, 42, 45, 48, 49 | lttrd 9813 |
. . . . . . . . . . . . 13
     |
51 | 46, 45, 50 | ltled 9800 |
. . . . . . . . . . . 12

    |
52 | | nnex 10637 |
. . . . . . . . . . . . . . 15
 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
   |
54 | | icossicc 11746 |
. . . . . . . . . . . . . . . 16
       |
55 | | snfi 7668 |
. . . . . . . . . . . . . . . . . . . . 21
 
 |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
     |
57 | | unfi 7856 |
. . . . . . . . . . . . . . . . . . . 20
           |
58 | 30, 56, 57 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
       |
59 | 9, 58 | syl5eqel 2553 |
. . . . . . . . . . . . . . . . . 18
   |
60 | 59 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 

  |
61 | | hoidmvlelem1.c |
. . . . . . . . . . . . . . . . . . 19
         |
62 | 61 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . 18
 

        |
63 | | elmapi 7511 |
. . . . . . . . . . . . . . . . . 18
                 |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
 

          |
65 | | hoidmvlelem1.h |
. . . . . . . . . . . . . . . . . . 19
                   
           |
66 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
67 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
68 | 67 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       |
69 | 68, 67 | ifbieq1d 3895 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
         |
70 | 66, 67, 69 | ifbieq12d 3899 |
. . . . . . . . . . . . . . . . . . . . . 22
                                               |
71 | 70 | cbvmptv 4488 |
. . . . . . . . . . . . . . . . . . . . 21
              
                                  |
72 | 71 | mpteq2i 4479 |
. . . . . . . . . . . . . . . . . . . 20
                 
                            
          |
73 | 72 | mpteq2i 4479 |
. . . . . . . . . . . . . . . . . . 19
                  
                                          |
74 | 65, 73 | eqtri 2493 |
. . . . . . . . . . . . . . . . . 18
                   
           |
75 | 11 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 

      |
76 | | hoidmvlelem1.d |
. . . . . . . . . . . . . . . . . . . 20
         |
77 | 76 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . 19
 

        |
78 | | elmapi 7511 |
. . . . . . . . . . . . . . . . . . 19
                 |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 

          |
80 | 74, 75, 60, 79 | hsphoif 38516 |
. . . . . . . . . . . . . . . . 17
 

                      |
81 | 27, 60, 64, 80 | hoidmvcl 38522 |
. . . . . . . . . . . . . . . 16
 

                                 |
82 | 54, 81 | sseldi 3416 |
. . . . . . . . . . . . . . 15
 

                                 |
83 | | eqid 2471 |
. . . . . . . . . . . . . . 15
                                                             |
84 | 82, 83 | fmptd 6061 |
. . . . . . . . . . . . . 14
                                        |
85 | 53, 84 | sge0cl 38337 |
. . . . . . . . . . . . 13
 Σ^                                     |
86 | 53, 84 | sge0xrcl 38341 |
. . . . . . . . . . . . . 14
 Σ^                                  |
87 | | pnfxr 11435 |
. . . . . . . . . . . . . . 15
 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . 14
   |
89 | | hoidmvlelem1.r |
. . . . . . . . . . . . . . . 16
 Σ^                      |
90 | 89 | rexrd 9708 |
. . . . . . . . . . . . . . 15
 Σ^                      |
91 | | nfv 1769 |
. . . . . . . . . . . . . . . 16
   |
92 | 27, 60, 64, 79 | hoidmvcl 38522 |
. . . . . . . . . . . . . . . . 17
 

                     |
93 | 54, 92 | sseldi 3416 |
. . . . . . . . . . . . . . . 16
 

                     |
94 | 4 | eldifbd 3403 |
. . . . . . . . . . . . . . . . . . 19
   |
95 | 10, 94 | eldifd 3401 |
. . . . . . . . . . . . . . . . . 18
     |
96 | 95 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 

    |
97 | 27, 60, 96, 9, 75, 74, 64, 79 | hsphoidmvle 38526 |
. . . . . . . . . . . . . . . 16
 

                                              |
98 | 91, 53, 82, 93, 97 | sge0lempt 38366 |
. . . . . . . . . . . . . . 15
 Σ^                                Σ^                      |
99 | 89 | ltpnfd 11446 |
. . . . . . . . . . . . . . 15
 Σ^                      |
100 | 86, 90, 88, 98, 99 | xrlelttrd 11480 |
. . . . . . . . . . . . . 14
 Σ^                                  |
101 | 86, 88, 100 | xrltned 37667 |
. . . . . . . . . . . . 13
 Σ^                                  |
102 | | ge0xrre 37729 |
. . . . . . . . . . . . 13
  Σ^                                   Σ^                                 Σ^                                  |
103 | 85, 101, 102 | syl2anc 673 |
. . . . . . . . . . . 12
 Σ^                                  |
104 | 53, 84 | sge0ge0 38340 |
. . . . . . . . . . . 12

Σ^                                  |
105 | | mulge0 10153 |
. . . . . . . . . . . 12
    
    Σ^                               
Σ^                                     Σ^                                   |
106 | 45, 51, 103, 104, 105 | syl22anc 1293 |
. . . . . . . . . . 11

   Σ^                                   |
107 | 41, 106 | eqbrtrd 4416 |
. . . . . . . . . 10
            
   Σ^                                   |
108 | 21, 107 | jca 541 |
. . . . . . . . 9
            ![[,] [,]](_icc.gif)                     Σ^                                    |
109 | | oveq1 6315 |
. . . . . . . . . . . 12
                       |
110 | 109 | oveq2d 6324 |
. . . . . . . . . . 11
     
                     |
111 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
                   |
112 | 111 | fveq1d 5881 |
. . . . . . . . . . . . . . 15
                                   |
113 | 112 | oveq2d 6324 |
. . . . . . . . . . . . . 14
                                                           |
114 | 113 | mpteq2dv 4483 |
. . . . . . . . . . . . 13
                                                               |
115 | 114 | fveq2d 5883 |
. . . . . . . . . . . 12
     Σ^                            Σ^                                  |
116 | 115 | oveq2d 6324 |
. . . . . . . . . . 11
        Σ^                                Σ^                                   |
117 | 110, 116 | breq12d 4408 |
. . . . . . . . . 10
             
   Σ^                            
               Σ^                                    |
118 | 117 | elrab 3184 |
. . . . . . . . 9
            ![[,] [,]](_icc.gif)                 Σ^                                         ![[,] [,]](_icc.gif)                     Σ^                                    |
119 | 108, 118 | sylibr 217 |
. . . . . . . 8
            ![[,] [,]](_icc.gif)                 Σ^                                |
120 | 119, 14 | syl6eleqr 2560 |
. . . . . . 7
       |
121 | | ne0i 3728 |
. . . . . . 7
       |
122 | 120, 121 | syl 17 |
. . . . . 6
   |
123 | 11, 13, 17, 122 | supicc 11806 |
. . . . 5
    
      ![[,] [,]](_icc.gif)        |
124 | 2, 123 | eqeltrd 2549 |
. . . 4
       ![[,] [,]](_icc.gif)        |
125 | 2 | oveq1d 6323 |
. . . . . . 7
                   |
126 | 125 | oveq2d 6324 |
. . . . . 6
  
           
        |
127 | 11, 13 | iccssred 37698 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)     
  |
128 | 17, 127 | sstrd 3428 |
. . . . . . . 8

  |
129 | 11, 13 | jca 541 |
. . . . . . . . . 10
             |
130 | | iccsupr 11752 |
. . . . . . . . . 10
                  ![[,] [,]](_icc.gif)          
      |
131 | 129, 17, 120, 130 | syl3anc 1292 |
. . . . . . . . 9
  

   |
132 | 131 | simp3d 1044 |
. . . . . . . 8
     |
133 | | eqid 2471 |
. . . . . . . 8
 
        
        |
134 | 128, 122,
132, 11, 133 | supsubc 37663 |
. . . . . . 7
              
           |
135 | 134 | oveq2d 6324 |
. . . . . 6
                

            |
136 | 46 | rexrd 9708 |
. . . . . . . 8
   |
137 | | icogelb 11711 |
. . . . . . . 8
        |
138 | 136, 88, 37, 137 | syl3anc 1292 |
. . . . . . 7

  |
139 | | vex 3034 |
. . . . . . . . . . . 12
 |
140 | | eqeq1 2475 |
. . . . . . . . . . . . 13
       

        |
141 | 140 | rexbidv 2892 |
. . . . . . . . . . . 12
  
     


        |
142 | 139, 141 | elab 3173 |
. . . . . . . . . . 11
  
       
        |
143 | 142 | biimpi 199 |
. . . . . . . . . 10
  
       
        |
144 | 143 | adantl 473 |
. . . . . . . . 9
 
 

       
        |
145 | | nfv 1769 |
. . . . . . . . . . 11
   |
146 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
147 | | nfre1 2846 |
. . . . . . . . . . . . 13
  
       |
148 | 147 | nfab 2616 |
. . . . . . . . . . . 12
  

        |
149 | 146, 148 | nfel 2624 |
. . . . . . . . . . 11

 
        |
150 | 145, 149 | nfan 2031 |
. . . . . . . . . 10
  
 
         |
151 | | nfv 1769 |
. . . . . . . . . 10
 
 |
152 | 11 | rexrd 9708 |
. . . . . . . . . . . . . . . . 17
       |
153 | 152 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
       |
154 | 13 | rexrd 9708 |
. . . . . . . . . . . . . . . . 17
       |
155 | 154 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
       |
156 | 17 | sselda 3418 |
. . . . . . . . . . . . . . . 16
 
       ![[,] [,]](_icc.gif)        |
157 | | iccgelb 11716 |
. . . . . . . . . . . . . . . 16
                ![[,] [,]](_icc.gif)             |
158 | 153, 155,
156, 157 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
 
       |
159 | 128 | sselda 3418 |
. . . . . . . . . . . . . . . 16
 
   |
160 | 11 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
       |
161 | 159, 160 | subge0d 10224 |
. . . . . . . . . . . . . . 15
 
 
     
       |
162 | 158, 161 | mpbird 240 |
. . . . . . . . . . . . . 14
 
         |
163 | 162 | 3adant3 1050 |
. . . . . . . . . . . . 13
 
      
        |
164 | | id 22 |
. . . . . . . . . . . . . . 15
      

       |
165 | 164 | eqcomd 2477 |
. . . . . . . . . . . . . 14
      
        |
166 | 165 | 3ad2ant3 1053 |
. . . . . . . . . . . . 13
 
      
        |
167 | 163, 166 | breqtrd 4420 |
. . . . . . . . . . . 12
 
      
  |
168 | 167 | 3exp 1230 |
. . . . . . . . . . 11
             |
169 | 168 | adantr 472 |
. . . . . . . . . 10
 
 

                   |
170 | 150, 151,
169 | rexlimd 2866 |
. . . . . . . . 9
 
 

                  |
171 | 144, 170 | mpd 15 |
. . . . . . . 8
 
 

      
  |
172 | 171 | ralrimiva 2809 |
. . . . . . 7
   

         |
173 | | simp3 1032 |
. . . . . . . . . . . 12
 
      

       |
174 | 159, 160 | resubcld 10068 |
. . . . . . . . . . . . 13
 
         |
175 | 174 | 3adant3 1050 |
. . . . . . . . . . . 12
 
      
        |
176 | 173, 175 | eqeltrd 2549 |
. . . . . . . . . . 11
 
      
  |
177 | 176 | 3exp 1230 |
. . . . . . . . . 10
             |
178 | 177 | rexlimdv 2870 |
. . . . . . . . 9
            |
179 | 178 | alrimiv 1781 |
. . . . . . . 8
          
   |
180 | | abss 3484 |
. . . . . . . 8
  

         

    
   |
181 | 179, 180 | sylibr 217 |
. . . . . . 7
  
         |
182 | 23 | eqcomd 2477 |
. . . . . . . . . 10
             |
183 | | oveq1 6315 |
. . . . . . . . . . . 12
                       |
184 | 183 | eqeq2d 2481 |
. . . . . . . . . . 11
           
             |
185 | 184 | rspcev 3136 |
. . . . . . . . . 10
     
                    |
186 | 120, 182,
185 | syl2anc 673 |
. . . . . . . . 9
          |
187 | | c0ex 9655 |
. . . . . . . . . 10
 |
188 | | eqeq1 2475 |
. . . . . . . . . . 11
       

        |
189 | 188 | rexbidv 2892 |
. . . . . . . . . 10
  
     


        |
190 | 187, 189 | elab 3173 |
. . . . . . . . 9
  
       
        |
191 | 186, 190 | sylibr 217 |
. . . . . . . 8
  
         |
192 | | ne0i 3728 |
. . . . . . . 8
  
        
         |
193 | 191, 192 | syl 17 |
. . . . . . 7
  
         |
194 | 13, 11 | resubcld 10068 |
. . . . . . . 8
             |
195 | | vex 3034 |
. . . . . . . . . . . . 13
 |
196 | | eqeq1 2475 |
. . . . . . . . . . . . . 14
       

        |
197 | 196 | rexbidv 2892 |
. . . . . . . . . . . . 13
  
     


        |
198 | 195, 197 | elab 3173 |
. . . . . . . . . . . 12
  
       
        |
199 | 198 | biimpi 199 |
. . . . . . . . . . 11
  
       
        |
200 | 199 | adantl 473 |
. . . . . . . . . 10
 
 

       
        |
201 | | nfcv 2612 |
. . . . . . . . . . . . 13
   |
202 | 201, 148 | nfel 2624 |
. . . . . . . . . . . 12

 
        |
203 | 145, 202 | nfan 2031 |
. . . . . . . . . . 11
  
 
         |
204 | | nfv 1769 |
. . . . . . . . . . 11
            |
205 | | simp3 1032 |
. . . . . . . . . . . . . 14
 
      

       |
206 | 160 | 3adant3 1050 |
. . . . . . . . . . . . . . 15
 
      
      |
207 | 13 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . 15
 
      
      |
208 | 156 | 3adant3 1050 |
. . . . . . . . . . . . . . 15
 
      
      ![[,] [,]](_icc.gif)        |
209 | 21 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . 15
 
      
          ![[,] [,]](_icc.gif)        |
210 | 206, 207,
208, 209 | iccsuble 37716 |
. . . . . . . . . . . . . 14
 
      
                  |
211 | 205, 210 | eqbrtrd 4416 |
. . . . . . . . . . . . 13
 
      
            |
212 | 211 | 3exp 1230 |
. . . . . . . . . . . 12
                       |
213 | 212 | adantr 472 |
. . . . . . . . . . 11
 
 

                             |
214 | 203, 204,
213 | rexlimd 2866 |
. . . . . . . . . 10
 
 

                            |
215 | 200, 214 | mpd 15 |
. . . . . . . . 9
 
 

      
            |
216 | 215 | ralrimiva 2809 |
. . . . . . . 8
   

                   |
217 | | breq2 4399 |
. . . . . . . . . 10
          
              |
218 | 217 | ralbidv 2829 |
. . . . . . . . 9
          
 
 
       
  
                     |
219 | 218 | rspcev 3136 |
. . . . . . . 8
              
       
              
       
  |
220 | 194, 216,
219 | syl2anc 673 |
. . . . . . 7
    
       
  |
221 | | eqid 2471 |
. . . . . . . 8
   
              
            |
222 | | biid 244 |
. . . . . . . 8
  
  
       
   
      
 
          
         
 
  
          

        
       
  
            |
223 | 221, 222 | supmul1 10598 |
. . . . . . 7
  
  
       
   
      
 
          
              
               
               |
224 | 38, 138, 172, 181, 193, 220, 223 | syl33anc 1307 |
. . . . . 6
     
               
               |
225 | 126, 135,
224 | 3eqtrd 2509 |
. . . . 5
  
           
               |
226 | | vex 3034 |
. . . . . . . . . . . 12
 |
227 | | eqeq1 2475 |
. . . . . . . . . . . . 13
   

    |
228 | 227 | rexbidv 2892 |
. . . . . . . . . . . 12
  
 
         
  
             |
229 | 226, 228 | elab 3173 |
. . . . . . . . . . 11
    

         
  
            |
230 | 229 | biimpi 199 |
. . . . . . . . . 10
    

            
            |
231 | | nfv 1769 |
. . . . . . . . . . . 12
  
         |
232 | | vex 3034 |
. . . . . . . . . . . . . . . . 17
 |
233 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . 18
       

        |
234 | 233 | rexbidv 2892 |
. . . . . . . . . . . . . . . . 17
  
     


        |
235 | 232, 234 | elab 3173 |
. . . . . . . . . . . . . . . 16
  
       
        |
236 | 235 | biimpi 199 |
. . . . . . . . . . . . . . 15
  
       
        |
237 | 236 | adantr 472 |
. . . . . . . . . . . . . 14
   
         


       |
238 | | simpl 464 |
. . . . . . . . . . . . . . . . . 18
   
           |
239 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . 19
      
            |
240 | 239 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
   
                   |
241 | 238, 240 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
   
                 |
242 | 241 | ex 441 |
. . . . . . . . . . . . . . . 16
                     |
243 | 242 | reximdv 2857 |
. . . . . . . . . . . . . . 15
    
      
           |
244 | 243 | adantl 473 |
. . . . . . . . . . . . . 14
   
         
 
     


          |
245 | 237, 244 | mpd 15 |
. . . . . . . . . . . . 13
   
         


         |
246 | 245 | ex 441 |
. . . . . . . . . . . 12
  
         


          |
247 | 231, 246 | rexlimi 2864 |
. . . . . . . . . . 11
   
          
          |
248 | 247 | a1i 11 |
. . . . . . . . . 10
    

           
 
          
           |
249 | 230, 248 | mpd 15 |
. . . . . . . . 9
    

          

         |
250 | 249 | adantl 473 |
. . . . . . . 8
 
   
            
          |
251 | | simp3 1032 |
. . . . . . . . . . . 12
 
        

         |
252 | 38 | adantr 472 |
. . . . . . . . . . . . . . 15
 
   |
253 | 252, 174 | remulcld 9689 |
. . . . . . . . . . . . . 14
 
 
         |
254 | 45 | adantr 472 |
. . . . . . . . . . . . . . 15
 
     |
255 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
   |
256 | 60 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . 20
       |
257 | 64 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . 20
               |
258 | 159 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
       |
259 | 79 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . 21
               |
260 | 74, 258, 256, 259 | hsphoif 38516 |
. . . . . . . . . . . . . . . . . . . 20
                       |
261 | 27, 256, 257, 260 | hoidmvcl 38522 |
. . . . . . . . . . . . . . . . . . 19
                                  |
262 | 54, 261 | sseldi 3416 |
. . . . . . . . . . . . . . . . . 18
                                  |
263 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
                                                     |
264 | 262, 263 | fmptd 6061 |
. . . . . . . . . . . . . . . . 17
 
                                    |
265 | 255, 264 | sge0cl 38337 |
. . . . . . . . . . . . . . . 16
 
 Σ^                                 |
266 | 255, 264 | sge0xrcl 38341 |
. . . . . . . . . . . . . . . . 17
 
 Σ^                              |
267 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
   |
268 | 90 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
 Σ^                      |
269 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . 19
     |
270 | 93 | adantlr 729 |
. . . . . . . . . . . . . . . . . . 19
                          |
271 | 96 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . 20
         |
272 | 27, 256, 271, 9, 258, 74, 257, 259 | hsphoidmvle 38526 |
. . . . . . . . . . . . . . . . . . 19
                                               |
273 | 269, 255,
262, 270, 272 | sge0lempt 38366 |
. . . . . . . . . . . . . . . . . 18
 
 Σ^                            Σ^                      |
274 | 99 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
 Σ^                      |
275 | 266, 268,
267, 273, 274 | xrlelttrd 11480 |
. . . . . . . . . . . . . . . . 17
 
 Σ^                              |
276 | 266, 267,
275 | xrltned 37667 |
. . . . . . . . . . . . . . . 16
 
 Σ^                              |
277 | | ge0xrre 37729 |
. . . . . . . . . . . . . . . 16
  Σ^                               Σ^                             Σ^                              |
278 | 265, 276,
277 | syl2anc 673 |
. . . . . . . . . . . . . . 15
 
 Σ^                              |
279 | 254, 278 | remulcld 9689 |
. . . . . . . . . . . . . 14
 
    Σ^                               |
280 | 127, 124 | sseldd 3419 |
. . . . . . . . . . . . . . . . 17
   |
281 | 27, 30, 95, 9, 61, 76, 89, 65, 280 | sge0hsphoire 38529 |
. . . . . . . . . . . . . . . 16
 Σ^                              |
282 | 45, 281 | remulcld 9689 |
. . . . . . . . . . . . . . 15
    Σ^                               |
283 | 282 | adantr 472 |
. . . . . . . . . . . . . 14
 
    Σ^                               |
284 | 14 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . 18

       ![[,] [,]](_icc.gif)             
   Σ^                                |
285 | 284 | biimpi 199 |
. . . . . . . . . . . . . . . . 17
        ![[,] [,]](_icc.gif)                 Σ^                                |
286 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . 20
               |
287 | 286 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
 
        
        |
288 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
289 | 288 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . . . . . 23
                           |
290 | 289 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                   |
291 | 290 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . . . . . . 21
                                                       |
292 | 291 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . 20
 Σ^                            Σ^                              |
293 | 292 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
    Σ^                                Σ^                               |
294 | 287, 293 | breq12d 4408 |
. . . . . . . . . . . . . . . . . 18
         
   Σ^                            
           Σ^                                |
295 | 294 | elrab 3184 |
. . . . . . . . . . . . . . . . 17
        ![[,] [,]](_icc.gif)                 Σ^                                     ![[,] [,]](_icc.gif)       
         Σ^                                |
296 | 285, 295 | sylib 201 |
. . . . . . . . . . . . . . . 16
        ![[,] [,]](_icc.gif)      
      
   Σ^                                |
297 | 296 | simprd 470 |
. . . . . . . . . . . . . . 15
 
          Σ^                               |
298 | 297 | adantl 473 |
. . . . . . . . . . . . . 14
 
 
          Σ^                               |
299 | 281 | adantr 472 |
. . . . . . . . . . . . . . 15
 
 Σ^                              |
300 | 51 | adantr 472 |
. . . . . . . . . . . . . . 15
 
     |
301 | 280 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
302 | 74, 301, 60, 79 | hsphoif 38516 |
. . . . . . . . . . . . . . . . . . 19
 

                  |
303 | 27, 60, 64, 302 | hoidmvcl 38522 |
. . . . . . . . . . . . . . . . . 18
 

                             |
304 | 54, 303 | sseldi 3416 |
. . . . . . . . . . . . . . . . 17
 

                             |
305 | 304 | adantlr 729 |
. . . . . . . . . . . . . . . 16
                                  |
306 | 301 | adantlr 729 |
. . . . . . . . . . . . . . . . 17
       |
307 | 128 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
308 | 122 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
309 | 132 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
310 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
311 | | suprub 10592 |
. . . . . . . . . . . . . . . . . . . 20
   

     
  |
312 | 307, 308,
309, 310, 311 | syl31anc 1295 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
313 | 312, 1 | syl6breqr 4436 |
. . . . . . . . . . . . . . . . . 18
 
   |
314 | 313 | adantr 472 |
. . . . . . . . . . . . . . . . 17
       |
315 | 27, 256, 271, 9, 258, 306, 314, 74, 257, 259 | hsphoidmvle2 38525 |
. . . . . . . . . . . . . . . 16
                                                       |
316 | 269, 255,
262, 305, 315 | sge0lempt 38366 |
. . . . . . . . . . . . . . 15
 
 Σ^                            Σ^                              |
317 | 278, 299,
254, 300, 316 | lemul2ad 10569 |
. . . . . . . . . . . . . 14
 
    Σ^                                Σ^                               |
318 | 253, 279,
283, 298, 317 | letrd 9809 |
. . . . . . . . . . . . 13
 
 
          Σ^                               |
319 | 318 | 3adant3 1050 |
. . . . . . . . . . . 12
 
        
           Σ^                               |
320 | 251, 319 | eqbrtrd 4416 |
. . . . . . . . . . 11
 
        
   Σ^                               |
321 | 320 | 3exp 1230 |
. . . . . . . . . 10
              Σ^                                 |
322 | 321 | rexlimdv 2870 |
. . . . . . . . 9
              Σ^                                |
323 | 322 | adantr 472 |
. . . . . . . 8
 
   
                         Σ^                                |
324 | 250, 323 | mpd 15 |
. . . . . . 7
 
   
           
   Σ^                               |
325 | 324 | ralrimiva 2809 |
. . . . . 6
     
               Σ^                               |
326 | 230 | adantl 473 |
. . . . . . . . . 10
 
   
            
 
            |
327 | | nfv 1769 |
. . . . . . . . . . . 12
   |
328 | | nfcv 2612 |
. . . . . . . . . . . . 13
   |
329 | | nfre1 2846 |
. . . . . . . . . . . . . 14
    

          |
330 | 329 | nfab 2616 |
. . . . . . . . . . . . 13
   
 
            |
331 | 328, 330 | nfel 2624 |
. . . . . . . . . . . 12
    
            |
332 | 327, 331 | nfan 2031 |
. . . . . . . . . . 11
    
 
             |
333 | | nfv 1769 |
. . . . . . . . . . 11
  |
334 | 236 | adantl 473 |
. . . . . . . . . . . . . 14
 
 

       
        |
335 | | simpr 468 |
. . . . . . . . . . . . . . . . . . 19
  
              |
336 | 252 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
  |
337 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . . . 22
 
      

       |
338 | 174 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . . . 22
 
      
        |
339 | 337, 338 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
  |
340 | 336, 339 | remulcld 9689 |
. . . . . . . . . . . . . . . . . . . 20
 
      
    |
341 | 340 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
  
              |
342 | 335, 341 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . 18
  
            |
343 | 342 | ex 441 |
. . . . . . . . . . . . . . . . 17
 
      
      |
344 | 343 | 3exp 1230 |
. . . . . . . . . . . . . . . 16
           
     |
345 | 344 | rexlimdv 2870 |
. . . . . . . . . . . . . . 15
           
    |
346 | 345 | adantr 472 |
. . . . . . . . . . . . . 14
 
 

                 
    |
347 | 334, 346 | mpd 15 |
. . . . . . . . . . . . 13
 
 

             |
348 | 347 | ex 441 |
. . . . . . . . . . . 12
   

             |
349 | 348 | adantr 472 |
. . . . . . . . . . 11
 
   
              

             |
350 | 332, 333,
349 | rexlimd 2866 |
. . . . . . . . . 10
 
   
               
         
   |
351 | 326, 350 | mpd 15 |
. . . . . . . . 9
 
   
              |
352 | 351 | ralrimiva 2809 |
. . . . . . . 8
     
              |
353 | | dfss3 3408 |
. . . . . . . 8
    
               
              |
354 | 352, 353 | sylibr 217 |
. . . . . . 7
  
 
             |
355 | 40 | eqcomd 2477 |
. . . . . . . . . 10
     |
356 | | oveq2 6316 |
. . . . . . . . . . . 12
 
     |
357 | 356 | eqeq2d 2481 |
. . . . . . . . . . 11
   

    |
358 | 357 | rspcev 3136 |
. . . . . . . . . 10
   
         
  
            |
359 | 191, 355,
358 | syl2anc 673 |
. . . . . . . . 9
   

           |
360 | | eqeq1 2475 |
. . . . . . . . . . 11
   

    |
361 | 360 | rexbidv 2892 |
. . . . . . . . . 10
  
 
         
  
             |
362 | 187, 361 | elab 3173 |
. . . . . . . . 9
    

         
  
            |
363 | 359, 362 | sylibr 217 |
. . . . . . . 8
    
             |
364 | | ne0i 3728 |
. . . . . . . 8
    

             
             |
365 | 363, 364 | syl 17 |
. . . . . . 7
  
 
             |
366 | 38, 194 | remulcld 9689 |
. . . . . . . 8
               |
367 | 194 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
             |
368 | 138 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
   |
369 | 13 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
       |
370 | | iccleub 11715 |
. . . . . . . . . . . . . . . . . 18
                ![[,] [,]](_icc.gif)             |
371 | 153, 155,
156, 370 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
 
       |
372 | 159, 369,
160, 371 | lesub1dd 10250 |
. . . . . . . . . . . . . . . 16
 
                   |
373 | 174, 367,
252, 368, 372 | lemul2ad 10569 |
. . . . . . . . . . . . . . 15
 
 
                     |
374 | 373 | 3adant3 1050 |
. . . . . . . . . . . . . 14
 
        
        
             |
375 | 251, 374 | eqbrtrd 4416 |
. . . . . . . . . . . . 13
 
        
              |
376 | 375 | 3exp 1230 |
. . . . . . . . . . . 12
           
               |
377 | 376 | rexlimdv 2870 |
. . . . . . . . . . 11
           
              |
378 | 377 | adantr 472 |
. . . . . . . . . 10
 
   
                      
              |
379 | 250, 378 | mpd 15 |
. . . . . . . . 9
 
   
           
              |
380 | 379 | ralrimiva 2809 |
. . . . . . . 8
     
                          |
381 | | breq2 4399 |
. . . . . . . . . 10
             
               |
382 | 381 | ralbidv 2829 |
. . . . . . . . 9
              
   
                
                           |
383 | 382 | rspcev 3136 |
. . . . . . . 8
                  
                            
 
           
  |
384 | 366, 380,
383 | syl2anc 673 |
. . . . . . 7
      
              |
385 | | suprleub 10595 |
. . . . . . 7
      

           
 
              
 
           
    Σ^                                    

               Σ^   |