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

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

        |
6 | 5 | simprbda 383 |
. . . 4
 
           |
7 | 1 | adantr 276 |
. . . . . . . 8
 
                |
8 | | xblss2.3 |
. . . . . . . . 9
   |
9 | 8 | adantr 276 |
. . . . . . . 8
 
           |
10 | | xmetcl 13822 |
. . . . . . . 8
      

      |
11 | 7, 9, 6, 10 | syl3anc 1238 |
. . . . . . 7
 
               |
12 | 11 | adantr 276 |
. . . . . 6
                   |
13 | | xblss2.6 |
. . . . . . . . . 10
       |
14 | 13 | adantr 276 |
. . . . . . . . 9
 
               |
15 | 14 | rexrd 8006 |
. . . . . . . 8
 
               |
16 | 3 | adantr 276 |
. . . . . . . 8
 
           |
17 | 15, 16 | xaddcld 9883 |
. . . . . . 7
 
                    |
18 | 17 | adantr 276 |
. . . . . 6
                        |
19 | | xblss2.5 |
. . . . . . 7
   |
20 | 19 | ad2antrr 488 |
. . . . . 6
               |
21 | 2 | adantr 276 |
. . . . . . . . . 10
 
           |
22 | | xmetcl 13822 |
. . . . . . . . . 10
      

      |
23 | 7, 21, 6, 22 | syl3anc 1238 |
. . . . . . . . 9
 
               |
24 | 15, 23 | xaddcld 9883 |
. . . . . . . 8
 
                        |
25 | | xmettri2 13831 |
. . . . . . . . 9
             
               |
26 | 7, 21, 9, 6, 25 | syl13anc 1240 |
. . . . . . . 8
 
                            |
27 | 5 | simplbda 384 |
. . . . . . . . 9
 
               |
28 | | xltadd2 9876 |
. . . . . . . . . 10
               
                         |
29 | 23, 16, 14, 28 | syl3anc 1238 |
. . . . . . . . 9
 
                                       |
30 | 27, 29 | mpbid 147 |
. . . . . . . 8
 
                                 |
31 | 11, 24, 17, 26, 30 | xrlelttrd 9809 |
. . . . . . 7
 
                        |
32 | 31 | adantr 276 |
. . . . . 6
                            |
33 | 19 | adantr 276 |
. . . . . . . . . 10
 
           |
34 | 16 | xnegcld 9854 |
. . . . . . . . . 10
 
             |
35 | 33, 34 | xaddcld 9883 |
. . . . . . . . 9
 
                 |
36 | | xblss2.7 |
. . . . . . . . . 10
    
  
     |
37 | 36 | adantr 276 |
. . . . . . . . 9
 
                     |
38 | | xleadd1a 9872 |
. . . . . . . . 9
            
                                  |
39 | 15, 35, 16, 37, 38 | syl31anc 1241 |
. . . . . . . 8
 
                               |
40 | 39 | adantr 276 |
. . . . . . 7
                     
             |
41 | | xnpcan 9871 |
. . . . . . . 8
                |
42 | 33, 41 | sylan 283 |
. . . . . . 7
                          |
43 | 40, 42 | breqtrd 4029 |
. . . . . 6
                     
  |
44 | 12, 18, 20, 32, 43 | xrltletrd 9810 |
. . . . 5
                   |
45 | 27 | adantr 276 |
. . . . . 6
                   |
46 | 36 | ad2antrr 488 |
. . . . . . . . 9
                         |
47 | 19 | ad2antrr 488 |
. . . . . . . . . . . . 13
               |
48 | | xrpnfdc 9841 |
. . . . . . . . . . . . 13

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

      |
53 | 7, 21, 9, 52 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
 
               |
54 | 51, 15, 35, 53, 37 | xrletrd 9811 |
. . . . . . . . . . . . . 14
 
                 |
55 | | ge0nemnf 9823 |
. . . . . . . . . . . . . 14
       
               |
56 | 35, 54, 55 | syl2anc 411 |
. . . . . . . . . . . . 13
 
                 |
