Step | Hyp | Ref
| Expression |
1 | | ivth.11 |
. . . 4
   
 |
2 | | ivth.10 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)        |
3 | | ssrab2 3500 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)      
  ![[,] [,]](_icc.gif)   |
4 | 2, 3 | eqsstri 3448 |
. . . . . . 7
  ![[,] [,]](_icc.gif)   |
5 | | ivth.1 |
. . . . . . . 8
   |
6 | | ivth.2 |
. . . . . . . 8
   |
7 | | iccssre 11741 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif) 
  |
8 | 5, 6, 7 | syl2anc 673 |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
  |
9 | 4, 8 | syl5ss 3429 |
. . . . . 6

  |
10 | | ivth.3 |
. . . . . . . . 9
   |
11 | | ivth.4 |
. . . . . . . . 9
   |
12 | | ivth.5 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif) 
  |
13 | | ivth.7 |
. . . . . . . . 9
       |
14 | | ivth.8 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
      |
15 | | ivth.9 |
. . . . . . . . 9
     
       |
16 | 5, 6, 10, 11, 12, 13, 14, 15, 2 | ivthlem1 22480 |
. . . . . . . 8
      |
17 | 16 | simpld 466 |
. . . . . . 7
   |
18 | | ne0i 3728 |
. . . . . . 7
   |
19 | 17, 18 | syl 17 |
. . . . . 6
   |
20 | 16 | simprd 470 |
. . . . . . 7
    |
21 | | breq2 4399 |
. . . . . . . . 9
 
   |
22 | 21 | ralbidv 2829 |
. . . . . . . 8
  

   |
23 | 22 | rspcev 3136 |
. . . . . . 7
    
   |
24 | 6, 20, 23 | syl2anc 673 |
. . . . . 6
     |
25 | 9, 19, 24 | 3jca 1210 |
. . . . 5
  

   |
26 | | suprcl 10591 |
. . . . 5
 
  
  
   |
27 | 25, 26 | syl 17 |
. . . 4
    
  |
28 | 1, 27 | syl5eqel 2553 |
. . 3
   |
29 | 15 | simpld 466 |
. . . . 5
    
  |
30 | 5, 6, 10, 11, 12, 13, 14, 15, 2, 1 | ivthlem2 22481 |
. . . . . 6
       |
31 | 13 | adantr 472 |
. . . . . . . . 9
 
    
      |
32 | | suprub 10592 |
. . . . . . . . . . . . . 14
   

     
  |
33 | 25, 17, 32 | syl2anc 673 |
. . . . . . . . . . . . 13

  
   |
34 | 33, 1 | syl6breqr 4436 |
. . . . . . . . . . . 12

  |
35 | | suprleub 10595 |
. . . . . . . . . . . . . . 15
   

           |
36 | 25, 6, 35 | syl2anc 673 |
. . . . . . . . . . . . . 14
     

   |
37 | 20, 36 | mpbird 240 |
. . . . . . . . . . . . 13
    
  |
38 | 1, 37 | syl5eqbr 4429 |
. . . . . . . . . . . 12

  |
39 | | elicc2 11724 |
. . . . . . . . . . . . 13
 
    ![[,] [,]](_icc.gif)  
    |
40 | 5, 6, 39 | syl2anc 673 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)  
    |
41 | 28, 34, 38, 40 | mpbir3and 1213 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
42 | 12, 41 | sseldd 3419 |
. . . . . . . . . 10
   |
43 | 42 | adantr 472 |
. . . . . . . . 9
 
    
  |
44 | 14 | ralrimiva 2809 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)         |
45 | | fveq2 5879 |
. . . . . . . . . . . . . 14
           |
46 | 45 | eleq1d 2533 |
. . . . . . . . . . . . 13
     
       |
47 | 46 | rspcv 3132 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)              |
48 | 41, 44, 47 | sylc 61 |
. . . . . . . . . . 11
       |
49 | | difrp 11360 |
. . . . . . . . . . 11
                     |
50 | 10, 48, 49 | syl2anc 673 |
. . . . . . . . . 10
               |
51 | 50 | biimpa 492 |
. . . . . . . . 9
 
    
        |
52 | | cncfi 22004 |
. . . . . . . . 9
     
                                       |
53 | 31, 43, 51, 52 | syl3anc 1292 |
. . . . . . . 8
 
    
                                |
54 | | ssralv 3479 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)   
                               ![[,] [,]](_icc.gif)                                  |
55 | 12, 54 | syl 17 |
. . . . . . . . . . 11
                                  ![[,] [,]](_icc.gif)                                  |
