Proof of Theorem xmulneg1
Step | Hyp | Ref
| Expression |
1 | | xneg0 11528 |
. . . . . . . . 9
   |
2 | 1 | eqeq2i 2483 |
. . . . . . . 8
 
      |
3 | | 0xr 9705 |
. . . . . . . . 9
 |
4 | | xneg11 11531 |
. . . . . . . . 9
      
   |
5 | 3, 4 | mpan2 685 |
. . . . . . . 8

 
 
   |
6 | 2, 5 | syl5bbr 267 |
. . . . . . 7

 
   |
7 | 6 | adantr 472 |
. . . . . 6
        |
8 | 7 | orbi1d 717 |
. . . . 5
      
     |
9 | 8 | ifbid 3894 |
. . . 4
                 
        

 
                     

                                   

 
                     

               |
10 | | xnegpnf 11525 |
. . . . . . . . . . . . . 14

 |
11 | 10 | eqeq2i 2483 |
. . . . . . . . . . . . 13
 
     |
12 | | simpll 768 |
. . . . . . . . . . . . . 14
      
  |
13 | | pnfxr 11435 |
. . . . . . . . . . . . . 14
 |
14 | | xneg11 11531 |
. . . . . . . . . . . . . 14
     
   |
15 | 12, 13, 14 | sylancl 675 |
. . . . . . . . . . . . 13
         
   |
16 | 11, 15 | syl5bbr 267 |
. . . . . . . . . . . 12
        
   |
17 | 16 | anbi2d 718 |
. . . . . . . . . . 11
        
  
     |
18 | | xnegmnf 11526 |
. . . . . . . . . . . . . 14

 |
19 | 18 | eqeq2i 2483 |
. . . . . . . . . . . . 13
 
     |
20 | | mnfxr 11437 |
. . . . . . . . . . . . . 14
 |
21 | | xneg11 11531 |
. . . . . . . . . . . . . 14
     
   |
22 | 12, 20, 21 | sylancl 675 |
. . . . . . . . . . . . 13
         
   |
23 | 19, 22 | syl5bbr 267 |
. . . . . . . . . . . 12
        
   |
24 | 23 | anbi2d 718 |
. . . . . . . . . . 11
                 |
25 | 17, 24 | orbi12d 724 |
. . . . . . . . . 10
                 
 
 
     |
26 | | xlt0neg1 11535 |
. . . . . . . . . . . . . . 15


     |
27 | 26 | ad2antrr 740 |
. . . . . . . . . . . . . 14
             |
28 | 27 | bicomd 206 |
. . . . . . . . . . . . 13
         
   |
29 | 28 | anbi1d 719 |
. . . . . . . . . . . 12
          
      |
30 | | xlt0neg2 11536 |
. . . . . . . . . . . . . . 15


     |
31 | 30 | ad2antrr 740 |
. . . . . . . . . . . . . 14
             |
32 | 31 | bicomd 206 |
. . . . . . . . . . . . 13
            |
33 | 32 | anbi1d 719 |
. . . . . . . . . . . 12
         
 
    |
34 | 29, 33 | orbi12d 724 |
. . . . . . . . . . 11
           

   
   
     |
35 | | orcom 394 |
. . . . . . . . . . 11
  

  
 
 
    |
36 | 34, 35 | syl6bb 269 |
. . . . . . . . . 10
           

   
 
 
     |
37 | 25, 36 | orbi12d 724 |
. . . . . . . . 9
             
        

 
  
  

    

       |
38 | 37 | biimpar 493 |
. . . . . . . 8
   
 
    

    

    
              

 
     |
39 | 38 | iftrued 3880 |
. . . . . . 7
   
 
    

    

    
                

             |
40 | | xmullem2 11576 |
. . . . . . . . . . 11
            

   
  

    

       |
41 | 40 | adantr 472 |
. . . . . . . . . 10
          
 
   

   
  

    

       |
42 | 23 | anbi2d 718 |
. . . . . . . . . . . . 13
        
  
     |
43 | 16 | anbi2d 718 |
. . . . . . . . . . . . 13
                 |
44 | 42, 43 | orbi12d 724 |
. . . . . . . . . . . 12
                 
 
 
     |
45 | 28 | anbi1d 719 |
. . . . . . . . . . . . . 14
          
      |
46 | 32 | anbi1d 719 |
. . . . . . . . . . . . . 14
         
 
    |
47 | 45, 46 | orbi12d 724 |
. . . . . . . . . . . . 13
           

   
   
     |
48 | | orcom 394 |
. . . . . . . . . . . . 13
  

  
 
 
    |
