Step | Hyp | Ref
| Expression |
1 | | fzfid 12186 |
. . . . . 6
 
                 
                       |
2 | | ioossre 11696 |
. . . . . . . . . . . . . 14
    |
3 | | pntpbnd1.y |
. . . . . . . . . . . . . 14
      |
4 | 2, 3 | sseldi 3430 |
. . . . . . . . . . . . 13
   |
5 | | 0red 9644 |
. . . . . . . . . . . . . 14
   |
6 | | pntpbnd1.x |
. . . . . . . . . . . . . . . 16
       |
7 | | 2re 10679 |
. . . . . . . . . . . . . . . . . 18
 |
8 | | ioossre 11696 |
. . . . . . . . . . . . . . . . . . . 20
     |
9 | | pntpbnd1.e |
. . . . . . . . . . . . . . . . . . . 20
       |
10 | 8, 9 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . 19
   |
11 | | eliooord 11694 |
. . . . . . . . . . . . . . . . . . . . 21
     
   |
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
13 | 12 | simpld 461 |
. . . . . . . . . . . . . . . . . . 19
   |
14 | 10, 13 | elrpd 11338 |
. . . . . . . . . . . . . . . . . 18
   |
15 | | rerpdivcl 11330 |
. . . . . . . . . . . . . . . . . 18
 
     |
16 | 7, 14, 15 | sylancr 669 |
. . . . . . . . . . . . . . . . 17
     |
17 | 16 | reefcld 14142 |
. . . . . . . . . . . . . . . 16
         |
18 | 6, 17 | syl5eqel 2533 |
. . . . . . . . . . . . . . 15
   |
19 | | efgt0 14157 |
. . . . . . . . . . . . . . . . 17
           |
20 | 16, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
         |
21 | 20, 6 | syl6breqr 4443 |
. . . . . . . . . . . . . . 15
   |
22 | | eliooord 11694 |
. . . . . . . . . . . . . . . . 17
   
    |
23 | 3, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
 
   |
24 | 23 | simpld 461 |
. . . . . . . . . . . . . . 15
   |
25 | 5, 18, 4, 21, 24 | lttrd 9796 |
. . . . . . . . . . . . . 14
   |
26 | 5, 4, 25 | ltled 9783 |
. . . . . . . . . . . . 13

  |
27 | | flge0nn0 12054 |
. . . . . . . . . . . . 13
         |
28 | 4, 26, 27 | syl2anc 667 |
. . . . . . . . . . . 12
       |
29 | | nn0p1nn 10909 |
. . . . . . . . . . . 12
    
        |
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
         |
31 | | elfzuz 11796 |
. . . . . . . . . . 11
             
               |
32 | | eluznn 11229 |
. . . . . . . . . . 11
       
          
  |
33 | 30, 31, 32 | syl2an 480 |
. . . . . . . . . 10
 
                
  |
34 | 33 | nnrpd 11339 |
. . . . . . . . 9
 
                
  |
35 | | pntpbnd.r |
. . . . . . . . . . 11
  ψ     |
36 | 35 | pntrf 24401 |
. . . . . . . . . 10
     |
37 | 36 | ffvelrni 6021 |
. . . . . . . . 9

      |
38 | 34, 37 | syl 17 |
. . . . . . . 8
 
                
      |
39 | 33 | peano2nnd 10626 |
. . . . . . . . 9
 
                
    |
40 | 33, 39 | nnmulcld 10657 |
. . . . . . . 8
 
                
      |
41 | 38, 40 | nndivred 10658 |
. . . . . . 7
 
                
            |
42 | 41 | adantlr 721 |
. . . . . 6
   
            
        
            
                |
43 | 1, 42 | fsumrecl 13800 |
. . . . 5
 
                 
                  
                |
44 | 38 | adantlr 721 |
. . . . . . 7
   
            
        
            
          |
45 | | fveq2 5865 |
. . . . . . . . . 10
           |
46 | 45 | breq2d 4414 |
. . . . . . . . 9
 
   
       |
47 | 46 | rspccva 3149 |
. . . . . . . 8
                   
                    
      |
48 | 47 | adantll 720 |
. . . . . . 7
   
            
        
            
          |
49 | 40 | adantlr 721 |
. . . . . . . 8
   
            
        
            
          |
50 | 49 | nnred 10624 |
. . . . . . 7
   
            
        
            
          |
