Proof of Theorem xrsdsreclblem
Step | Hyp | Ref
| Expression |
1 | | necom 2721 |
. . . . 5

  |
2 | | xrleltne 11236 |
. . . . . 6
   
   |
3 | | mnfxr 11208 |
. . . . . . . . . . . 12
 |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
          
  |
5 | | simpl1 991 |
. . . . . . . . . . 11
             |
6 | | simpl2 992 |
. . . . . . . . . . 11
             |
7 | | pnfnre 9539 |
. . . . . . . . . . . . . 14
 |
8 | 7 | neli 2787 |
. . . . . . . . . . . . 13
 |
9 | | mnfle 11227 |
. . . . . . . . . . . . . . . . . 18

  |
10 | 5, 9 | syl 16 |
. . . . . . . . . . . . . . . . 17
          
  |
11 | | simpl3 993 |
. . . . . . . . . . . . . . . . 17
             |
12 | 4, 5, 6, 10, 11 | xrlelttrd 11248 |
. . . . . . . . . . . . . . . 16
          
  |
13 | | xrltne 11251 |
. . . . . . . . . . . . . . . 16
 
  |
14 | 4, 6, 12, 13 | syl3anc 1219 |
. . . . . . . . . . . . . . 15
             |
15 | | xaddpnf1 11310 |
. . . . . . . . . . . . . . 15
         |
16 | 6, 14, 15 | syl2anc 661 |
. . . . . . . . . . . . . 14
                 |
17 | 16 | eleq1d 2523 |
. . . . . . . . . . . . 13
                   |
18 | 8, 17 | mtbiri 303 |
. . . . . . . . . . . 12
          
  
   |
19 | | ngtmnft 11253 |
. . . . . . . . . . . . . 14


   |
20 | 5, 19 | syl 16 |
. . . . . . . . . . . . 13
           
   |
21 | | simpr 461 |
. . . . . . . . . . . . . 14
                   |
22 | | xnegeq 11291 |
. . . . . . . . . . . . . . . . 17
      |
23 | | xnegmnf 11294 |
. . . . . . . . . . . . . . . . 17

 |
24 | 22, 23 | syl6eq 2511 |
. . . . . . . . . . . . . . . 16
     |
25 | 24 | oveq2d 6219 |
. . . . . . . . . . . . . . 15
             |
26 | 25 | eleq1d 2523 |
. . . . . . . . . . . . . 14
               |
27 | 21, 26 | syl5ibcom 220 |
. . . . . . . . . . . . 13
           
  
    |
28 | 20, 27 | sylbird 235 |
. . . . . . . . . . . 12
           
  
    |
29 | 18, 28 | mt3d 125 |
. . . . . . . . . . 11
          
  |
30 | | xrre2 11256 |
. . . . . . . . . . 11
    
  |
31 | 4, 5, 6, 29, 11, 30 | syl32anc 1227 |
. . . . . . . . . 10
             |
32 | | pnfxr 11206 |
. . . . . . . . . . . 12
 |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
          
  |
34 | 5 | xnegcld 11377 |
. . . . . . . . . . . . . . 15
               |
35 | | xnegpnf 11293 |
. . . . . . . . . . . . . . . . 17

 |
36 | | pnfge 11224 |
. . . . . . . . . . . . . . . . . . . 20

  |
37 | 6, 36 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
             |
38 | 5, 6, 33, 11, 37 | xrltletrd 11249 |
. . . . . . . . . . . . . . . . . 18
             |
39 | | xltnegi 11300 |
. . . . . . . . . . . . . . . . . 18
  
     |
40 | 5, 33, 38, 39 | syl3anc 1219 |
. . . . . . . . . . . . . . . . 17
                |
41 | 35, 40 | syl5eqbrr 4437 |
. . . . . . . . . . . . . . . 16
          
    |
42 | | xrltne 11251 |
. . . . . . . . . . . . . . . 16
          |
43 | 4, 34, 41, 42 | syl3anc 1219 |
. . . . . . . . . . . . . . 15
               |
44 | | xaddpnf2 11311 |
. . . . . . . . . . . . . . 15
  
          |
45 | 34, 43, 44 | syl2anc 661 |
. . . . . . . . . . . . . 14
                  |
46 | 45 | eleq1d 2523 |
. . . . . . . . . . . . 13
             
  
   |
47 | 8, 46 | mtbiri 303 |
. . . . . . . . . . . 12
          
 
     |
48 | | nltpnft 11252 |
. . . . . . . . . . . . . 14


   |
49 | 6, 48 | syl 16 |
. . . . . . . . . . . . 13
           
   |
50 | | oveq1 6210 |
. . . . . . . . . . . . . . 15
              |
51 | 50 | eleq1d 2523 |
. . . . . . . . . . . . . 14
                |
52 | 21, 51 | syl5ibcom 220 |
. . . . . . . . . . . . 13
           
 
      |
53 | 49, 52 | sylbird 235 |
. . . . . . . . . . . 12
           
 
      |
54 | 47, 53 | mt3d 125 |
. . . . . . . . . . 11
             |
55 | | xrre2 11256 |
. . . . . . . . . . 11
      
  |
56 | 5, 6, 33, 11, 54, 55 | syl32anc 1227 |
. . . . . . . . . 10
             |
57 | 31, 56 | jca 532 |
. . . . . . . . 9
               |
58 | 57 | ex 434 |
. . . . . . . 8
         
     |
59 | 58 | 3expia 1190 |
. . . . . . 7
          
      |
60 | 59 | 3adant3 1008 |
. . . . . 6
          
      |
61 | 2, 60 | sylbird 235 |
. . . . 5
          
      |
62 | 1, 61 | syl5bi 217 |
. . . 4
          
      |
63 | 62 | 3exp 1187 |
. . 3


        
        |
64 | 63 | com34 83 |
. 2


        
        |
65 | 64 | 3imp1 1201 |
1
           
     |