Proof of Theorem xrlttr
Step | Hyp | Ref
| Expression |
1 | | elxr 8466 |
. 2

    |
2 | | elxr 8466 |
. . 3

    |
3 | | elxr 8466 |
. . . . . . . . 9

    |
4 | | lttr 6889 |
. . . . . . . . . . . 12
 
  
    |
5 | 4 | 3expa 1103 |
. . . . . . . . . . 11
   
       |
6 | 5 | an32s 502 |
. . . . . . . . . 10
           |
7 | | rexr 6868 |
. . . . . . . . . . . . . . . 16
   |
8 | | pnfnlt 8478 |
. . . . . . . . . . . . . . . 16

  |
9 | 7, 8 | syl 14 |
. . . . . . . . . . . . . . 15
   |
10 | 9 | adantr 261 |
. . . . . . . . . . . . . 14
 
   |
11 | | breq1 3758 |
. . . . . . . . . . . . . . 15
     |
12 | 11 | adantl 262 |
. . . . . . . . . . . . . 14
 
     |
13 | 10, 12 | mtbird 597 |
. . . . . . . . . . . . 13
 
   |
14 | 13 | pm2.21d 549 |
. . . . . . . . . . . 12
 
     |
15 | 14 | adantll 445 |
. . . . . . . . . . 11
         |
16 | 15 | adantld 263 |
. . . . . . . . . 10
           |
17 | | rexr 6868 |
. . . . . . . . . . . . . . . 16
   |
18 | | nltmnf 8479 |
. . . . . . . . . . . . . . . 16

  |
19 | 17, 18 | syl 14 |
. . . . . . . . . . . . . . 15
   |
20 | 19 | adantr 261 |
. . . . . . . . . . . . . 14
 
   |
21 | | breq2 3759 |
. . . . . . . . . . . . . . 15
     |
22 | 21 | adantl 262 |
. . . . . . . . . . . . . 14
 
     |
23 | 20, 22 | mtbird 597 |
. . . . . . . . . . . . 13
 
   |
24 | 23 | pm2.21d 549 |
. . . . . . . . . . . 12
 
     |
25 | 24 | adantlr 446 |
. . . . . . . . . . 11
         |
26 | 25 | adantrd 264 |
. . . . . . . . . 10
           |
27 | 6, 16, 26 | 3jaodan 1200 |
. . . . . . . . 9
    
        |
28 | 3, 27 | sylan2b 271 |
. . . . . . . 8
           |
29 | 28 | an32s 502 |
. . . . . . 7
   
       |
30 | | ltpnf 8472 |
. . . . . . . . . . 11
   |
31 | 30 | adantr 261 |
. . . . . . . . . 10
 
   |
32 | | breq2 3759 |
. . . . . . . . . . 11
     |
33 | 32 | adantl 262 |
. . . . . . . . . 10
 
     |
34 | 31, 33 | mpbird 156 |
. . . . . . . . 9
 
   |
35 | 34 | adantlr 446 |
. . . . . . . 8
   
   |
36 | 35 | a1d 22 |
. . . . . . 7
   
       |
37 | | nltmnf 8479 |
. . . . . . . . . . . 12

  |
38 | 37 | adantr 261 |
. . . . . . . . . . 11
     |
39 | | breq2 3759 |
. . . . . . . . . . . 12
     |
40 | 39 | adantl 262 |
. . . . . . . . . . 11
       |
41 | 38, 40 | mtbird 597 |
. . . . . . . . . 10
     |
42 | 41 | pm2.21d 549 |
. . . . . . . . 9
       |
43 | 42 | adantld 263 |
. . . . . . . 8
    
    |
44 | 43 | adantll 445 |
. . . . . . 7
   
       |
45 | 29, 36, 44 | 3jaodan 1200 |
. . . . . 6
    
 
 
    |
46 | 45 | anasss 379 |
. . . . 5
  

         |
47 | | pnfnlt 8478 |
. . . . . . . . . 10

  |
48 | 47 | adantl 262 |
. . . . . . . . 9
 

  |
49 | | breq1 3758 |
. . . . . . . . . 10
     |
50 | 49 | adantr 261 |
. . . . . . . . 9
 
 
   |
51 | 48, 50 | mtbird 597 |
. . . . . . . 8
 
   |
52 | 51 | pm2.21d 549 |
. . . . . . 7
 
 
   |
53 | 52 | adantrd 264 |
. . . . . 6
 
       |
54 | 53 | adantrr 448 |
. . . . 5
  

         |
55 | | mnflt 8474 |
. . . . . . . . . . 11
   |
56 | 55 | adantl 262 |
. . . . . . . . . 10
 

  |
57 | | breq1 3758 |
. . . . . . . . . . 11
     |
58 | 57 | adantr 261 |
. . . . . . . . . 10
 
     |
59 | 56, 58 | mpbird 156 |
. . . . . . . . 9
 
   |
60 | 59 | a1d 22 |
. . . . . . . 8
 
       |
61 | 60 | adantlr 446 |
. . . . . . 7
   
       |
62 | | mnfltpnf 8476 |
. . . . . . . . . 10
 |
63 | | breq12 3760 |
. . . . . . . . . 10
 
     |
64 | 62, 63 | mpbiri 157 |
. . . . . . . . 9
 
   |
65 | 64 | a1d 22 |
. . . . . . . 8
 
       |
66 | 65 | adantlr 446 |
. . . . . . 7
   
       |
67 | 43 | adantll 445 |
. . . . . . 7
   
       |
68 | 61, 66, 67 | 3jaodan 1200 |
. . . . . 6
    
 
 
    |
69 | 68 | anasss 379 |
. . . . 5
  

         |
70 | 46, 54, 69 | 3jaoian 1199 |
. . . 4
  
  
    
    |
71 | 70 | 3impb 1099 |
. . 3
  
 
        |
72 | 2, 71 | syl3an3b 1172 |
. 2
  
   
    |
73 | 1, 72 | syl3an1b 1170 |
1
    
    |