Step | Hyp | Ref
| Expression |
1 | | ivth.7 |
. . . . 5
       |
2 | 1 | adantr 452 |
. . . 4
 
    
      |
3 | | ivth.5 |
. . . . . 6
   ![[,] [,]](_icc.gif) 
  |
4 | | ivth.11 |
. . . . . . . 8
   
 |
5 | | ivth.10 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)        |
6 | | ssrab2 3392 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)      
  ![[,] [,]](_icc.gif)   |
7 | 5, 6 | eqsstri 3342 |
. . . . . . . . . . 11
  ![[,] [,]](_icc.gif)   |
8 | | ivth.1 |
. . . . . . . . . . . 12
   |
9 | | ivth.2 |
. . . . . . . . . . . 12
   |
10 | | iccssre 10952 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif) 
  |
11 | 8, 9, 10 | syl2anc 643 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif) 
  |
12 | 7, 11 | syl5ss 3323 |
. . . . . . . . . 10

  |
13 | | ivth.3 |
. . . . . . . . . . . . 13
   |
14 | | ivth.4 |
. . . . . . . . . . . . 13
   |
15 | | ivth.8 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
      |
16 | | ivth.9 |
. . . . . . . . . . . . 13
     
       |
17 | 8, 9, 13, 14, 3, 1, 15, 16, 5 | ivthlem1 19305 |
. . . . . . . . . . . 12
      |
18 | 17 | simpld 446 |
. . . . . . . . . . 11
   |
19 | | ne0i 3598 |
. . . . . . . . . . 11
   |
20 | 18, 19 | syl 16 |
. . . . . . . . . 10
   |
21 | 17 | simprd 450 |
. . . . . . . . . . 11
    |
22 | | breq2 4180 |
. . . . . . . . . . . . 13
 
   |
23 | 22 | ralbidv 2690 |
. . . . . . . . . . . 12
  

   |
24 | 23 | rspcev 3016 |
. . . . . . . . . . 11
    
   |
25 | 9, 21, 24 | syl2anc 643 |
. . . . . . . . . 10
     |
26 | 12, 20, 25 | 3jca 1134 |
. . . . . . . . 9
  

   |
27 | | suprcl 9928 |
. . . . . . . . 9
 
  
  
   |
28 | 26, 27 | syl 16 |
. . . . . . . 8
    
  |
29 | 4, 28 | syl5eqel 2492 |
. . . . . . 7
   |
30 | | suprub 9929 |
. . . . . . . . 9
   

     
  |
31 | 26, 18, 30 | syl2anc 643 |
. . . . . . . 8

  
   |
32 | 31, 4 | syl6breqr 4216 |
. . . . . . 7

  |
33 | | suprleub 9932 |
. . . . . . . . . 10
   

           |
34 | 26, 9, 33 | syl2anc 643 |
. . . . . . . . 9
     

   |
35 | 21, 34 | mpbird 224 |
. . . . . . . 8
    
  |
36 | 4, 35 | syl5eqbr 4209 |
. . . . . . 7

  |
37 | | elicc2 10935 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif)  
    |
38 | 8, 9, 37 | syl2anc 643 |
. . . . . . 7
    ![[,] [,]](_icc.gif)  
    |
39 | 29, 32, 36, 38 | mpbir3and 1137 |
. . . . . 6
   ![[,] [,]](_icc.gif)    |
40 | 3, 39 | sseldd 3313 |
. . . . 5
   |
41 | 40 | adantr 452 |
. . . 4
 
    
  |
42 | 15 | ralrimiva 2753 |
. . . . . . 7
    ![[,] [,]](_icc.gif)         |
43 | | fveq2 5691 |
. . . . . . . . 9
           |
44 | 43 | eleq1d 2474 |
. . . . . . . 8
     
       |
45 | 44 | rspcv 3012 |
. . . . . . 7
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)              |
46 | 39, 42, 45 | sylc 58 |
. . . . . 6
       |
47 | | difrp 10605 |
. . . . . 6
     
               |
48 | 46, 13, 47 | syl2anc 643 |
. . . . 5
               |
49 | 48 | biimpa 471 |
. . . 4
 
    
        |
50 | | cncfi 18881 |
. . . 4
     

     
                                |
51 | 2, 41, 49, 50 | syl3anc 1184 |
. . 3
 
    
                                |
52 | | ssralv 3371 |
. . . . . . 7
   ![[,] [,]](_icc.gif)   
                               ![[,] [,]](_icc.gif)                                  |
