Proof of Theorem signswch
Step | Hyp | Ref
| Expression |
1 | | df-pr 3962 |
. . . . . 6
            |
2 | | snsstp1 4114 |
. . . . . . 7
         |
3 | | snsstp3 4116 |
. . . . . . 7
 
      |
4 | 2, 3 | unssi 3600 |
. . . . . 6
             |
5 | 1, 4 | eqsstri 3448 |
. . . . 5
          |
6 | 5 | sseli 3414 |
. . . 4
            |
7 | | signsw.p |
. . . . 5
                   |
8 | 7 | signspval 29513 |
. . . 4
            
         |
9 | 6, 8 | sylan 479 |
. . 3
                     |
10 | 9 | neeq1d 2702 |
. 2
              
 
 
    |
11 | | neeq1 2705 |
. . . 4
      
 
 
    |
12 | 11 | bibi1d 326 |
. . 3
          
  
  
      |
13 | | neeq1 2705 |
. . . 4
      
 
 
    |
14 | 13 | bibi1d 326 |
. . 3
          
  
  
      |
15 | | neirr 2652 |
. . . . 5
 |
16 | 15 | a1i 11 |
. . . 4
            

  |
17 | | 0re 9661 |
. . . . . 6
 |
18 | 17 | ltnri 9761 |
. . . . 5
 |
19 | | simpr 468 |
. . . . . . . 8
            
   |
20 | 19 | oveq2d 6324 |
. . . . . . 7
            
       |
21 | | neg1cn 10735 |
. . . . . . . . . 10
  |
22 | | ax-1cn 9615 |
. . . . . . . . . 10
 |
23 | | prssi 4119 |
. . . . . . . . . 10
          |
24 | 21, 22, 23 | mp2an 686 |
. . . . . . . . 9
     |
25 | | simpll 768 |
. . . . . . . . 9
            
       |
26 | 24, 25 | sseldi 3416 |
. . . . . . . 8
            
   |
27 | 26 | mul01d 9850 |
. . . . . . 7
            
     |
28 | 20, 27 | eqtrd 2505 |
. . . . . 6
            
     |
29 | 28 | breq1d 4405 |
. . . . 5
            
       |
30 | 18, 29 | mtbiri 310 |
. . . 4
            

    |
31 | 16, 30 | 2falsed 358 |
. . 3
            
       |
32 | | simplr 770 |
. . . . . . . 8
            

       |
33 | | tpcomb 4060 |
. . . . . . . 8
           |
34 | 32, 33 | syl6eleq 2559 |
. . . . . . 7
            

       |
35 | | simpr 468 |
. . . . . . . 8
            

  |
36 | 35 | neqned 2650 |
. . . . . . 7
            

  |
37 | 34, 36 | jca 541 |
. . . . . 6
            

         |
38 | | eldifsn 4088 |
. . . . . . 7
         
         |
39 | | neg1ne0 10737 |
. . . . . . . . 9
  |
40 | | ax-1ne0 9626 |
. . . . . . . . 9
 |
41 | | diftpsn3 4101 |
. . . . . . . . 9
  

               |
42 | 39, 40, 41 | mp2an 686 |
. . . . . . . 8
              |
43 | 42 | eleq2i 2541 |
. . . . . . 7
         
      |
44 | 38, 43 | bitr3i 259 |
. . . . . 6
       
      |
45 | 37, 44 | sylib 201 |
. . . . 5
            

      |
46 | | neirr 2652 |
. . . . . . . . . . 11
   |
47 | | 0le1 10158 |
. . . . . . . . . . . . 13
 |
48 | | 1re 9660 |
. . . . . . . . . . . . . 14
 |
49 | 17, 48 | lenlti 9772 |
. . . . . . . . . . . . 13

  |
50 | 47, 49 | mpbi 213 |
. . . . . . . . . . . 12
 |
51 | | neg1mulneg1e1 10850 |
. . . . . . . . . . . . 13
     |
52 | 51 | breq1i 4402 |
. . . . . . . . . . . 12
    
  |
53 | 50, 52 | mtbir 306 |
. . . . . . . . . . 11
   
 |
54 | 46, 53 | 2false 357 |
. . . . . . . . . 10
      
  |
55 | | neeq1 2705 |
. . . . . . . . . . 11
   
     |
56 | | oveq2 6316 |
. . . . . . . . . . . 12
           |
57 | 56 | breq1d 4405 |
. . . . . . . . . . 11
     
       |
58 | 55, 57 | bibi12d 328 |
. . . . . . . . . 10
       
       
    |
59 | 54, 58 | mpbiri 241 |
. . . . . . . . 9
   
      |
60 | 59 | adantl 473 |
. . . . . . . 8
         
      |
61 | | neg1rr 10736 |
. . . . . . . . . . . 12
  |
62 | | neg1lt0 10738 |
. . . . . . . . . . . . 13
  |