51 | 49 | nngt0d 10653 |
. . . . . . 7
   
            
        
            
          |
52 | | divge0 10474 |
. . . . . . 7
      
               
            |
53 | 44, 48, 50, 51, 52 | syl22anc 1269 |
. . . . . 6
   
            
        
            
                |
54 | 1, 42, 53 | fsumge0 13855 |
. . . . 5
 
                 
    
                              |
55 | 43, 54 | absidd 13484 |
. . . 4
 
                 
                     
                                             |
56 | 42, 53 | absidd 13484 |
. . . . 5
   
            
        
            
                              |
57 | 56 | sumeq2dv 13769 |
. . . 4
 
                 
                  
                                                |
58 | 55, 57 | eqtr4d 2488 |
. . 3
 
                 
                     
                                                 |
59 | | fzfid 12186 |
. . . . 5
 
                     
             
     |
60 | 41 | adantlr 721 |
. . . . . 6
   
            
        
            
                |
61 | 60 | recnd 9669 |
. . . . 5
   
            
        
            
                |
62 | 59, 61 | fsumneg 13848 |
. . . 4
 
                     
                                            
                |
63 | 38 | adantlr 721 |
. . . . . . . . . 10
   
            
        
            
          |
64 | 63 | renegcld 10046 |
. . . . . . . . 9
   
            
        
            
           |
65 | 45 | breq1d 4412 |
. . . . . . . . . . . 12
     
       |
66 | 65 | rspccva 3149 |
. . . . . . . . . . 11
                       
            
          |
67 | 66 | adantll 720 |
. . . . . . . . . 10
   
            
        
            
          |
68 | 63 | le0neg1d 10185 |
. . . . . . . . . 10
   
            
        
            
                 |
69 | 67, 68 | mpbid 214 |
. . . . . . . . 9
   
            
        
            
           |
70 | 40 | adantlr 721 |
. . . . . . . . . 10
   
            
        
            
          |
71 | 70 | nnred 10624 |
. . . . . . . . 9
   
            
        
            
          |
72 | 70 | nngt0d 10653 |
. . . . . . . . 9
   
            
        
            
          |
73 | | divge0 10474 |
. . . . . . . . 9
                                      |
74 | 64, 69, 71, 72, 73 | syl22anc 1269 |
. . . . . . . 8
   
            
        
            
                 |
75 | 38 | recnd 9669 |
. . . . . . . . . 10
 
                
      |
76 | 40 | nncnd 10625 |
. . . . . . . . . 10
 
                
      |
77 | 40 | nnne0d 10654 |
. . . . . . . . . 10
 
                
      |
78 | 75, 76, 77 | divnegd 10396 |
. . . . . . . . 9
 
                
                        |
79 | 78 | adantlr 721 |
. . . . . . . 8
   
            
        
            
                            |
80 | 74, 79 | breqtrrd 4429 |
. . . . . . 7
   
            
        
            
                 |
81 | 60 | le0neg1d 10185 |
. . . . . . 7
   
            
        
            
                             |
82 | 80, 81 | mpbird 236 |
. . . . . 6
   
            
        
            
                |
83 | 60, 82 | absnidd 13475 |
. . . . 5
   
            
        
            
                               |
84 | 83 | sumeq2dv 13769 |
. . . 4
 
                     
                                                                |
85 | 59, 60 | fsumrecl 13800 |
. . . . 5
 
                     
                               |
86 | 60 | renegcld 10046 |
. . . . . . . 8
   
            
        
            
                 |
87 | 59, 86, 80 | fsumge0 13855 |
. . . . . . 7
 
                     
                                |
88 | 87, 62 | breqtrd 4427 |
. . . . . 6
 
                     
                                |
89 | 85 | le0neg1d 10185 |
. . . . . 6
 
                     
                             
              
                 |
90 | 88, 89 | mpbird 236 |
. . . . 5
 
                     
                            
  |
91 | 85, 90 | absnidd 13475 |
. . . 4
 
                     
                 
                                              |
92 | 62, 84, 91 | 3eqtr4rd 2496 |
. . 3
 
                     
                 
                                                 |
93 | | pntpbnd1.c |
. . . . . . . . . . . . 13
   |
94 | | pntpbnd1.1 |
. . . . . . . . . . . . . 14
   |
95 | | 2rp 11307 |
. . . . . . . . . . . . . 14
 |
