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

  |
2 | 1 | adantl 262 |
. . . 4
    |
3 | | xrlttr 8486 |
. . . . 5
    
    |
4 | 3 | adantl 262 |
. . . 4
 
   
    |
5 | 2, 4 | ispod 4032 |
. . 3
  |
6 | 5 | trud 1251 |
. 2
 |
7 | | elxr 8466 |
. . . . 5

    |
8 | | elxr 8466 |
. . . . . . . . . 10

    |
9 | | elxr 8466 |
. . . . . . . . . . . . . 14

    |
10 | | simplr 482 |
. . . . . . . . . . . . . . . 16
   
   |
11 | | simpll 481 |
. . . . . . . . . . . . . . . 16
   
   |
12 | | simpr 103 |
. . . . . . . . . . . . . . . 16
   
   |
13 | | axltwlin 6884 |
. . . . . . . . . . . . . . . 16
 
       |
14 | 10, 11, 12, 13 | syl3anc 1134 |
. . . . . . . . . . . . . . 15
   
       |
15 | | ltpnf 8472 |
. . . . . . . . . . . . . . . . . . 19
   |
16 | 15 | ad2antlr 458 |
. . . . . . . . . . . . . . . . . 18
   
   |
17 | | breq2 3759 |
. . . . . . . . . . . . . . . . . . 19
     |
18 | 17 | adantl 262 |
. . . . . . . . . . . . . . . . . 18
   
     |
19 | 16, 18 | mpbird 156 |
. . . . . . . . . . . . . . . . 17
   
   |
20 | 19 | orcd 651 |
. . . . . . . . . . . . . . . 16
   
     |
21 | 20 | a1d 22 |
. . . . . . . . . . . . . . 15
   
       |
22 | | mnflt 8474 |
. . . . . . . . . . . . . . . . . . 19
   |
23 | 22 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . 18
   
   |
24 | | breq1 3758 |
. . . . . . . . . . . . . . . . . . 19
     |
25 | 24 | adantl 262 |
. . . . . . . . . . . . . . . . . 18
   
 
   |
26 | 23, 25 | mpbird 156 |
. . . . . . . . . . . . . . . . 17
   
   |
27 | 26 | olcd 652 |
. . . . . . . . . . . . . . . 16
   
     |
28 | 27 | a1d 22 |
. . . . . . . . . . . . . . 15
   
       |
29 | 14, 21, 28 | 3jaodan 1200 |
. . . . . . . . . . . . . 14
    
 
      |
30 | 9, 29 | sylan2b 271 |
. . . . . . . . . . . . 13
   
  
    |
31 | 30 | anasss 379 |
. . . . . . . . . . . 12
  
        |
32 | 31 | ancoms 255 |
. . . . . . . . . . 11
   
       |
33 | | ltpnf 8472 |
. . . . . . . . . . . . . . . . . . 19
   |
34 | 33 | adantl 262 |
. . . . . . . . . . . . . . . . . 18
   
   |
35 | | breq2 3759 |
. . . . . . . . . . . . . . . . . . 19
     |
36 | 35 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . 18
   
     |
37 | 34, 36 | mpbird 156 |
. . . . . . . . . . . . . . . . 17
   
   |
38 | 37 | olcd 652 |
. . . . . . . . . . . . . . . 16
   
     |
39 | 38 | a1d 22 |
. . . . . . . . . . . . . . 15
   
       |
40 | 15 | ad2antlr 458 |
. . . . . . . . . . . . . . . . . 18
   
   |
41 | 17 | adantl 262 |
. . . . . . . . . . . . . . . . . 18
   
     |
42 | 40, 41 | mpbird 156 |
. . . . . . . . . . . . . . . . 17
   
   |
43 | 42 | orcd 651 |
. . . . . . . . . . . . . . . 16
   
     |
44 | 43 | a1d 22 |
. . . . . . . . . . . . . . 15
   
       |
45 | | mnfltpnf 8476 |
. . . . . . . . . . . . . . . . . . 19
 |
46 | | breq12 3760 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
47 | 46 | ancoms 255 |
. . . . . . . . . . . . . . . . . . 19
 
     |
48 | 45, 47 | mpbiri 157 |
. . . . . . . . . . . . . . . . . 18
 
   |
