Proof of Theorem signswch
Step | Hyp | Ref
| Expression |
1 | | df-pr 3980 |
. . . . . . 7
            |
2 | | snsstp1 4124 |
. . . . . . . 8
         |
3 | | snsstp3 4126 |
. . . . . . . 8
 
      |
4 | 2, 3 | unssi 3631 |
. . . . . . 7
             |
5 | 1, 4 | eqsstri 3486 |
. . . . . 6
          |
6 | 5 | sseli 3452 |
. . . . 5
            |
7 | 6 | adantr 465 |
. . . 4
           
       |
8 | | signsw.p |
. . . . 5
                   |
9 | 8 | signspval 27089 |
. . . 4
            
         |
10 | 7, 9 | sylancom 667 |
. . 3
                     |
11 | 10 | neeq1d 2725 |
. 2
              
 
 
    |
12 | | neeq1 2729 |
. . . 4
      
 
 
    |
13 | 12 | bibi1d 319 |
. . 3
          
  
  
      |
14 | | neeq1 2729 |
. . . 4
      
 
 
    |
15 | 14 | bibi1d 319 |
. . 3
          
  
  
      |
16 | | neirr 2653 |
. . . . 5
 |
17 | 16 | a1i 11 |
. . . 4
            

  |
18 | | 0re 9489 |
. . . . . 6
 |
19 | 18 | ltnri 9586 |
. . . . 5
 |
20 | | simpr 461 |
. . . . . . . 8
            
   |
21 | 20 | oveq2d 6208 |
. . . . . . 7
            
       |
22 | | neg1cn 10528 |
. . . . . . . . . 10
  |
23 | | ax-1cn 9443 |
. . . . . . . . . 10
 |
24 | | prssi 4129 |
. . . . . . . . . 10
          |
25 | 22, 23, 24 | mp2an 672 |
. . . . . . . . 9
     |
26 | | simpll 753 |
. . . . . . . . 9
            
       |
27 | 25, 26 | sseldi 3454 |
. . . . . . . 8
            
   |
28 | 27 | mul01d 9671 |
. . . . . . 7
            
     |
29 | 21, 28 | eqtrd 2492 |
. . . . . 6
            
     |
30 | 29 | breq1d 4402 |
. . . . 5
            
       |
31 | 19, 30 | mtbiri 303 |
. . . 4
            

    |
32 | 17, 31 | 2falsed 351 |
. . 3
            
       |
33 | | simplr 754 |
. . . . . . . . 9
            

       |
34 | | tpcomb 4072 |
. . . . . . . . 9
           |
35 | 33, 34 | syl6eleq 2549 |
. . . . . . . 8
            

       |
36 | | simpr 461 |
. . . . . . . . 9
            

  |
37 | 36 | neneqad 2652 |
. . . . . . . 8
            

  |
38 | 35, 37 | jca 532 |
. . . . . . 7
            

         |
39 | | eldifsn 4100 |
. . . . . . . 8
         
         |
40 | | neg1ne0 10530 |
. . . . . . . . . 10
  |
41 | | ax-1ne0 9454 |
. . . . . . . . . 10
 |
42 | | diftpsn3 4112 |
. . . . . . . . . 10
  

               |
43 | 40, 41, 42 | mp2an 672 |
. . . . . . . . 9
              |
44 | 43 | eleq2i 2529 |
. . . . . . . 8
         
      |
45 | 39, 44 | bitr3i 251 |
. . . . . . 7
       
      |
46 | 38, 45 | sylib 196 |
. . . . . 6
            

      |
47 | 46 | adantr 465 |
. . . . 5
                
      |
48 | | neirr 2653 |
. . . . . . . . . . 11
   |
49 | | 0le1 9966 |
. . . . . . . . . . . . 13
 |
50 | | 1re 9488 |
. . . . . . . . . . . . . 14
 |
51 | 18, 50 | lenlti 9597 |
. . . . . . . . . . . . 13

  |
52 | 49, 51 | mpbi 208 |
. . . . . . . . . . . 12
 |
53 | | neg1mulneg1e1 10642 |
. . . . . . . . . . . . 13
     |
54 | 53 | breq1i 4399 |
. . . . . . . . . . . 12
    
  |
55 | 52, 54 | mtbir 299 |
. . . . . . . . . . 11
   
 |
56 | 48, 55 | 2false 350 |
. . . . . . . . . 10
      
  |
57 | | neeq1 2729 |
. . . . . . . . . . 11
   
     |
58 | | oveq2 6200 |
. . . . . . . . . . . 12
           |
59 | 58 | breq1d 4402 |
. . . . . . . . . . 11
     
       |
60 | 57, 59 | bibi12d 321 |
. . . . . . . . . 10
       
       
    |
61 | 56, 60 | mpbiri 233 |
. . . . . . . . 9
   
      |
62 | 61 | adantl 466 |
. . . . . . . 8
         
      |
63 | | neg1lt0 10531 |
. . . . . . . . . . . . 13
  |
64 | | 0lt1 9965 |
. . . . . . . . . . . . 13
 |