96 | | rpaddcl 11323 |
. . . . . . . . . . . . . 14
   
   |
97 | 94, 95, 96 | sylancl 668 |
. . . . . . . . . . . . 13
     |
98 | 93, 97 | syl5eqel 2533 |
. . . . . . . . . . . 12
   |
99 | 98, 14 | rpdivcld 11358 |
. . . . . . . . . . 11
     |
100 | 99 | rpred 11341 |
. . . . . . . . . 10
     |
101 | 100 | reefcld 14142 |
. . . . . . . . 9
         |
102 | | pnfxr 11412 |
. . . . . . . . 9
 |
103 | | icossre 11715 |
. . . . . . . . 9
                    |
104 | 101, 102,
103 | sylancl 668 |
. . . . . . . 8
            |
105 | | pntpbnd1.k |
. . . . . . . 8
            |
106 | 104, 105 | sseldd 3433 |
. . . . . . 7
   |
107 | 106, 4 | remulcld 9671 |
. . . . . 6
     |
108 | 4 | recnd 9669 |
. . . . . . . . 9
   |
109 | 108 | mulid2d 9661 |
. . . . . . . 8
     |
110 | | 1red 9658 |
. . . . . . . . . 10
   |
111 | | efgt1 14170 |
. . . . . . . . . . 11
  
        |
112 | 99, 111 | syl 17 |
. . . . . . . . . 10
         |
113 | | elicopnf 11730 |
. . . . . . . . . . . . 13
       
        
           |
114 | 101, 113 | syl 17 |
. . . . . . . . . . . 12
          
           |
115 | 114 | simplbda 630 |
. . . . . . . . . . 11
 
                  |
116 | 105, 115 | mpdan 674 |
. . . . . . . . . 10
         |
117 | 110, 101,
106, 112, 116 | ltletrd 9795 |
. . . . . . . . 9
   |
118 | | ltmul1 10455 |
. . . . . . . . . 10
 

          |
119 | 110, 106,
4, 25, 118 | syl112anc 1272 |
. . . . . . . . 9
         |
120 | 117, 119 | mpbid 214 |
. . . . . . . 8
  
    |
121 | 109, 120 | eqbrtrrd 4425 |
. . . . . . 7
     |
122 | 4, 107, 121 | ltled 9783 |
. . . . . 6

    |
123 | | flword2 12048 |
. . . . . 6
  
       
            |
124 | 4, 107, 122, 123 | syl3anc 1268 |
. . . . 5
    
            |
125 | 107 | flcld 12034 |
. . . . . 6
    
    |
126 | | uzid 11173 |
. . . . . 6
                         |
127 | 125, 126 | syl 17 |
. . . . 5
    
              |
128 | | elfzuzb 11794 |
. . . . 5
                 
  
                                  |
129 | 124, 127,
128 | sylanbrc 670 |
. . . 4
    
            
     |
130 | | oveq2 6298 |
. . . . . . . 8
                               |
131 | 130 | raleqdv 2993 |
. . . . . . 7
      
          
   
               
       |
132 | 130 | raleqdv 2993 |
. . . . . . 7
      
              
                   
   |
133 | 131, 132 | orbi12d 716 |
. . . . . 6
                                      
                 
    
                       |
134 | 133 | imbi2d 318 |
. . . . 5
      
 
               
                 
 
                   
                        |
135 | | oveq2 6298 |
. . . . . . . 8
                       |
136 | 135 | raleqdv 2993 |
. . . . . . 7
  
          
   
                   |
137 | 135 | raleqdv 2993 |
. . . . . . 7
  
              
                   |
138 | 136, 137 | orbi12d 716 |
. . . . . 6
                                  
                                 
    |
139 | 138 | imbi2d 318 |
. . . . 5
  
 
               
                 
 
               
                    |
140 | | oveq2 6298 |
. . . . . . . 8
                           |
141 | 140 | raleqdv 2993 |
. . . . . . 7
    
          
   
                     |
142 | 140 | raleqdv 2993 |
. . . . . . 7
    
              
                     |
143 | 141, 142 | orbi12d 716 |
. . . . . 6
                                    
                                     
    |
144 | 143 | imbi2d 318 |
. . . . 5
    
 
               
                 
 
                 
                      |
145 | | oveq2 6298 |
. . . . . . . 8
    
                        
     |
146 | 145 | raleqdv 2993 |
. . . . . . 7
    
   
          
   
                 
       |