49 | 47, 48 | syl6bb 269 |
. . . . . . . . . . . 12
           

   
 
 
     |
50 | 44, 49 | orbi12d 724 |
. . . . . . . . . . 11
             
        

 
  
  

    

       |
51 | 50 | notbid 301 |
. . . . . . . . . 10
                      

 
  
  

    

       |
52 | 41, 51 | sylibrd 242 |
. . . . . . . . 9
          
 
   

   
              

 
      |
53 | 52 | imp 436 |
. . . . . . . 8
   
 
    

    

    
  
           

       |
54 | 53 | iffalsed 3883 |
. . . . . . 7
   
 
    

    

    
                

              
        

 
      
                   

 
      
    |
55 | | iftrue 3878 |
. . . . . . . . . 10
   

    

        

    

          
 
   

            |
56 | 55 | adantl 473 |
. . . . . . . . 9
   
 
    

    

    
          

          
 
   

            |
57 | | xnegeq 11523 |
. . . . . . . . 9
     
 
   

          
 
   

                      

          
 
   

             |
58 | 56, 57 | syl 17 |
. . . . . . . 8
   
 
    

    

    
      
 
   

          
 
   

             |
59 | 58, 10 | syl6eq 2521 |
. . . . . . 7
   
 
    

    

    
      
 
   

          
 
   

            |
60 | 39, 54, 59 | 3eqtr4d 2515 |
. . . . . 6
   
 
    

    

    
                

              
        

 
      
               

          
 
   

            |
61 | 50 | biimpar 493 |
. . . . . . . . . 10
   
 
    

    

    
              

 
     |
62 | 61 | iftrued 3880 |
. . . . . . . . 9
   
 
    

    

    
                

              
        

 
      
     |
63 | 41 | con2d 119 |
. . . . . . . . . . . . . 14
          
 
   

   
  

    

       |
64 | 63 | imp 436 |
. . . . . . . . . . . . 13
   
 
    

    

    
  

    

      |
65 | 64 | iffalsed 3883 |
. . . . . . . . . . . 12
   
 
    

    

    
          

          
 
   

              
 
   

           |
66 | | iftrue 3878 |
. . . . . . . . . . . . 13
   

    

        

    

           |
67 | 66 | adantl 473 |
. . . . . . . . . . . 12
   
 
    

    

    
          

           |
68 | 65, 67 | eqtrd 2505 |
. . . . . . . . . . 11
   
 
    

    

    
          

          
 
   

            |
69 | | xnegeq 11523 |
. . . . . . . . . . 11
     
 
   

          
 
   

                      

          
 
   

             |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
   
 
    

    

    
      
 
   

          
 
   

             |
71 | 70, 18 | syl6eq 2521 |
. . . . . . . . 9
   
 
    

    

    
      
 
   

          
 
   

            |
72 | 62, 71 | eqtr4d 2508 |
. . . . . . . 8
   
 
    

    

    
                

              
        

 
      
               

          
 
   

            |
73 | 72 | adantlr 729 |
. . . . . . 7
    
 
          

       

    

    
                

              
        

 
      
               

          
 
   

            |
74 | 37 | notbid 301 |
. . . . . . . . . . 11
                      

 
  
  

    

       |
75 | 74 | biimpar 493 |
. . . . . . . . . 10
   
 
    

    

    
  
           

       |
76 | 75 | adantr 472 |
. . . . . . . . 9
    
 
          

       

    

    
  
           

       |
77 | 76 | iffalsed 3883 |
. . . . . . . 8
    
 
          

       

    

    
                

                |
78 | 51 | biimpar 493 |
. . . . . . . . . 10
   
 
    

    

    
  
           

       |
79 | 78 | adantlr 729 |
. . . . . . . . 9
    
 
          

       

    

    
  
           

       |
80 | 79 | iffalsed 3883 |
. . . . . . . 8
    
 
          

       

    

    
                

              
        

 
      
                   

 
      
    |
81 | | iffalse 3881 |
. . . . . . . . . . . 12
         

        

    

          
 
   

              
 
   

           |
82 | 81 | ad2antlr 741 |
. . . . . . . . . . 11
    
 
          

       

    

    
          

          
 
   

              
 
   

           |
83 | | iffalse 3881 |
. . . . . . . . . . . 12
         

        

    

             |
84 | 83 | adantl 473 |
. . . . . . . . . . 11
    
 
          

       

    

    
          

             |
85 | 82, 84 | eqtrd 2505 |
. . . . . . . . . 10
    
 
          

       

    

    
          

          
 
   

              |
86 | | xnegeq 11523 |
. . . . . . . . . 10
     
 
   

          
 
   

                        

          
 
   

                |
