Step | Hyp | Ref
| Expression |
1 | | ivth.7 |
. . 3
       |
2 | | ivth.5 |
. . . 4
   ![[,] [,]](_icc.gif) 
  |
3 | | ivthinclemlopn.q |
. . . . . 6
   |
4 | | fveq2 5517 |
. . . . . . . 8
           |
5 | 4 | breq1d 4015 |
. . . . . . 7
     
       |
6 | | ivthinclem.l |
. . . . . . 7
   ![[,] [,]](_icc.gif)        |
7 | 5, 6 | elrab2 2898 |
. . . . . 6

   ![[,] [,]](_icc.gif) 
       |
8 | 3, 7 | sylib 122 |
. . . . 5
    ![[,] [,]](_icc.gif)         |
9 | 8 | simpld 112 |
. . . 4
   ![[,] [,]](_icc.gif)    |
10 | 2, 9 | sseldd 3158 |
. . 3
   |
11 | | ivth.3 |
. . . . 5
   |
12 | | fveq2 5517 |
. . . . . . 7
           |
13 | 12 | eleq1d 2246 |
. . . . . 6
     
       |
14 | | ivth.8 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)  
      |
15 | 14 | ralrimiva 2550 |
. . . . . 6
    ![[,] [,]](_icc.gif)         |
16 | 13, 15, 9 | rspcdva 2848 |
. . . . 5
       |
17 | 11, 16 | resubcld 8340 |
. . . 4
         |
18 | 8 | simprd 114 |
. . . . 5
    
  |
19 | 16, 11 | posdifd 8491 |
. . . . 5
               |
20 | 18, 19 | mpbid 147 |
. . . 4
         |
21 | 17, 20 | elrpd 9695 |
. . 3
         |
22 | | cncfi 14104 |
. . 3
     

     
                                |
23 | 1, 10, 21, 22 | syl3anc 1238 |
. 2
                                 |
24 | | ivth.1 |
. . . . . . . . . 10
   |
25 | | ivth.2 |
. . . . . . . . . 10
   |
26 | | elicc2 9940 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif)  
    |
27 | 24, 25, 26 | syl2anc 411 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)  
    |
28 | 9, 27 | mpbid 147 |
. . . . . . . 8
 
   |
29 | 28 | simp1d 1009 |
. . . . . . 7
   |
30 | 29 | adantr 276 |
. . . . . 6
 
 
      
              
          |
31 | | simprl 529 |
. . . . . . . 8
 
 
      
              
          |
32 | 31 | rphalfcld 9711 |
. . . . . . 7
 
 
      
              
            |
33 | 32 | rpred 9698 |
. . . . . 6
 
 
      
              
            |
34 | 30, 33 | readdcld 7989 |
. . . . 5
 
 
      
              
        
     |
35 | 24 | adantr 276 |
. . . . . 6
 
 
      
              
          |
36 | 28 | simp2d 1010 |
. . . . . . 7

  |
37 | 36 | adantr 276 |
. . . . . 6
 
 
      
              
          |
38 | 30, 32 | ltaddrpd 9732 |
. . . . . . 7
 
 
      
              
              |
39 | 30, 34, 38 | ltled 8078 |
. . . . . 6
 
 
      
              
              |
40 | 35, 30, 34, 37, 39 | letrd 8083 |
. . . . 5
 
 
      
              
              |
41 | 25 | adantr 276 |
. . . . . 6
 
 
      
              
          |
42 | 31 | rpred 9698 |
. . . . . . . 8
 
 
      
              
          |
43 | 30, 42 | readdcld 7989 |
. . . . . . 7
 
 
      
              
        
   |
44 | | rphalflt 9685 |
. . . . . . . . 9

    |
45 | 31, 44 | syl 14 |
. . . . . . . 8
 
 
      
              
            |
46 | 33, 42, 30, 45 | ltadd2dd 8381 |
. . . . . . 7
 
 
      
              
        
       |
47 | 29 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
    
                                   |
48 | 31 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
    
                                   |
49 | 48 | rpred 9698 |
. . . . . . . . . . . . . . . . 17
    
                                   |
50 | 47, 49 | resubcld 8340 |
. . . . . . . . . . . . . . . 16
    
                                 
   |
51 | 25 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
    
                                   |
52 | 47, 48 | ltsubrpd 9731 |
. . . . . . . . . . . . . . . 16
    
                                 
   |
53 | 28 | simp3d 1011 |
. . . . . . . . . . . . . . . . 17

  |
54 | 53 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
    
                                   |
55 | 50, 47, 51, 52, 54 | ltletrd 8382 |
. . . . . . . . . . . . . . 15
    
                                 
   |
56 | | simpr 110 |
. . . . . . . . . . . . . . 15
    
                                     |
