Step | Hyp | Ref
| Expression |
1 | | xblss2.1 |
. . . . . 6
        |
2 | | xblss2.2 |
. . . . . 6
   |
3 | | xblss2.4 |
. . . . . 6
   |
4 | | elbl 12319 |
. . . . . 6
      
         

        |
5 | 1, 2, 3, 4 | syl3anc 1184 |
. . . . 5
         

        |
6 | 5 | simprbda 378 |
. . . 4
 
           |
7 | 1 | adantr 272 |
. . . . . . . 8
 
                |
8 | | xblss2.3 |
. . . . . . . . 9
   |
9 | 8 | adantr 272 |
. . . . . . . 8
 
           |
10 | | xmetcl 12280 |
. . . . . . . 8
      

      |
11 | 7, 9, 6, 10 | syl3anc 1184 |
. . . . . . 7
 
               |
12 | 11 | adantr 272 |
. . . . . 6
                   |
13 | | xblss2.6 |
. . . . . . . . . 10
       |
14 | 13 | adantr 272 |
. . . . . . . . 9
 
               |
15 | 14 | rexrd 7687 |
. . . . . . . 8
 
               |
16 | 3 | adantr 272 |
. . . . . . . 8
 
           |
17 | 15, 16 | xaddcld 9508 |
. . . . . . 7
 
                    |
18 | 17 | adantr 272 |
. . . . . 6
                        |
19 | | xblss2.5 |
. . . . . . 7
   |
20 | 19 | ad2antrr 475 |
. . . . . 6
               |
21 | 2 | adantr 272 |
. . . . . . . . . 10
 
           |
22 | | xmetcl 12280 |
. . . . . . . . . 10
      

      |
23 | 7, 21, 6, 22 | syl3anc 1184 |
. . . . . . . . 9
 
               |
24 | 15, 23 | xaddcld 9508 |
. . . . . . . 8
 
                        |
25 | | xmettri2 12289 |
. . . . . . . . 9
             
               |
26 | 7, 21, 9, 6, 25 | syl13anc 1186 |
. . . . . . . 8
 
                            |
27 | 5 | simplbda 379 |
. . . . . . . . 9
 
               |
28 | | xltadd2 9501 |
. . . . . . . . . 10
               
                         |
29 | 23, 16, 14, 28 | syl3anc 1184 |
. . . . . . . . 9
 
                                       |
30 | 27, 29 | mpbid 146 |
. . . . . . . 8
 
                                 |
31 | 11, 24, 17, 26, 30 | xrlelttrd 9434 |
. . . . . . 7
 
                        |
32 | 31 | adantr 272 |
. . . . . 6
                            |
33 | 19 | adantr 272 |
. . . . . . . . . 10
 
           |
34 | 16 | xnegcld 9479 |
. . . . . . . . . 10
 
             |
35 | 33, 34 | xaddcld 9508 |
. . . . . . . . 9
 
                 |
36 | | xblss2.7 |
. . . . . . . . . 10
    
  
     |
37 | 36 | adantr 272 |
. . . . . . . . 9
 
                     |
38 | | xleadd1a 9497 |
. . . . . . . . 9
            
                                  |
39 | 15, 35, 16, 37, 38 | syl31anc 1187 |
. . . . . . . 8
 
                               |
40 | 39 | adantr 272 |
. . . . . . 7
                     
             |
41 | | xnpcan 9496 |
. . . . . . . 8
                |
42 | 33, 41 | sylan 279 |
. . . . . . 7
                          |
43 | 40, 42 | breqtrd 3899 |
. . . . . 6
                     
  |
44 | 12, 18, 20, 32, 43 | xrltletrd 9435 |
. . . . 5
                   |
45 | 27 | adantr 272 |
. . . . . 6
                   |
46 | 36 | ad2antrr 475 |
. . . . . . . . 9
                         |
47 | 19 | ad2antrr 475 |
. . . . . . . . . . . . 13
               |
48 | | xrpnfdc 9466 |
. . . . . . . . . . . . 13

DECID
  |
49 | 47, 48 | syl 14 |
. . . . . . . . . . . 12
            
DECID
  |
50 | | 0xr 7684 |
. . . . . . . . . . . . . . . 16
 |
51 | 50 | a1i 9 |
. . . . . . . . . . . . . . 15
 
           |
52 | | xmetge0 12293 |
. . . . . . . . . . . . . . . 16
      

      |
53 | 7, 21, 9, 52 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
 
               |