53 | 3, 52 | syl 16 |
. . . . . 6
                                  ![[,] [,]](_icc.gif)                                  |
54 | 53 | ad2antrr 707 |
. . . . 5
          
                               ![[,] [,]](_icc.gif)                                  |
55 | 9 | ad2antrr 707 |
. . . . . . . . 9
           |
56 | 29 | ad2antrr 707 |
. . . . . . . . . 10
           |
57 | | rphalfcl 10596 |
. . . . . . . . . . . 12

    |
58 | 57 | adantl 453 |
. . . . . . . . . . 11
             |
59 | 58 | rpred 10608 |
. . . . . . . . . 10
             |
60 | 56, 59 | readdcld 9075 |
. . . . . . . . 9
         
     |
61 | | ifcl 3739 |
. . . . . . . . 9
  
                   |
62 | 55, 60, 61 | syl2anc 643 |
. . . . . . . 8
          
             |
63 | 8 | ad2antrr 707 |
. . . . . . . . 9
           |
64 | 32 | ad2antrr 707 |
. . . . . . . . 9
           |
65 | 16 | simprd 450 |
. . . . . . . . . . . . . . 15
       |
66 | 8 | rexrd 9094 |
. . . . . . . . . . . . . . . . . 18
   |
67 | 9 | rexrd 9094 |
. . . . . . . . . . . . . . . . . 18
   |
68 | 8, 9, 14 | ltled 9181 |
. . . . . . . . . . . . . . . . . 18

  |
69 | | ubicc2 10974 |
. . . . . . . . . . . . . . . . . 18
     ![[,] [,]](_icc.gif)    |
70 | 66, 67, 68, 69 | syl3anc 1184 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)    |
71 | | fveq2 5691 |
. . . . . . . . . . . . . . . . . . 19
           |
72 | 71 | eleq1d 2474 |
. . . . . . . . . . . . . . . . . 18
     
       |
73 | 72 | rspcv 3012 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)              |
74 | 70, 42, 73 | sylc 58 |
. . . . . . . . . . . . . . . 16
       |
75 | | lttr 9112 |
. . . . . . . . . . . . . . . 16
     
          
                |
76 | 46, 13, 74, 75 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
      
    
           |
77 | 65, 76 | mpan2d 656 |
. . . . . . . . . . . . . 14
         
       |
78 | 77 | imp 419 |
. . . . . . . . . . . . 13
 
    
          |
79 | 78 | adantr 452 |
. . . . . . . . . . . 12
                   |
80 | 46 | ltnrd 9167 |
. . . . . . . . . . . . . . . . 17
           |
81 | | fveq2 5691 |
. . . . . . . . . . . . . . . . . . 19
           |
82 | 81 | breq2d 4188 |
. . . . . . . . . . . . . . . . . 18
     
   
           |
83 | 82 | notbid 286 |
. . . . . . . . . . . . . . . . 17
     
   
           |
84 | 80, 83 | syl5ibrcom 214 |
. . . . . . . . . . . . . . . 16
 
           |
85 | 84 | necon2ad 2619 |
. . . . . . . . . . . . . . 15
             |
86 | 85, 36 | jctild 528 |
. . . . . . . . . . . . . 14
          
    |
87 | 29, 9 | ltlend 9178 |
. . . . . . . . . . . . . 14
  
    |
88 | 86, 87 | sylibrd 226 |
. . . . . . . . . . . . 13
             |
89 | 88 | ad2antrr 707 |
. . . . . . . . . . . 12
             
       |
90 | 79, 89 | mpd 15 |
. . . . . . . . . . 11
           |
91 | 56, 58 | ltaddrpd 10637 |
. . . . . . . . . . 11
               |
92 | | breq2 4180 |
. . . . . . . . . . . 12
                               |
93 | | breq2 4180 |
. . . . . . . . . . . 12
                   
  
                |
94 | 92, 93 | ifboth 3734 |
. . . . . . . . . . 11
                      |
95 | 90, 91, 94 | syl2anc 643 |
. . . . . . . . . 10
                        |
96 | 56, 62, 95 | ltled 9181 |
. . . . . . . . 9
                        |
97 | 63, 56, 62, 64, 96 | letrd 9187 |
. . . . . . . 8
                        |
98 | | min1 10736 |
. . . . . . . . 9
  
                   |
99 | 55, 60, 98 | syl2anc 643 |
. . . . . . . 8
          
             |
100 | | elicc2 10935 |
. . . . . . . . . 10
 
                 ![[,] [,]](_icc.gif)    
                         
               |