56 | 55 | ad2antrr 740 |
. . . . . . . . . 10
          
                               ![[,] [,]](_icc.gif)                                  |
57 | 28 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
           |
58 | | ltsubrp 11358 |
. . . . . . . . . . . . . . 15
 
  
  |
59 | 57, 58 | sylancom 680 |
. . . . . . . . . . . . . 14
         
   |
60 | 59, 1 | syl6breq 4435 |
. . . . . . . . . . . . 13
         
    
  |
61 | 25 | ad2antrr 740 |
. . . . . . . . . . . . . 14
               |
62 | | rpre 11331 |
. . . . . . . . . . . . . . . 16

  |
63 | 62 | adantl 473 |
. . . . . . . . . . . . . . 15
           |
64 | 57, 63 | resubcld 10068 |
. . . . . . . . . . . . . 14
         
   |
65 | | suprlub 10593 |
. . . . . . . . . . . . . 14
   

      
  
  

   |
66 | 61, 64, 65 | syl2anc 673 |
. . . . . . . . . . . . 13
           
  
  

   |
67 | 60, 66 | mpbid 215 |
. . . . . . . . . . . 12
         
    |
68 | 4 | sseli 3414 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif)    |
69 | 68 | ad2antrl 742 |
. . . . . . . . . . . . . . 15
        
   
 
  ![[,] [,]](_icc.gif)    |
70 | | simplll 776 |
. . . . . . . . . . . . . . . . . . 19
        
   
 
  |
71 | 70, 8 | syl 17 |
. . . . . . . . . . . . . . . . . 18
        
   
 
  ![[,] [,]](_icc.gif)    |
72 | 71, 69 | sseldd 3419 |
. . . . . . . . . . . . . . . . 17
        
   
 
  |
73 | 70, 28 | syl 17 |
. . . . . . . . . . . . . . . . 17
        
   
 
  |
74 | 70, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
        
   
 
      |
75 | | simprl 772 |
. . . . . . . . . . . . . . . . . . 19
        
   
 
  |
76 | | suprub 10592 |
. . . . . . . . . . . . . . . . . . 19
   

     
  |
77 | 74, 75, 76 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
        
   
 
      |
78 | 77, 1 | syl6breqr 4436 |
. . . . . . . . . . . . . . . . 17
        
   
 
  |
79 | 72, 73, 78 | abssuble0d 13571 |
. . . . . . . . . . . . . . . 16
        
   
 
          |
80 | 63 | adantr 472 |
. . . . . . . . . . . . . . . . 17
        
   
 
  |
81 | | simprr 774 |
. . . . . . . . . . . . . . . . 17
        
   
 
    |
82 | 73, 80, 72, 81 | ltsub23d 10239 |
. . . . . . . . . . . . . . . 16
        
   
 
    |
83 | 79, 82 | eqbrtrd 4416 |
. . . . . . . . . . . . . . 15
        
   
 
        |
84 | 69, 83, 75 | jca32 544 |
. . . . . . . . . . . . . 14
        
   
 
   ![[,] [,]](_icc.gif) 
      
    |
85 | 84 | ex 441 |
. . . . . . . . . . . . 13
            
    ![[,] [,]](_icc.gif)        
     |
86 | 85 | reximdv2 2855 |
. . . . . . . . . . . 12
          


   ![[,] [,]](_icc.gif)         
    |
87 | 67, 86 | mpd 15 |
. . . . . . . . . . 11
            ![[,] [,]](_icc.gif)         
   |
88 | | r19.29 2912 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)                                  ![[,] [,]](_icc.gif)         
     ![[,] [,]](_icc.gif)                                           |
89 | | pm3.45 852 |
. . . . . . . . . . . . . . 15
                                                          
    |
90 | 89 | imp 436 |
. . . . . . . . . . . . . 14
                                    
                      
   |
91 | 68 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . . 21
             ![[,] [,]](_icc.gif)    |
92 | 44 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . 21
           
  ![[,] [,]](_icc.gif)         |
93 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
94 | 93 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
95 | 94 | rspcv 3132 |
. . . . . . . . . . . . . . . . . . . . 21
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)              |
96 | 91, 92, 95 | sylc 61 |
. . . . . . . . . . . . . . . . . . . 20
                 |
97 | 48 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . 20
                 |
98 | 10 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . 21
          
  |
99 | 97, 98 | resubcld 10068 |
. . . . . . . . . . . . . . . . . . . 20
                   |