57 | 51, 47, 49 | absdifltd 11189 |
. . . . . . . . . . . . . . 15
    
                                     
 
 
       |
58 | 55, 56, 57 | mpbir2and 944 |
. . . . . . . . . . . . . 14
    
                                         |
59 | | fvoveq1 5900 |
. . . . . . . . . . . . . . . . 17
          
    |
60 | 59 | breq1d 4015 |
. . . . . . . . . . . . . . . 16
       
         |
61 | 60 | imbrov2fvoveq 5902 |
. . . . . . . . . . . . . . 15
                                  
 
                        |
62 | | simplrr 536 |
. . . . . . . . . . . . . . 15
    
                                 
      
              
        |
63 | 24 | rexrd 8009 |
. . . . . . . . . . . . . . . . . 18
   |
64 | 25 | rexrd 8009 |
. . . . . . . . . . . . . . . . . 18
   |
65 | | ivth.4 |
. . . . . . . . . . . . . . . . . . 19
   |
66 | 24, 25, 65 | ltled 8078 |
. . . . . . . . . . . . . . . . . 18

  |
67 | | ubicc2 9987 |
. . . . . . . . . . . . . . . . . 18
     ![[,] [,]](_icc.gif)    |
68 | 63, 64, 66, 67 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)    |
69 | 2, 68 | sseldd 3158 |
. . . . . . . . . . . . . . . 16
   |
70 | 69 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
    
                                   |
71 | 61, 62, 70 | rspcdva 2848 |
. . . . . . . . . . . . . 14
    
                                     
 
                       |
72 | 58, 71 | mpd 13 |
. . . . . . . . . . . . 13
    
                                               
       |
73 | | fveq2 5517 |
. . . . . . . . . . . . . . . . 17
           |
74 | 73 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
     
       |
75 | 15 | adantr 276 |
. . . . . . . . . . . . . . . 16
 
 
      
              
           ![[,] [,]](_icc.gif)         |
76 | 68 | adantr 276 |
. . . . . . . . . . . . . . . 16
 
 
      
              
          ![[,] [,]](_icc.gif)    |
77 | 74, 75, 76 | rspcdva 2848 |
. . . . . . . . . . . . . . 15
 
 
      
              
              |
78 | 77 | adantr 276 |
. . . . . . . . . . . . . 14
    
                                       |
79 | 16 | ad2antrr 488 |
. . . . . . . . . . . . . 14
    
                                       |
80 | 17 | ad2antrr 488 |
. . . . . . . . . . . . . 14
    
                                 
       |
81 | 78, 79, 80 | absdifltd 11189 |
. . . . . . . . . . . . 13
    
                                                     
                                     |
82 | 72, 81 | mpbid 147 |
. . . . . . . . . . . 12
    
                                       
                             |
83 | 82 | simprd 114 |
. . . . . . . . . . 11
    
                                                   |
84 | 79 | recnd 7988 |
. . . . . . . . . . . 12
    
                                       |
85 | 11 | recnd 7988 |
. . . . . . . . . . . . 13
   |
86 | 85 | ad2antrr 488 |
. . . . . . . . . . . 12
    
                                   |
87 | 84, 86 | pncan3d 8273 |
. . . . . . . . . . 11
    
                                               |
88 | 83, 87 | breqtrd 4031 |
. . . . . . . . . 10
    
                                       |
89 | | ivth.9 |
. . . . . . . . . . . 12
     
       |
90 | 89 | simprd 114 |
. . . . . . . . . . 11
       |
91 | 90 | ad2antrr 488 |
. . . . . . . . . 10
    
                                       |
92 | 88, 91 | jca 306 |
. . . . . . . . 9
    
                                     
       |
93 | 11 | ad2antrr 488 |
. . . . . . . . . 10
    
                                   |
94 | | ltnsym2 8050 |
. . . . . . . . . 10
     
     
       |
95 | 78, 93, 94 | syl2anc 411 |
. . . . . . . . 9
    
                                     
       |
96 | 92, 95 | pm2.65da 661 |
. . . . . . . 8
 
 
      
              
            |
97 | 43, 41, 96 | nltled 8080 |
. . . . . . 7
 
 
      
              
        
   |
98 | 34, 43, 41, 46, 97 | ltletrd 8382 |
. . . . . 6
 
 
      
              
        
     |
99 | 34, 41, 98 | ltled 8078 |
. . . . 5
 
 
      
              
        
     |
100 | | elicc2 9940 |
. . . . . 6
 
        ![[,] [,]](_icc.gif)      
    
  
    |
101 | 35, 41, 100 | syl2anc 411 |
. . . . 5
 
 
      
              
               ![[,] [,]](_icc.gif) 
 
               |
102 | 34, 40, 99, 101 | mpbir3and 1180 |
. . . 4
 
 
      
              
        
     ![[,] [,]](_icc.gif)    |