147 | 145 | raleqdv 2993 |
. . . . . . 7
    
   
              
                     
   |
148 | 146, 147 | orbi12d 716 |
. . . . . 6
    
                                   
                   
    
            
            |
149 | 148 | imbi2d 318 |
. . . . 5
    
   
 
               
                 
 
            
        
            
             |
150 | | elfzle3 11805 |
. . . . . . . . 9
                           |
151 | | elfzel2 11798 |
. . . . . . . . . . . 12
                     |
152 | 151 | zred 11040 |
. . . . . . . . . . 11
                     |
153 | 152 | ltp1d 10537 |
. . . . . . . . . 10
                           |
154 | | peano2re 9806 |
. . . . . . . . . . . 12
             |
155 | 152, 154 | syl 17 |
. . . . . . . . . . 11
                       |
156 | 152, 155 | ltnled 9782 |
. . . . . . . . . 10
                   
     
             |
157 | 153, 156 | mpbid 214 |
. . . . . . . . 9
                    
      |
158 | 150, 157 | pm2.21dd 178 |
. . . . . . . 8
                     |
159 | 158 | rgen 2747 |
. . . . . . 7
                   
 |
160 | 159 | olci 393 |
. . . . . 6
 
                   
                     |
161 | 160 | 2a1i 12 |
. . . . 5
                                
    
                       |
162 | | elfzofz 11935 |
. . . . . . . . . 10
      ..^      
                |
163 | | elfzp12 11873 |
. . . . . . . . . . 11
                                                       |
164 | 124, 163 | syl 17 |
. . . . . . . . . 10
            
  
                         |
165 | 162, 164 | syl5ib 223 |
. . . . . . . . 9
       ..^   
                            |
166 | 165 | imp 431 |
. . . . . . . 8
 
     ..^   
                            |
167 | 30 | nnrpd 11339 |
. . . . . . . . . . . . . 14
         |
168 | 36 | ffvelrni 6021 |
. . . . . . . . . . . . . 14
      
            |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . 13
             |
170 | 5, 169 | letrid 9787 |
. . . . . . . . . . . 12
                     
   |
171 | 170 | adantr 467 |
. . . . . . . . . . 11
 
    
                        |
172 | | oveq1 6297 |
. . . . . . . . . . . . . . . 16
               |
173 | 172 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
                                   |
174 | 4 | flcld 12034 |
. . . . . . . . . . . . . . . . 17
       |
175 | 174 | peano2zd 11043 |
. . . . . . . . . . . . . . . 16
         |
176 | | fzsn 11840 |
. . . . . . . . . . . . . . . 16
                                 |
177 | 175, 176 | syl 17 |
. . . . . . . . . . . . . . 15
                           |
178 | 173, 177 | sylan9eqr 2507 |
. . . . . . . . . . . . . 14
 
    
                      |
179 | 178 | raleqdv 2993 |
. . . . . . . . . . . . 13
 
    
 
                
                 |
180 | | ovex 6318 |
. . . . . . . . . . . . . 14
       |
181 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
                       |
182 | 181 | breq2d 4414 |
. . . . . . . . . . . . . 14
       
   
             |
183 | 180, 182 | ralsn 4010 |
. . . . . . . . . . . . 13
 
                         |
184 | 179, 183 | syl6bb 265 |
. . . . . . . . . . . 12
 
    
 
                
             |
185 | 178 | raleqdv 2993 |
. . . . . . . . . . . . 13
 
    
 
                
                |
186 | 181 | breq1d 4412 |
. . . . . . . . . . . . . 14
           
             |
187 | 180, 186 | ralsn 4010 |
. . . . . . . . . . . . 13
 
                        |
188 | 185, 187 | syl6bb 265 |
. . . . . . . . . . . 12
 
    
 
                
             |
189 | 184, 188 | orbi12d 716 |
. . . . . . . . . . 11
 
    
  
            
    
                 
                         |
190 | 171, 189 | mpbird 236 |
. . . . . . . . . 10
 
    
 
                 
                    |
191 | 190 | a1d 26 |
. . . . . . . . 9
 
    
  
          
    
                                                    
    |
192 | | elfzuz 11796 |
. . . . . . . . . . . . . . . . 17
             
               |
193 | 192 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
                
            |