100 | 96, 97, 99 | absdifltd 13572 |
. . . . . . . . . . . . . . . . . . 19
                               
                                     |
101 | 97 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
102 | 98 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
  |
103 | 101, 102 | nncand 10010 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
104 | 103 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . 21
                                   |
105 | 93 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
       |
106 | 105, 2 | elrab2 3186 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

   ![[,] [,]](_icc.gif) 
       |
107 | 106 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
108 | 107 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
  |
109 | 96, 98 | lenltd 9798 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
110 | 108, 109 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . 22
          
      |
111 | 110 | pm2.21d 109 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
112 | 104, 111 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
113 | 112 | adantrd 475 |
. . . . . . . . . . . . . . . . . . 19
                            
                
       |
114 | 100, 113 | sylbid 223 |
. . . . . . . . . . . . . . . . . 18
                               
       |
115 | 114 | expr 626 |
. . . . . . . . . . . . . . . . 17
                              
        |
116 | 115 | com23 80 |
. . . . . . . . . . . . . . . 16
                                       |
117 | 116 | impd 438 |
. . . . . . . . . . . . . . 15
                              
        |
118 | 117 | adantr 472 |
. . . . . . . . . . . . . 14
        

  ![[,] [,]](_icc.gif)                         
       |
119 | 90, 118 | syl5 32 |
. . . . . . . . . . . . 13
        

  ![[,] [,]](_icc.gif)                                         
       |
120 | 119 | rexlimdva 2871 |
. . . . . . . . . . . 12
          
  ![[,] [,]](_icc.gif)                                      
         |
121 | 88, 120 | syl5 32 |
. . . . . . . . . . 11
              ![[,] [,]](_icc.gif)                                  ![[,] [,]](_icc.gif)         
         |
122 | 87, 121 | mpan2d 688 |
. . . . . . . . . 10
          
  ![[,] [,]](_icc.gif)                              
       |
123 | 56, 122 | syld 44 |
. . . . . . . . 9
          
                           
       |
124 | 123 | rexlimdva 2871 |
. . . . . . . 8
 
    
 

      
                    
       |
125 | 53, 124 | mpd 15 |
. . . . . . 7
 
    
      |
126 | 125 | pm2.01da 449 |
. . . . . 6
       |
127 | 48, 10 | lttri3d 9792 |
. . . . . 6
          
        |
128 | 30, 126, 127 | mpbir2and 936 |
. . . . 5
       |
129 | 29, 128 | breqtrrd 4422 |
. . . 4
    
      |
130 | 48 | ltnrd 9786 |
. . . . . . . 8
           |
131 | | fveq2 5879 |
. . . . . . . . . 10
           |
132 | 131 | breq1d 4405 |
. . . . . . . . 9
     
   
           |
133 | 132 | notbid 301 |
. . . . . . . 8
     
   
           |
134 | 130, 133 | syl5ibcom 228 |
. . . . . . 7
 
           |
135 | 134 | necon2ad 2658 |
. . . . . 6
             |
136 | 135, 34 | jctild 552 |
. . . . 5
          
    |
137 | 5, 28 | ltlend 9797 |
. . . . 5
  
    |
138 | 136, 137 | sylibrd 242 |
. . . 4
             |
139 | 129, 138 | mpd 15 |
. . 3
   |
140 | 15 | simprd 470 |
. . . . 5
       |
141 | 128, 140 | eqbrtrd 4416 |
. . . 4
    
      |
142 | | fveq2 5879 |
. . . . . . . . . 10
           |
143 | 142 | breq2d 4407 |
. . . . . . . . 9
     
   
           |
144 | 143 | notbid 301 |
. . . . . . . 8
     
   
           |
145 | 130, 144 | syl5ibrcom 230 |
. . . . . . 7
 
           |
146 | 145 | necon2ad 2658 |
. . . . . 6
             |
147 | 146, 38 | jctild 552 |
. . . . 5
          
    |
148 | 28, 6 | ltlend 9797 |
. . . . 5
  
    |
149 | 147, 148 | sylibrd 242 |
. . . 4
             |
150 | 141, 149 | mpd 15 |
. . 3
   |
151 | 5 | rexrd 9708 |
. . . 4
   |
152 | 6 | rexrd 9708 |
. . . 4
   |
153 | | elioo2 11702 |
. . . 4
   
   

    |
154 | 151, 152,
153 | syl2anc 673 |
. . 3
           |
155 | 28, 139, 150, 154 | mpbir3and 1213 |
. 2
       |
156 | 155, 128 | jca 541 |
1
             |