65 | | neg1rr 10529 |
. . . . . . . . . . . . . 14
  |
66 | 65, 18, 50 | lttri 9603 |
. . . . . . . . . . . . 13
  

   |
67 | 63, 64, 66 | mp2an 672 |
. . . . . . . . . . . 12
  |
68 | 65, 50 | ltnei 9601 |
. . . . . . . . . . . 12
 
   |
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . 11
  |
70 | 22 | mulid1i 9491 |
. . . . . . . . . . . 12
     |
71 | 70, 63 | eqbrtri 4411 |
. . . . . . . . . . 11
    |
72 | 69, 71 | 2th 239 |
. . . . . . . . . 10
 
     |
73 | | neeq1 2729 |
. . . . . . . . . . 11
  
    |
74 | | oveq2 6200 |
. . . . . . . . . . . 12
         |
75 | 74 | breq1d 4402 |
. . . . . . . . . . 11
    
      |
76 | 73, 75 | bibi12d 321 |
. . . . . . . . . 10
      
          |
77 | 72, 76 | mpbiri 233 |
. . . . . . . . 9
  
      |
78 | 77 | adantl 466 |
. . . . . . . 8
      
 
      |
79 | | elpri 3997 |
. . . . . . . 8
      
   |
80 | 62, 78, 79 | mpjaodan 784 |
. . . . . . 7
         
   |
81 | 80 | adantr 465 |
. . . . . 6
         
      |
82 | | neeq2 2731 |
. . . . . . . 8
  
    |
83 | | oveq1 6199 |
. . . . . . . . 9
  
      |
84 | 83 | breq1d 4402 |
. . . . . . . 8
    
      |
85 | 82, 84 | bibi12d 321 |
. . . . . . 7
      
 
       |
86 | 85 | adantl 466 |
. . . . . 6
            
 
       |
87 | 81, 86 | mpbird 232 |
. . . . 5
        
     |
88 | 47, 87 | sylancom 667 |
. . . 4
                       |
89 | 46 | adantr 465 |
. . . . 5
               
      |
90 | 69 | necomi 2718 |
. . . . . . . . . . 11
  |
91 | 22, 23 | mulcomi 9495 |
. . . . . . . . . . . . 13
       |
92 | 91 | breq1i 4399 |
. . . . . . . . . . . 12
      
  |
93 | 71, 92 | mpbi 208 |
. . . . . . . . . . 11
    |
94 | 90, 93 | 2th 239 |
. . . . . . . . . 10
    
  |
95 | | neeq1 2729 |
. . . . . . . . . . 11
  
    |
96 | | oveq2 6200 |
. . . . . . . . . . . 12
         |
97 | 96 | breq1d 4402 |
. . . . . . . . . . 11
    
      |
98 | 95, 97 | bibi12d 321 |
. . . . . . . . . 10
      
 
       |
99 | 94, 98 | mpbiri 233 |
. . . . . . . . 9
  
     |
100 | 99 | adantl 466 |
. . . . . . . 8
        
     |
101 | | neirr 2653 |
. . . . . . . . . . 11
 |
102 | 23 | mulid1i 9491 |
. . . . . . . . . . . . 13
   |
103 | 102 | breq1i 4399 |
. . . . . . . . . . . 12
  
  |
104 | 52, 103 | mtbir 299 |
. . . . . . . . . . 11
   |
105 | 101, 104 | 2false 350 |
. . . . . . . . . 10

    |
106 | | neeq1 2729 |
. . . . . . . . . . 11
 
   |
107 | | oveq2 6200 |
. . . . . . . . . . . 12
       |
108 | 107 | breq1d 4402 |
. . . . . . . . . . 11
   
     |
109 | 106, 108 | bibi12d 321 |
. . . . . . . . . 10
     

      |
110 | 105, 109 | mpbiri 233 |
. . . . . . . . 9
 
     |
111 | 110 | adantl 466 |
. . . . . . . 8
      

     |
112 | 100, 111,
79 | mpjaodan 784 |
. . . . . . 7
           |
113 | 112 | adantr 465 |
. . . . . 6
      

     |
114 | | neeq2 2731 |
. . . . . . . 8
 
   |
115 | | oveq1 6199 |
. . . . . . . . 9
 
     |
116 | 115 | breq1d 4402 |
. . . . . . . 8
   
     |
117 | 114, 116 | bibi12d 321 |
. . . . . . 7
     

      |
118 | 117 | adantl 466 |
. . . . . 6
      
 
          |
119 | 113, 118 | mpbird 232 |
. . . . 5
      
      |
120 | 89, 119 | sylancom 667 |
. . . 4
                      |
121 | | elpri 3997 |
. . . . 5
      
   |
122 | 121 | ad2antrr 725 |
. . . 4
            

     |
123 | 88, 120, 122 | mpjaodan 784 |
. . 3
            

      |
124 | 13, 15, 32, 123 | ifbothda 3924 |
. 2
                       |
125 | 11, 124 | bitrd 253 |
1
              
     |