49 | 48 | adantlr 446 |
. . . . . . . . . . . . . . . . 17
   
   |
50 | 49 | olcd 652 |
. . . . . . . . . . . . . . . 16
   
     |
51 | 50 | a1d 22 |
. . . . . . . . . . . . . . 15
   
       |
52 | 39, 44, 51 | 3jaodan 1200 |
. . . . . . . . . . . . . 14
    
 
      |
53 | 9, 52 | sylan2b 271 |
. . . . . . . . . . . . 13
   
  
    |
54 | 53 | anasss 379 |
. . . . . . . . . . . 12
  
        |
55 | 54 | ancoms 255 |
. . . . . . . . . . 11
   
       |
56 | | rexr 6868 |
. . . . . . . . . . . . . . 15
   |
57 | | nltmnf 8479 |
. . . . . . . . . . . . . . 15

  |
58 | 56, 57 | syl 14 |
. . . . . . . . . . . . . 14
   |
59 | 58 | ad2antrr 457 |
. . . . . . . . . . . . 13
   
   |
60 | | breq2 3759 |
. . . . . . . . . . . . . 14
     |
61 | 60 | adantl 262 |
. . . . . . . . . . . . 13
   
     |
62 | 59, 61 | mtbird 597 |
. . . . . . . . . . . 12
   
   |
63 | 62 | pm2.21d 549 |
. . . . . . . . . . 11
   
       |
64 | 32, 55, 63 | 3jaodan 1200 |
. . . . . . . . . 10
    
 
      |
65 | 8, 64 | sylan2b 271 |
. . . . . . . . 9
   
  
    |
66 | 65 | anasss 379 |
. . . . . . . 8
  
  

    |
67 | 66 | ancoms 255 |
. . . . . . 7
   
       |
68 | | pnfnlt 8478 |
. . . . . . . . . 10

  |
69 | 68 | ad2antlr 458 |
. . . . . . . . 9
   
   |
70 | | breq1 3758 |
. . . . . . . . . 10
     |
71 | 70 | adantl 262 |
. . . . . . . . 9
   
 
   |
72 | 69, 71 | mtbird 597 |
. . . . . . . 8
   
   |
73 | 72 | pm2.21d 549 |
. . . . . . 7
   
       |
74 | | df-3or 885 |
. . . . . . . . . . 11
 
  

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

 

   |
76 | | mnfltxr 8477 |
. . . . . . . . . . . . . . 15
 

  |
77 | 76 | adantl 262 |
. . . . . . . . . . . . . 14
  
 
  |
78 | | breq1 3758 |
. . . . . . . . . . . . . . 15
     |
79 | 78 | adantr 261 |
. . . . . . . . . . . . . 14
  
 
    |
80 | 77, 79 | mpbird 156 |
. . . . . . . . . . . . 13
  
 
  |
81 | 80 | orcd 651 |
. . . . . . . . . . . 12
  
 
    |
82 | 81 | a1d 22 |
. . . . . . . . . . 11
  
 
      |
83 | | eqtr3 2056 |
. . . . . . . . . . . . 13
 
   |
84 | 83 | breq1d 3765 |
. . . . . . . . . . . 12
 
     |
85 | | olc 631 |
. . . . . . . . . . . 12
     |
86 | 84, 85 | syl6bi 152 |
. . . . . . . . . . 11
 
  
    |
87 | 82, 86 | jaodan 709 |
. . . . . . . . . 10
   
  
      |
88 | 75, 87 | sylan2b 271 |
. . . . . . . . 9
 
 

    |
89 | 88 | ancoms 255 |
. . . . . . . 8
         |
90 | 89 | adantlr 446 |
. . . . . . 7
   
       |
91 | 67, 73, 90 | 3jaodan 1200 |
. . . . . 6
    
 
      |
92 | 91 | 3impa 1098 |
. . . . 5
           |
93 | 7, 92 | syl3an3b 1172 |
. . . 4
         |
94 | 93 | 3com13 1108 |
. . 3
         |
95 | 94 | rgen3 2400 |
. 2
   

   |
96 | | df-iso 4025 |
. 2
          |
97 | 6, 95, 96 | mpbir2an 848 |
1
 |