87 | 85, 86 | syl 17 |
. . . . . . . . 9
    
 
          

       

    

    
      
 
   

          
 
   

                |
88 | | xmullem 11575 |
. . . . . . . . . . . 12
    
 
          

       

    

    
  |
89 | 88 | recnd 9687 |
. . . . . . . . . . 11
    
 
          

       

    

    
  |
90 | | ancom 457 |
. . . . . . . . . . . . . . 15
  
    |
91 | | orcom 394 |
. . . . . . . . . . . . . . . 16
       |
92 | 91 | notbii 303 |
. . . . . . . . . . . . . . 15
  
    |
93 | 90, 92 | anbi12i 711 |
. . . . . . . . . . . . . 14
      
 
 
    |
94 | | orcom 394 |
. . . . . . . . . . . . . . 15
   

    

            

      |
95 | 94 | notbii 303 |
. . . . . . . . . . . . . 14
         

            

      |
96 | 93, 95 | anbi12i 711 |
. . . . . . . . . . . . 13
   
 
    

    

         
          

       |
97 | | orcom 394 |
. . . . . . . . . . . . . 14
   

    

            

      |
98 | 97 | notbii 303 |
. . . . . . . . . . . . 13
         

            

      |
99 | | xmullem 11575 |
. . . . . . . . . . . . 13
    
 
          

       

    

    
  |
100 | 96, 98, 99 | syl2anb 487 |
. . . . . . . . . . . 12
    
 
          

       

    

    
  |
101 | 100 | recnd 9687 |
. . . . . . . . . . 11
    
 
          

       

    

    
  |
102 | 89, 101 | mulneg1d 10092 |
. . . . . . . . . 10
    
 
          

       

    

    
    
   |
103 | | rexneg 11527 |
. . . . . . . . . . . 12
      |
104 | 88, 103 | syl 17 |
. . . . . . . . . . 11
    
 
          

       

    

    
     |
105 | 104 | oveq1d 6323 |
. . . . . . . . . 10
    
 
          

       

    

    
        |
106 | 88, 100 | remulcld 9689 |
. . . . . . . . . . 11
    
 
          

       

    

    
    |
107 | | rexneg 11527 |
. . . . . . . . . . 11
        
   |
108 | 106, 107 | syl 17 |
. . . . . . . . . 10
    
 
          

       

    

    
         |
109 | 102, 105,
108 | 3eqtr4d 2515 |
. . . . . . . . 9
    
 
          

       

    

    
         |
110 | 87, 109 | eqtr4d 2508 |
. . . . . . . 8
    
 
          

       

    

    
      
 
   

          
 
   

               |
111 | 77, 80, 110 | 3eqtr4d 2515 |
. . . . . . 7
    
 
          

       

    

    
                

              
        

 
      
               

          
 
   

            |
112 | 73, 111 | pm2.61dan 808 |
. . . . . 6
   
 
    

    

    
                

              
        

 
      
               

          
 
   

            |
113 | 60, 112 | pm2.61dan 808 |
. . . . 5
              
        

 
                     

                  
 
   

          
 
   

            |
114 | 113 | ifeq2da 3903 |
. . . 4
             
           

              
        

 
      
                

    

          
 
   

             |
115 | 9, 114 | eqtrd 2505 |
. . 3
                 
        

 
                     

                               

          
 
   

             |
116 | | xnegeq 11523 |
. . . . 5
           

    

          
 
   

          
            

    

          
 
   

               |
117 | 116, 1 | syl6eq 2521 |
. . . 4
           

    

          
 
   

          
            

    

          
 
   

             |
118 | | xnegeq 11523 |
. . . 4
           

    

          
 
   

               

    

          
 
   

                            

          
 
   

                       

          
 
   

            |
119 | 117, 118 | ifsb 3885 |
. . 3
                  

          
 
   

                       

    

          
 
   

            |
120 | 115, 119 | syl6eqr 2523 |
. 2
                 
        

 
                     

                               

          
 
   

             |
121 | | xnegcl 11529 |
. . 3

    |
122 | | xmulval 11541 |
. . 3
  

                             

              
        

 
      
      |
123 | 121, 122 | sylan 479 |
. 2
                       
        

 
                     

               |
124 | | xmulval 11541 |
. . 3
                  
 
   

          
 
   

             |
125 | | xnegeq 11523 |
. . 3
                

    

          
 
   

                              

    

          
 
   

             |
126 | 124, 125 | syl 17 |
. 2
                            

          
 
   

             |
127 | 120, 123,
126 | 3eqtr4d 2515 |
1
                  |