63 | | 0lt1 10157 |
. . . . . . . . . . . . 13
 |
64 | 61, 17, 48 | lttri 9778 |
. . . . . . . . . . . . 13
  

   |
65 | 62, 63, 64 | mp2an 686 |
. . . . . . . . . . . 12
  |
66 | 61, 65 | gtneii 9764 |
. . . . . . . . . . 11
  |
67 | 21 | mulid1i 9663 |
. . . . . . . . . . . 12
     |
68 | 67, 62 | eqbrtri 4415 |
. . . . . . . . . . 11
    |
69 | 66, 68 | 2th 247 |
. . . . . . . . . 10
 
     |
70 | | neeq1 2705 |
. . . . . . . . . . 11
  
    |
71 | | oveq2 6316 |
. . . . . . . . . . . 12
         |
72 | 71 | breq1d 4405 |
. . . . . . . . . . 11
    
      |
73 | 70, 72 | bibi12d 328 |
. . . . . . . . . 10
      
          |
74 | 69, 73 | mpbiri 241 |
. . . . . . . . 9
  
      |
75 | 74 | adantl 473 |
. . . . . . . 8
      
 
      |
76 | | elpri 3976 |
. . . . . . . 8
      
   |
77 | 60, 75, 76 | mpjaodan 803 |
. . . . . . 7
         
   |
78 | 77 | adantr 472 |
. . . . . 6
         
      |
79 | | neeq2 2706 |
. . . . . . . 8
  
    |
80 | | oveq1 6315 |
. . . . . . . . 9
  
      |
81 | 80 | breq1d 4405 |
. . . . . . . 8
    
      |
82 | 79, 81 | bibi12d 328 |
. . . . . . 7
      
 
       |
83 | 82 | adantl 473 |
. . . . . 6
            
 
       |
84 | 78, 83 | mpbird 240 |
. . . . 5
        
     |
85 | 45, 84 | sylan 479 |
. . . 4
                       |
86 | 66 | necomi 2697 |
. . . . . . . . . . 11
  |
87 | 21, 22 | mulcomi 9667 |
. . . . . . . . . . . . 13
       |
88 | 87 | breq1i 4402 |
. . . . . . . . . . . 12
      
  |
89 | 68, 88 | mpbi 213 |
. . . . . . . . . . 11
    |
90 | 86, 89 | 2th 247 |
. . . . . . . . . 10
    
  |
91 | | neeq1 2705 |
. . . . . . . . . . 11
  
    |
92 | | oveq2 6316 |
. . . . . . . . . . . 12
         |
93 | 92 | breq1d 4405 |
. . . . . . . . . . 11
    
      |
94 | 91, 93 | bibi12d 328 |
. . . . . . . . . 10
      
 
       |
95 | 90, 94 | mpbiri 241 |
. . . . . . . . 9
  
     |
96 | 95 | adantl 473 |
. . . . . . . 8
        
     |
97 | | neirr 2652 |
. . . . . . . . . . 11
 |
98 | 22 | mulid1i 9663 |
. . . . . . . . . . . . 13
   |
99 | 98 | breq1i 4402 |
. . . . . . . . . . . 12
  
  |
100 | 50, 99 | mtbir 306 |
. . . . . . . . . . 11
   |
101 | 97, 100 | 2false 357 |
. . . . . . . . . 10

    |
102 | | neeq1 2705 |
. . . . . . . . . . 11
 
   |
103 | | oveq2 6316 |
. . . . . . . . . . . 12
       |
104 | 103 | breq1d 4405 |
. . . . . . . . . . 11
   
     |
105 | 102, 104 | bibi12d 328 |
. . . . . . . . . 10
     

      |
106 | 101, 105 | mpbiri 241 |
. . . . . . . . 9
 
     |
107 | 106 | adantl 473 |
. . . . . . . 8
      

     |
108 | 96, 107, 76 | mpjaodan 803 |
. . . . . . 7
           |
109 | 108 | adantr 472 |
. . . . . 6
      

     |
110 | | neeq2 2706 |
. . . . . . . 8
 
   |
111 | | oveq1 6315 |
. . . . . . . . 9
 
     |
112 | 111 | breq1d 4405 |
. . . . . . . 8
   
     |
113 | 110, 112 | bibi12d 328 |
. . . . . . 7
     

      |
114 | 113 | adantl 473 |
. . . . . 6
      
 
          |
115 | 109, 114 | mpbird 240 |
. . . . 5
      
      |
116 | 45, 115 | sylan 479 |
. . . 4
                      |
117 | | elpri 3976 |
. . . . 5
      
   |
118 | 117 | ad2antrr 740 |
. . . 4
            

     |
119 | 85, 116, 118 | mpjaodan 803 |
. . 3
            

      |
120 | 12, 14, 31, 119 | ifbothda 3907 |
. 2
                       |
121 | 10, 120 | bitrd 261 |
1
              
     |