103 | 16 | adantr 276 |
. . . . . . 7
 
 
      
              
              |
104 | | fveq2 5517 |
. . . . . . . . 9
            
      |
105 | 104 | eleq1d 2246 |
. . . . . . . 8
         
           |
106 | 105, 75, 102 | rspcdva 2848 |
. . . . . . 7
 
 
      
              
                  |
107 | | breq2 4009 |
. . . . . . . . . . 11
     
       |
108 | | fveq2 5517 |
. . . . . . . . . . . 12
            
      |
109 | 108 | breq2d 4017 |
. . . . . . . . . . 11
         
   
               |
110 | 107, 109 | imbi12d 234 |
. . . . . . . . . 10
          
    
    
                |
111 | | breq1 4008 |
. . . . . . . . . . . . . 14
 
   |
112 | 12 | breq1d 4015 |
. . . . . . . . . . . . . 14
     
   
           |
113 | 111, 112 | imbi12d 234 |
. . . . . . . . . . . . 13
      
    

            |
114 | 113 | ralbidv 2477 |
. . . . . . . . . . . 12
  
  ![[,] [,]](_icc.gif)       
    
   ![[,] [,]](_icc.gif)   
            |
115 | | ivthinc.i |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)              |
116 | 115 | expr 375 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   
           |
117 | 116 | ralrimiva 2550 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)   
           |
118 | 117 | ralrimiva 2550 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       
       |
119 | 114, 118,
9 | rspcdva 2848 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)       
       |
120 | 119 | adantr 276 |
. . . . . . . . . 10
 
 
      
              
           ![[,] [,]](_icc.gif)   
           |
121 | 110, 120,
102 | rspcdva 2848 |
. . . . . . . . 9
 
 
      
              
                    
       |
122 | 38, 121 | mpd 13 |
. . . . . . . 8
 
 
      
              
               
      |
123 | 103, 106,
122 | ltled 8078 |
. . . . . . 7
 
 
      
              
               
      |
124 | 103, 106,
123 | abssubge0d 11187 |
. . . . . 6
 
 
      
              
                              
           |
125 | 30 | recnd 7988 |
. . . . . . . . . . 11
 
 
      
              
          |
126 | 33 | recnd 7988 |
. . . . . . . . . . 11
 
 
      
              
            |
127 | 125, 126 | pncan2d 8272 |
. . . . . . . . . 10
 
 
      
              
                  |
128 | 127 | fveq2d 5521 |
. . . . . . . . 9
 
 
      
              
                          |
129 | 32 | rpge0d 9702 |
. . . . . . . . . 10
 
 
      
              
            |
130 | 33, 129 | absidd 11178 |
. . . . . . . . 9
 
 
      
              
                  |
131 | 128, 130 | eqtrd 2210 |
. . . . . . . 8
 
 
      
              
                      |
132 | 131, 45 | eqbrtrd 4027 |
. . . . . . 7
 
 
      
              
                    |
133 | | fvoveq1 5900 |
. . . . . . . . . 10
                       |
134 | 133 | breq1d 4015 |
. . . . . . . . 9
           
             |
135 | 134 | imbrov2fvoveq 5902 |
. . . . . . . 8
                                                    
                    |
136 | | simprr 531 |
. . . . . . . 8
 
 
      
              
        
      
              
        |
137 | 2 | adantr 276 |
. . . . . . . . 9
 
 
      
              
          ![[,] [,]](_icc.gif)    |
138 | 137, 102 | sseldd 3158 |
. . . . . . . 8
 
 
      
              
        
     |
139 | 135, 136,
138 | rspcdva 2848 |
. . . . . . 7
 
 
      
              
                          
                   |
140 | 132, 139 | mpd 13 |
. . . . . 6
 
 
      
              
                          
       |
141 | 124, 140 | eqbrtrrd 4029 |
. . . . 5
 
 
      
              
            
                 |
142 | 11 | adantr 276 |
. . . . . 6
 
 
      
              
          |
143 | 106, 142,
103 | ltsub1d 8513 |
. . . . 5
 
 
      
              
            
   
                       |
144 | 141, 143 | mpbird 167 |
. . . 4
 
 
      
              
                  |
145 | | fveq2 5517 |
. . . . . 6
            
      |
146 | 145 | breq1d 4015 |
. . . . 5
         
           |
147 | 146, 6 | elrab2 2898 |
. . . 4
    
 
     ![[,] [,]](_icc.gif)             |
148 | 102, 144,
147 | sylanbrc 417 |
. . 3
 
 
      
              
        
     |
149 | | breq2 4009 |
. . . 4
     
       |
150 | 149 | rspcev 2843 |
. . 3
           
  |
151 | 148, 38, 150 | syl2anc 411 |
. 2
 
 
      
              
        
  |
152 | 23, 151 | rexlimddv 2599 |
1
    |