Step | Hyp | Ref
| Expression |
1 | | xrltnr 9779 |
. . . . 5

  |
2 | 1 | adantl 277 |
. . . 4
    |
3 | | xrlttr 9795 |
. . . . 5
    
    |
4 | 3 | adantl 277 |
. . . 4
 
   

   |
5 | 2, 4 | ispod 4305 |
. . 3
  |
6 | 5 | mptru 1362 |
. 2
 |
7 | | elxr 9776 |
. . . . 5

    |
8 | | elxr 9776 |
. . . . . . . . . 10

    |
9 | | elxr 9776 |
. . . . . . . . . . . . . 14

    |
10 | | simplr 528 |
. . . . . . . . . . . . . . . 16
       |
11 | | simpll 527 |
. . . . . . . . . . . . . . . 16
       |
12 | | simpr 110 |
. . . . . . . . . . . . . . . 16
       |
13 | | axltwlin 8025 |
. . . . . . . . . . . . . . . 16
 
 
     |
14 | 10, 11, 12, 13 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
     
     |
15 | | ltpnf 9780 |
. . . . . . . . . . . . . . . . . . 19
   |
16 | 15 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . 18
       |
17 | | breq2 4008 |
. . . . . . . . . . . . . . . . . . 19
 
   |
18 | 17 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
     
   |
19 | 16, 18 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
       |
20 | 19 | orcd 733 |
. . . . . . . . . . . . . . . 16
         |
21 | 20 | a1d 22 |
. . . . . . . . . . . . . . 15
     
     |
22 | | mnflt 9783 |
. . . . . . . . . . . . . . . . . . 19
   |
23 | 22 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
    
  |
24 | | breq1 4007 |
. . . . . . . . . . . . . . . . . . 19
 
   |
25 | 24 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
     
   |
26 | 23, 25 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
       |
27 | 26 | olcd 734 |
. . . . . . . . . . . . . . . 16
         |
28 | 27 | a1d 22 |
. . . . . . . . . . . . . . 15
     
     |
29 | 14, 21, 28 | 3jaodan 1306 |
. . . . . . . . . . . . . 14
        
    |
30 | 9, 29 | sylan2b 287 |
. . . . . . . . . . . . 13
     
     |
31 | 30 | anasss 399 |
. . . . . . . . . . . 12
  
 

     |
32 | 31 | ancoms 268 |
. . . . . . . . . . 11
   
 
     |
33 | | ltpnf 9780 |
. . . . . . . . . . . . . . . . . . 19
   |
34 | 33 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
       |
35 | | breq2 4008 |
. . . . . . . . . . . . . . . . . . 19
 
   |
36 | 35 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
         |
37 | 34, 36 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
       |
38 | 37 | olcd 734 |
. . . . . . . . . . . . . . . 16
         |
39 | 38 | a1d 22 |
. . . . . . . . . . . . . . 15
     
     |
40 | 15 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . 18
       |
41 | 17 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
     
   |
42 | 40, 41 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
       |
43 | 42 | orcd 733 |
. . . . . . . . . . . . . . . 16
         |
44 | 43 | a1d 22 |
. . . . . . . . . . . . . . 15
     
     |
45 | | mnfltpnf 9785 |
. . . . . . . . . . . . . . . . . . 19
 |
46 | | breq12 4009 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
47 | 46 | ancoms 268 |
. . . . . . . . . . . . . . . . . . 19
 
     |
48 | 45, 47 | mpbiri 168 |
. . . . . . . . . . . . . . . . . 18
 
   |
49 | 48 | adantlr 477 |
. . . . . . . . . . . . . . . . 17
       |
50 | 49 | olcd 734 |
. . . . . . . . . . . . . . . 16
         |
51 | 50 | a1d 22 |
. . . . . . . . . . . . . . 15
     
     |
52 | 39, 44, 51 | 3jaodan 1306 |
. . . . . . . . . . . . . 14
        
    |