194 | | eluzfz2 11807 |
. . . . . . . . . . . . . . . 16
          
            |
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . . . 15
 
                
            |
196 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
197 | 196 | breq2d 4414 |
. . . . . . . . . . . . . . . 16
 
   
       |
198 | 197 | rspcv 3146 |
. . . . . . . . . . . . . . 15
            
          
           |
199 | 195, 198 | syl 17 |
. . . . . . . . . . . . . 14
 
                
 
                      |
200 | | pntpbnd1.3 |
. . . . . . . . . . . . . . . . . . 19
                    |
201 | 200 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
                
                   |
202 | | eluznn 11229 |
. . . . . . . . . . . . . . . . . . . . 21
       
          
  |
203 | 30, 192, 202 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . 20
 
                
  |
204 | 203 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
                                            
  |
205 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
           |
206 | 205 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                
        |
207 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
     |
208 | | zltp1le 10986 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
               |
209 | 174, 207,
208 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                
              |
210 | 206, 209 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                
      |
211 | | fllt 12042 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
         |
212 | 4, 207, 211 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                
        |
213 | 210, 212 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . 21
 
                
  |
214 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
      
    |
215 | 214 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                
        |
216 | | flge 12041 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  
    
     |
217 | 107, 207,
216 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                
  
         |
218 | 215, 217 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . 21
 
                
    |
219 | 213, 218 | jca 535 |
. . . . . . . . . . . . . . . . . . . 20
 
                
      |
220 | 219 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
                                             
     |
221 | 9 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
                                            
      |
222 | 3 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
                                            
     |
223 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
                                                    
       
          |
224 | 35, 221, 6, 222, 204, 220, 223 | pntpbnd1a 24423 |
. . . . . . . . . . . . . . . . . . 19
                                                      
  |
225 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
226 | | breq1 4405 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
     |
227 | 225, 226 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . 21
  
   
      |
228 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
229 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
230 | 228, 229 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
231 | 230 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
                       |
232 | 231 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . 21
           
             |
233 | 227, 232 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . 20
   
                                 |
234 | 233 | rspcev 3150 |
. . . . . . . . . . . . . . . . . . 19
   
                                  |
235 | 204, 220,
224, 234 | syl12anc 1266 |
. . . . . . . . . . . . . . . . . 18
                                             
 
                |
236 | 201, 235 | mtand 665 |
. . . . . . . . . . . . . . . . 17
 
                
                          |
237 | 236 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                                   |
238 | 203 | nnrpd 11339 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                
  |
239 | 36 | ffvelrni 6021 |
. . . . . . . . . . . . . . . . . . . . . . 23

      |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                
      |
241 | 240 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
                            
          |
242 | 241 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . 20
                            
          |
243 | 242 | subid1d 9975 |
. . . . . . . . . . . . . . . . . . 19
                            
                |
244 | 203 | peano2nnd 10626 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                
    |
245 | 244 | nnrpd 11339 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                
    |
246 | 36 | ffvelrni 6021 |
. . . . . . . . . . . . . . . . . . . . . 22
  
        |
247 | 245, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
                
        |
248 | 247 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
                            
       
    |
249 | | 0red 9644 |
. . . . . . . . . . . . . . . . . . . 20
                            
      |
250 | | 0re 9643 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
251 | | letric 9734 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   
     |
252 | 250, 247,
251 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                
    
           |
253 | 252 | ord 379 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                
    
           |
254 | 253 | imp 431 |
. . . . . . . . . . . . . . . . . . . . 21
                                   |
255 | 254 | adantrl 722 |
. . . . . . . . . . . . . . . . . . . 20
                            
       
    |
256 | 248, 249,
241, 255 | lesub2dd 10230 |
. . . . . . . . . . . . . . . . . . 19
                            
                        |
257 | 243, 256 | eqbrtrrd 4425 |
. . . . . . . . . . . . . . . . . 18
                            
                      |
258 | | simprl 764 |
. . . . . . . . . . . . . . . . . . 19
                            
          |
259 | 241, 258 | absidd 13484 |
. . . . . . . . . . . . . . . . . 18
                            
                  |
260 | 248, 249,
241, 255, 258 | letrd 9792 |
. . . . . . . . . . . . . . . . . . 19
                            
       
        |
261 | 248, 241,
260 | abssuble0d 13494 |
. . . . . . . . . . . . . . . . . 18
                            
                            
     |