57 | 56 | adantr 276 |
. . . . . . . . . . . 12
                     |
58 | | xaddmnf1 9847 |
. . . . . . . . . . . . . . . . 17
         |
59 | 58 | ex 115 |
. . . . . . . . . . . . . . . 16


       |
60 | 47, 59 | syl 14 |
. . . . . . . . . . . . . . 15
             
       |
61 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
               |
62 | | xnegeq 9826 |
. . . . . . . . . . . . . . . . . . 19
      |
63 | 61, 62 | syl 14 |
. . . . . . . . . . . . . . . . . 18
                  |
64 | | xnegpnf 9827 |
. . . . . . . . . . . . . . . . . 18

 |
65 | 63, 64 | eqtrdi 2226 |
. . . . . . . . . . . . . . . . 17
                 |
66 | 65 | oveq2d 5890 |
. . . . . . . . . . . . . . . 16
                         |
67 | 66 | eqeq1d 2186 |
. . . . . . . . . . . . . . 15
                           |
68 | 60, 67 | sylibrd 169 |
. . . . . . . . . . . . . 14
             
         |
69 | 68 | a1d 22 |
. . . . . . . . . . . . 13
             DECID

  
       |
70 | 69 | necon1ddc 2425 |
. . . . . . . . . . . 12
             DECID
           |
71 | 49, 57, 70 | mp2d 47 |
. . . . . . . . . . 11
               |
72 | 71, 65 | oveq12d 5892 |
. . . . . . . . . 10
                        |
73 | | pnfaddmnf 9849 |
. . . . . . . . . 10
 
  |
74 | 72, 73 | eqtrdi 2226 |
. . . . . . . . 9
                     |
75 | 46, 74 | breqtrd 4029 |
. . . . . . . 8
                   |
76 | 53 | biantrud 304 |
. . . . . . . . . 10
 
                  
        |
77 | | xrletri3 9803 |
. . . . . . . . . . 11
                
        |
78 | 15, 50, 77 | sylancl 413 |
. . . . . . . . . 10
 
                  
        |
79 | | xmeteq0 13829 |
. . . . . . . . . . 11
      

    
   |
80 | 7, 21, 9, 79 | syl3anc 1238 |
. . . . . . . . . 10
 
             
   |
81 | 76, 78, 80 | 3bitr2d 216 |
. . . . . . . . 9
 
             
   |
82 | 81 | adantr 276 |
. . . . . . . 8
                 
   |
83 | 75, 82 | mpbid 147 |
. . . . . . 7
               |
84 | 83 | oveq1d 5889 |
. . . . . 6
                       |
85 | 61, 71 | eqtr4d 2213 |
. . . . . 6
               |
86 | 45, 84, 85 | 3brtr3d 4034 |
. . . . 5
                   |
87 | | xmetge0 13835 |
. . . . . . . . . . 11
      

      |
88 | 7, 21, 6, 87 | syl3anc 1238 |
. . . . . . . . . 10
 
               |
89 | 51, 23, 16, 88, 27 | xrlelttrd 9809 |
. . . . . . . . 9
 
           |
90 | 51, 16, 89 | xrltled 9798 |
. . . . . . . 8
 
           |
91 | | ge0nemnf 9823 |
. . . . . . . 8
     |
92 | 16, 90, 91 | syl2anc 411 |
. . . . . . 7
 
           |
93 | 16, 92 | jca 306 |
. . . . . 6
 
         
   |
94 | | xrnemnf 9776 |
. . . . . 6
  
    |
95 | 93, 94 | sylib 122 |
. . . . 5
 
             |
96 | 44, 86, 95 | mpjaodan 798 |
. . . 4
 
               |
97 | | elbl 13861 |
. . . . 5
      
         

        |
98 | 7, 9, 33, 97 | syl3anc 1238 |
. . . 4
 
                           |
99 | 6, 96, 98 | mpbir2and 944 |
. . 3
 
                   |
100 | 99 | ex 115 |
. 2
         
           |
101 | 100 | ssrdv 3161 |
1
                   |