54 | 51, 15, 35, 53, 37 | xrletrd 9436 |
. . . . . . . . . . . . . 14
 
                 |
55 | | ge0nemnf 9448 |
. . . . . . . . . . . . . 14
       
               |
56 | 35, 54, 55 | syl2anc 406 |
. . . . . . . . . . . . 13
 
                 |
57 | 56 | adantr 272 |
. . . . . . . . . . . 12
                     |
58 | | xaddmnf1 9472 |
. . . . . . . . . . . . . . . . 17
         |
59 | 58 | ex 114 |
. . . . . . . . . . . . . . . 16


       |
60 | 47, 59 | syl 14 |
. . . . . . . . . . . . . . 15
             
       |
61 | | simpr 109 |
. . . . . . . . . . . . . . . . . . 19
               |
62 | | xnegeq 9451 |
. . . . . . . . . . . . . . . . . . 19
      |
63 | 61, 62 | syl 14 |
. . . . . . . . . . . . . . . . . 18
                  |
64 | | xnegpnf 9452 |
. . . . . . . . . . . . . . . . . 18

 |
65 | 63, 64 | syl6eq 2148 |
. . . . . . . . . . . . . . . . 17
                 |
66 | 65 | oveq2d 5722 |
. . . . . . . . . . . . . . . 16
                         |
67 | 66 | eqeq1d 2108 |
. . . . . . . . . . . . . . 15
                           |
68 | 60, 67 | sylibrd 168 |
. . . . . . . . . . . . . 14
             
         |
69 | 68 | a1d 22 |
. . . . . . . . . . . . 13
             DECID

  
       |
70 | 69 | necon1ddc 2345 |
. . . . . . . . . . . 12
             DECID
           |
71 | 49, 57, 70 | mp2d 47 |
. . . . . . . . . . 11
               |
72 | 71, 65 | oveq12d 5724 |
. . . . . . . . . 10
                        |
73 | | pnfaddmnf 9474 |
. . . . . . . . . 10
 
  |
74 | 72, 73 | syl6eq 2148 |
. . . . . . . . 9
                     |
75 | 46, 74 | breqtrd 3899 |
. . . . . . . 8
                   |
76 | 53 | biantrud 300 |
. . . . . . . . . 10
 
                  
        |
77 | | xrletri3 9429 |
. . . . . . . . . . 11
                
        |
78 | 15, 50, 77 | sylancl 407 |
. . . . . . . . . 10
 
                  
        |
79 | | xmeteq0 12287 |
. . . . . . . . . . 11
      

    
   |
80 | 7, 21, 9, 79 | syl3anc 1184 |
. . . . . . . . . 10
 
             
   |
81 | 76, 78, 80 | 3bitr2d 215 |
. . . . . . . . 9
 
             
   |
82 | 81 | adantr 272 |
. . . . . . . 8
                 
   |
83 | 75, 82 | mpbid 146 |
. . . . . . 7
               |
84 | 83 | oveq1d 5721 |
. . . . . 6
                       |
85 | 61, 71 | eqtr4d 2135 |
. . . . . 6
               |
86 | 45, 84, 85 | 3brtr3d 3904 |
. . . . 5
                   |
87 | | xmetge0 12293 |
. . . . . . . . . . 11
      

      |
88 | 7, 21, 6, 87 | syl3anc 1184 |
. . . . . . . . . 10
 
               |
89 | 51, 23, 16, 88, 27 | xrlelttrd 9434 |
. . . . . . . . 9
 
           |
90 | 51, 16, 89 | xrltled 9426 |
. . . . . . . 8
 
           |
91 | | ge0nemnf 9448 |
. . . . . . . 8
     |
92 | 16, 90, 91 | syl2anc 406 |
. . . . . . 7
 
           |
93 | 16, 92 | jca 302 |
. . . . . 6
 
         
   |
94 | | xrnemnf 9405 |
. . . . . 6
  
    |
95 | 93, 94 | sylib 121 |
. . . . 5
 
             |
96 | 44, 86, 95 | mpjaodan 753 |
. . . 4
 
               |
97 | | elbl 12319 |
. . . . 5
      
         

        |
98 | 7, 9, 33, 97 | syl3anc 1184 |
. . . 4
 
                           |
99 | 6, 96, 98 | mpbir2and 896 |
. . 3
 
                   |
100 | 99 | ex 114 |
. 2
         
           |
101 | 100 | ssrdv 3053 |
1
                   |