53 | 9, 52 | sylan2b 287 |
. . . . . . . . . . . . 13
     
     |
54 | 53 | anasss 399 |
. . . . . . . . . . . 12
  
 

     |
55 | 54 | ancoms 268 |
. . . . . . . . . . 11
   
 
     |
56 | | rexr 8003 |
. . . . . . . . . . . . . . 15
   |
57 | | nltmnf 9788 |
. . . . . . . . . . . . . . 15

  |
58 | 56, 57 | syl 14 |
. . . . . . . . . . . . . 14
   |
59 | 58 | ad2antrr 488 |
. . . . . . . . . . . . 13
   

  |
60 | | breq2 4008 |
. . . . . . . . . . . . . 14
 
   |
61 | 60 | adantl 277 |
. . . . . . . . . . . . 13
   
 
   |
62 | 59, 61 | mtbird 673 |
. . . . . . . . . . . 12
   

  |
63 | 62 | pm2.21d 619 |
. . . . . . . . . . 11
   
 
     |
64 | 32, 55, 63 | 3jaodan 1306 |
. . . . . . . . . 10
    
  
     |
65 | 8, 64 | sylan2b 287 |
. . . . . . . . 9
   
  
    |
66 | 65 | anasss 399 |
. . . . . . . 8
    

     |
67 | 66 | ancoms 268 |
. . . . . . 7
   
 
     |
68 | | pnfnlt 9787 |
. . . . . . . . . 10

  |
69 | 68 | ad2antlr 489 |
. . . . . . . . 9
   

  |
70 | | breq1 4007 |
. . . . . . . . . 10
 
   |
71 | 70 | adantl 277 |
. . . . . . . . 9
   
 
   |
72 | 69, 71 | mtbird 673 |
. . . . . . . 8
   

  |
73 | 72 | pm2.21d 619 |
. . . . . . 7
   
 
     |
74 | | df-3or 979 |
. . . . . . . . . . 11
 

 

   |
75 | 9, 74 | bitri 184 |
. . . . . . . . . 10

      |
76 | | mnfltxr 9786 |
. . . . . . . . . . . . . . 15
 

  |
77 | 76 | adantl 277 |
. . . . . . . . . . . . . 14
  
    |
78 | | breq1 4007 |
. . . . . . . . . . . . . . 15
 
   |
79 | 78 | adantr 276 |
. . . . . . . . . . . . . 14
  
  
   |
80 | 77, 79 | mpbird 167 |
. . . . . . . . . . . . 13
  
    |
81 | 80 | orcd 733 |
. . . . . . . . . . . 12
  
  
   |
82 | 81 | a1d 22 |
. . . . . . . . . . 11
  
  
     |
83 | | eqtr3 2197 |
. . . . . . . . . . . . 13
 
   |
84 | 83 | breq1d 4014 |
. . . . . . . . . . . 12
 
     |
85 | | olc 711 |
. . . . . . . . . . . 12
 
   |
86 | 84, 85 | syl6bi 163 |
. . . . . . . . . . 11
 
  
    |
87 | 82, 86 | jaodan 797 |
. . . . . . . . . 10
        
    |
88 | 75, 87 | sylan2b 287 |
. . . . . . . . 9
 
  
    |
89 | 88 | ancoms 268 |
. . . . . . . 8
   
     |
90 | 89 | adantlr 477 |
. . . . . . 7
   
 
     |
91 | 67, 73, 90 | 3jaodan 1306 |
. . . . . 6
    
  
     |
92 | 91 | 3impa 1194 |
. . . . 5
      
    |
93 | 7, 92 | syl3an3b 1276 |
. . . 4
   
     |
94 | 93 | 3com13 1208 |
. . 3
   
     |
95 | 94 | rgen3 2564 |
. 2
   

   |
96 | | df-iso 4298 |
. 2
   
      |
97 | 6, 95, 96 | mpbir2an 942 |
1
 |