262 | 257, 259,
261 | 3brtr4d 4433 |
. . . . . . . . . . . . . . . . 17
                            
           
       
          |
263 | 262 | expr 620 |
. . . . . . . . . . . . . . . 16
                         
             
       
           |
264 | 237, 263 | mt3d 129 |
. . . . . . . . . . . . . . 15
                                 |
265 | 264 | ex 436 |
. . . . . . . . . . . . . 14
 
                
              |
266 | 199, 265 | syld 45 |
. . . . . . . . . . . . 13
 
                
 
                        |
267 | | ovex 6318 |
. . . . . . . . . . . . . 14
   |
268 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
          
    |
269 | 268 | breq2d 4414 |
. . . . . . . . . . . . . 14
   
   
         |
270 | 267, 269 | ralsn 4010 |
. . . . . . . . . . . . 13
 
            
    |
271 | 266, 270 | syl6ibr 231 |
. . . . . . . . . . . 12
 
                
 
                            |
272 | 271 | ancld 556 |
. . . . . . . . . . 11
 
                
 
                
          
    
             |
273 | | fzsuc 11843 |
. . . . . . . . . . . . . 14
          
                              |
274 | 193, 273 | syl 17 |
. . . . . . . . . . . . 13
 
                
                              |
275 | 274 | raleqdv 2993 |
. . . . . . . . . . . 12
 
                
 
                
                         |
276 | | ralunb 3615 |
. . . . . . . . . . . 12
 
                                 
    
            |
277 | 275, 276 | syl6bb 265 |
. . . . . . . . . . 11
 
                
 
                
 
               
             |
278 | 272, 277 | sylibrd 238 |
. . . . . . . . . 10
 
                
 
                                    |
279 | 196 | breq1d 4412 |
. . . . . . . . . . . . . . . 16
     
       |
280 | 279 | rspcv 3146 |
. . . . . . . . . . . . . . 15
            
              
       |
281 | 195, 280 | syl 17 |
. . . . . . . . . . . . . 14
 
                
 
                      |
282 | 236 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                                   |
283 | 253 | con1d 128 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                
                |
284 | 283 | imp 431 |
. . . . . . . . . . . . . . . . . . . . 21
                          
        |
285 | 284 | adantrl 722 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
286 | 240 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
                                       |
287 | 286 | renegcld 10046 |
. . . . . . . . . . . . . . . . . . . . 21
                                        |
288 | 247 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
                                    
    |
289 | 287, 288 | addge02d 10202 |
. . . . . . . . . . . . . . . . . . . 20
                                                             |
290 | 285, 289 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
                                                     |
291 | 288 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . 20
                                    
    |
292 | 286 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
293 | 291, 292 | negsubd 9992 |
. . . . . . . . . . . . . . . . . . 19
                                                  
         |
294 | 290, 293 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . 18
                                                    |
295 | | simprl 764 |
. . . . . . . . . . . . . . . . . . 19
                                       |
296 | 286, 295 | absnidd 13475 |
. . . . . . . . . . . . . . . . . 18
                                                |
297 | | 0red 9644 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
298 | 286, 297,
288, 295, 285 | letrd 9792 |
. . . . . . . . . . . . . . . . . . 19
                                             |
299 | 286, 288,
298 | abssubge0d 13493 |
. . . . . . . . . . . . . . . . . 18
                                                               |
300 | 294, 296,
299 | 3brtr4d 4433 |
. . . . . . . . . . . . . . . . 17
                                        
       
          |
301 | 300 | expr 620 |
. . . . . . . . . . . . . . . 16
                               
                           |
302 | 282, 301 | mt3d 129 |
. . . . . . . . . . . . . . 15
                                 |
303 | 302 | ex 436 |
. . . . . . . . . . . . . 14
 
                
    
         |
304 | 281, 303 | syld 45 |
. . . . . . . . . . . . 13
 
                
 
                        |
305 | 268 | breq1d 4412 |
. . . . . . . . . . . . . 14
       
         |
306 | 267, 305 | ralsn 4010 |
. . . . . . . . . . . . 13
 
                |
307 | 304, 306 | syl6ibr 231 |
. . . . . . . . . . . 12
 
                
 
                           |
308 | 307 | ancld 556 |
. . . . . . . . . . 11
 
                
 
                
              
             |
309 | 274 | raleqdv 2993 |
. . . . . . . . . . . 12
 
                
 
                
                         |