101 | 8, 9, 100 | syl2anc 643 |
. . . . . . . . 9
                 ![[,] [,]](_icc.gif)    
                         
               |
102 | 101 | ad2antrr 707 |
. . . . . . . 8
            
            ![[,] [,]](_icc.gif) 
  
                         
               |
103 | 62, 97, 99, 102 | mpbir3and 1137 |
. . . . . . 7
          
             ![[,] [,]](_icc.gif)    |
104 | 56, 62, 96 | abssubge0d 12193 |
. . . . . . . 8
              
               
              |
105 | | rpre 10578 |
. . . . . . . . . . . 12

  |
106 | 105 | adantl 453 |
. . . . . . . . . . 11
           |
107 | 56, 106 | readdcld 9075 |
. . . . . . . . . 10
         
   |
108 | | min2 10737 |
. . . . . . . . . . 11
  
                       |
109 | 55, 60, 108 | syl2anc 643 |
. . . . . . . . . 10
          
                 |
110 | | rphalflt 10598 |
. . . . . . . . . . . 12

    |
111 | 110 | adantl 453 |
. . . . . . . . . . 11
             |
112 | 59, 106, 56, 111 | ltadd2dd 9189 |
. . . . . . . . . 10
         
       |
113 | 62, 60, 107, 109, 112 | lelttrd 9188 |
. . . . . . . . 9
          
               |
114 | 62, 56, 106 | ltsubadd2d 9584 |
. . . . . . . . 9
                           
               |
115 | 113, 114 | mpbird 224 |
. . . . . . . 8
            
             |
116 | 104, 115 | eqbrtrd 4196 |
. . . . . . 7
              
               |
117 | | oveq1 6051 |
. . . . . . . . . . 11
                   
             |
118 | 117 | fveq2d 5695 |
. . . . . . . . . 10
                                         |
119 | 118 | breq1d 4186 |
. . . . . . . . 9
                    
                      |
120 | | breq2 4180 |
. . . . . . . . 9
                               |
121 | 119, 120 | anbi12d 692 |
. . . . . . . 8
                     
        
                             |
122 | 121 | rspcev 3016 |
. . . . . . 7
                 ![[,] [,]](_icc.gif)                     
  
            
  ![[,] [,]](_icc.gif)             |
123 | 103, 116,
95, 122 | syl12anc 1182 |
. . . . . 6
            ![[,] [,]](_icc.gif)         
   |
124 | | r19.29 2810 |
. . . . . . 7
     ![[,] [,]](_icc.gif)                                  ![[,] [,]](_icc.gif)         
 
   ![[,] [,]](_icc.gif)                         
            
    |
125 | | pm3.45 808 |
. . . . . . . . . 10
                                                               |
126 | 125 | imp 419 |
. . . . . . . . 9
                                    
 
               
        |
127 | | simprr 734 |
. . . . . . . . . . . . . 14
        
    ![[,] [,]](_icc.gif)      |
128 | | simprl 733 |
. . . . . . . . . . . . . . . . 17
        
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
129 | | simplll 735 |
. . . . . . . . . . . . . . . . . 18
        
    ![[,] [,]](_icc.gif)      |
130 | 129, 42 | syl 16 |
. . . . . . . . . . . . . . . . 17
        
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
131 | | fveq2 5691 |
. . . . . . . . . . . . . . . . . . 19
           |
132 | 131 | eleq1d 2474 |
. . . . . . . . . . . . . . . . . 18
     
       |
133 | 132 | rspcv 3012 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)              |
134 | 128, 130,
133 | sylc 58 |
. . . . . . . . . . . . . . . 16
        
    ![[,] [,]](_icc.gif)          |
135 | 129, 46 | syl 16 |
. . . . . . . . . . . . . . . 16
        
    ![[,] [,]](_icc.gif)          |
136 | 129, 13 | syl 16 |
. . . . . . . . . . . . . . . . 17
        
    ![[,] [,]](_icc.gif)      |
137 | 136, 135 | resubcld 9425 |
. . . . . . . . . . . . . . . 16
        
    ![[,] [,]](_icc.gif)    
       |
138 | 134, 135,
137 | absdifltd 12195 |
. . . . . . . . . . . . . . 15
        
    ![[,] [,]](_icc.gif)                        
                                     |
139 | | ltle 9123 |
. . . . . . . . . . . . . . . . . . 19
     
         
   |
140 | 134, 136,
139 | syl2anc 643 |
. . . . . . . . . . . . . . . . . 18
        
    ![[,] [,]](_icc.gif)        
       |
141 | 135 | recnd 9074 |
. . . . . . . . . . . . . . . . . . . 20
        
    ![[,] [,]](_icc.gif)          |
142 | 136 | recnd 9074 |
. . . . . . . . . . . . . . . . . . . 20
        
    ![[,] [,]](_icc.gif)      |
143 | 141, 142 | pncan3d 9374 |
. . . . . . . . . . . . . . . . . . 19
        
    ![[,] [,]](_icc.gif)                  |
144 | 143 | breq2d 4188 |
. . . . . . . . . . . . . . . . . 18
        
    ![[,] [,]](_icc.gif)        
           
       |
145 | 131 | breq1d 4186 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
146 | 145, 5 | elrab2 3058 |
. . . . . . . . . . . . . . . . . . . 20

   ![[,] [,]](_icc.gif) 
       |
147 | 146 | baib 872 |
. . . . . . . . . . . . . . . . . . 19
   ![[,] [,]](_icc.gif)  
       |
148 | 147 | ad2antrl 709 |
. . . . . . . . . . . . . . . . . 18
        
    ![[,] [,]](_icc.gif)    
       |
149 | 140, 144,
148 | 3imtr4d 260 |
. . . . . . . . . . . . . . . . 17
        
    ![[,] [,]](_icc.gif)        
               |
150 | | suprub 9929 |
. . . . . . . . . . . . . . . . . . . . 21
   

     
  |
151 | 150, 4 | syl6breqr 4216 |
. . . . . . . . . . . . . . . . . . . 20
   

    |
152 | 151 | ex 424 |
. . . . . . . . . . . . . . . . . . 19
 
  

   |
153 | 129, 26, 152 | 3syl 19 |
. . . . . . . . . . . . . . . . . 18
        
    ![[,] [,]](_icc.gif)    
   |
154 | 129, 11 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
        
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
155 | 154, 128 | sseldd 3313 |
. . . . . . . . . . . . . . . . . . 19
        
    ![[,] [,]](_icc.gif)      |
156 | 129, 29 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
        
    ![[,] [,]](_icc.gif)      |
157 | 155, 156 | lenltd 9179 |
. . . . . . . . . . . . . . . . . 18
        
    ![[,] [,]](_icc.gif)    
   |
158 | 153, 157 | sylibd 206 |
. . . . . . . . . . . . . . . . 17
        
    ![[,] [,]](_icc.gif)    
   |
159 | 149, 158 | syld 42 |
. . . . . . . . . . . . . . . 16
        
    ![[,] [,]](_icc.gif)        
               |
160 | 159 | adantld 454 |
. . . . . . . . . . . . . . 15
        
    ![[,] [,]](_icc.gif)           
             
            
   |
161 | 138, 160 | sylbid 207 |
. . . . . . . . . . . . . 14
        
    ![[,] [,]](_icc.gif)                        
   |
162 | 127, 161 | mt2d 111 |
. . . . . . . . . . . . 13
        
    ![[,] [,]](_icc.gif)                          |
163 | 162 | pm2.21d 100 |
. . . . . . . . . . . 12
        
    ![[,] [,]](_icc.gif)                            
   |
164 | 163 | expr 599 |
. . . . . . . . . . 11
        

  ![[,] [,]](_icc.gif)                            
    |
165 | 164 | com23 74 |
. . . . . . . . . 10
        

  ![[,] [,]](_icc.gif)                                 |
166 | 165 | imp3a 421 |
. . . . . . . . 9
        

  ![[,] [,]](_icc.gif)                   
         
   |
167 | 126, 166 | syl5 30 |
. . . . . . . 8
        

  ![[,] [,]](_icc.gif)                          
            
 
       |
168 | 167 | rexlimdva 2794 |
. . . . . . 7
          
  ![[,] [,]](_icc.gif)                                      
 
       |
169 | 124, 168 | syl5 30 |
. . . . . 6
              ![[,] [,]](_icc.gif)                                  ![[,] [,]](_icc.gif)         
 
       |
170 | 123, 169 | mpan2d 656 |
. . . . 5
          
  ![[,] [,]](_icc.gif)                              
       |
171 | 54, 170 | syld 42 |
. . . 4
          
                           
       |
172 | 171 | rexlimdva 2794 |
. . 3
 
    
 

      
              
     
       |
173 | 51, 172 | mpd 15 |
. 2
 
    
      |
174 | 173 | pm2.01da 430 |
1
       |