Proof of Theorem sgn3da
Step | Hyp | Ref
| Expression |
1 | | sgn3da.0 |
. . . . . . . . 9
   |
2 | | sgnval 13151 |
. . . . . . . . 9

sgn       
       |
3 | 1, 2 | syl 17 |
. . . . . . . 8
 sgn               |
4 | 3 | eqeq2d 2461 |
. . . . . . 7
  sgn 
     
        |
5 | 4 | pm5.32i 643 |
. . . . . 6
 
sgn   
              |
6 | | sgn3da.1 |
. . . . . . . . 9
 sgn 
    |
7 | 6 | eqcoms 2459 |
. . . . . . . 8
 sgn 
    |
8 | 7 | bicomd 205 |
. . . . . . 7
 sgn 
    |
9 | 8 | adantl 468 |
. . . . . 6
 
sgn   
   |
10 | 5, 9 | sylbir 217 |
. . . . 5
 
     
      
   |
11 | 10 | expcom 437 |
. . . 4
           
 
    |
12 | 11 | pm5.74d 251 |
. . 3
           
  
     |
13 | 3 | eqeq2d 2461 |
. . . . . . 7
        sgn                      |
14 | 13 | pm5.32i 643 |
. . . . . 6
 
      sgn  
                     |
15 | | eqeq1 2455 |
. . . . . . . . 9
       
  sgn        sgn     |
16 | 15 | imbi1d 319 |
. . . . . . . 8
       
   sgn    
 
   
  
    sgn    
 
       |
17 | | eqeq1 2455 |
. . . . . . . . 9
        sgn        sgn     |
18 | 17 | imbi1d 319 |
. . . . . . . 8
         sgn 
    
 
         sgn    
 
       |
19 | | sgn3da.6 |
. . . . . . . . . . . . . . 15
 
   |
20 | 19 | adantr 467 |
. . . . . . . . . . . . . 14
         |
21 | | simp2 1009 |
. . . . . . . . . . . . . . 15
       |
22 | 21 | 3expia 1210 |
. . . . . . . . . . . . . 14
     
   |
23 | 20, 22 | impbida 843 |
. . . . . . . . . . . . 13
 
   
   |
24 | | pm3.24 893 |
. . . . . . . . . . . . . . . . 17
   |
25 | 24 | pm2.21i 135 |
. . . . . . . . . . . . . . . 16
  
  |
26 | 25 | adantl 468 |
. . . . . . . . . . . . . . 15
 
     |
27 | 26 | expr 620 |
. . . . . . . . . . . . . 14
 
 
   |
28 | | tbtru 1454 |
. . . . . . . . . . . . . 14
  
 

  |
29 | 27, 28 | sylib 200 |
. . . . . . . . . . . . 13
 
  
   |
30 | 23, 29 | anbi12d 717 |
. . . . . . . . . . . 12
 
   
 
      |
31 | | ancom 452 |
. . . . . . . . . . . . 13
     |
32 | | truan 1461 |
. . . . . . . . . . . . 13
    |
33 | 31, 32 | bitri 253 |
. . . . . . . . . . . 12
    |
34 | 30, 33 | syl6bb 265 |
. . . . . . . . . . 11
 
   
 
     |
35 | 34 | 3adant3 1028 |
. . . . . . . . . 10
 
 sgn      

 
   |
36 | | sgn3da.3 |
. . . . . . . . . . . 12
 sgn       |
37 | 36 | eqcoms 2459 |
. . . . . . . . . . 11
  sgn      |
38 | 37 | 3ad2ant3 1031 |
. . . . . . . . . 10
 
 sgn   
   |
39 | 35, 38 | bitr4d 260 |
. . . . . . . . 9
 
 sgn      

 
   |
40 | 39 | 3expia 1210 |
. . . . . . . 8
 
   sgn    
 
      |
41 | 19 | 3adant2 1027 |
. . . . . . . . . . . . . . 15
 
   |
42 | 41 | 3expia 1210 |
. . . . . . . . . . . . . 14
 
     |
43 | | tbtru 1454 |
. . . . . . . . . . . . . 14
  
     |
44 | 42, 43 | sylib 200 |
. . . . . . . . . . . . 13
 
   
  |
45 | | pm3.35 591 |
. . . . . . . . . . . . . . 15
  
 
  |
46 | 45 | adantll 720 |
. . . . . . . . . . . . . 14
    
    |
47 | | simp2 1009 |
. . . . . . . . . . . . . . 15
   
   |
48 | 47 | 3expia 1210 |
. . . . . . . . . . . . . 14
    
    |
49 | 46, 48 | impbida 843 |
. . . . . . . . . . . . 13
 
  
    |
50 | 44, 49 | anbi12d 717 |
. . . . . . . . . . . 12
 
   
 
      |
51 | | truan 1461 |
. . . . . . . . . . . 12
    |
52 | 50, 51 | syl6bb 265 |
. . . . . . . . . . 11
 
   
 
     |
53 | 52 | 3adant3 1028 |
. . . . . . . . . 10
 
sgn  
    
 
   |
54 | | sgn3da.2 |
. . . . . . . . . . . 12
 sgn 
    |
55 | 54 | eqcoms 2459 |
. . . . . . . . . . 11
 sgn 
    |
56 | 55 | 3ad2ant3 1031 |
. . . . . . . . . 10
 
sgn  
    |
57 | 53, 56 | bitr4d 260 |
. . . . . . . . 9
 
sgn  
    
 
   |
58 | 57 | 3expia 1210 |
. . . . . . . 8
 
  sgn    
 
      |
59 | 16, 18, 40, 58 | ifbothda 3916 |
. . . . . . 7
        sgn 
    
 
    |
60 | 59 | imp 431 |
. . . . . 6
 
      sgn     
 
     |
61 | 14, 60 | sylbir 217 |
. . . . 5
 
                    
 
     |
62 | 61 | expcom 437 |
. . . 4
                      

 
    |
63 | 62 | pm5.74d 251 |
. . 3
                   
  

   
    |
64 | | sgn3da.4 |
. . . . 5
 
   |
65 | 64 | expcom 437 |
. . . 4
     |
66 | 65 | adantl 468 |
. . 3
      |
67 | 19 | ex 436 |
. . . . . . 7
     |
68 | 67 | adantr 467 |
. . . . . 6
 
     |
69 | | simp1 1008 |
. . . . . . . 8
 
   |
70 | | df-ne 2624 |
. . . . . . . . . . . 12

  |
71 | | 0xr 9687 |
. . . . . . . . . . . . 13
 |
72 | | xrlttri2 11441 |
. . . . . . . . . . . . 13
   
     |
73 | 1, 71, 72 | sylancl 668 |
. . . . . . . . . . . 12
       |
74 | 70, 73 | syl5bbr 263 |
. . . . . . . . . . 11
       |
75 | 74 | biimpa 487 |
. . . . . . . . . 10
 
 
   |
76 | 75 | ord 379 |
. . . . . . . . 9
 
 
   |
77 | 76 | 3impia 1205 |
. . . . . . . 8
 

  |
78 | | sgn3da.5 |
. . . . . . . 8
 

  |
79 | 69, 77, 78 | syl2anc 667 |
. . . . . . 7
 
   |
80 | 79 | 3expia 1210 |
. . . . . 6
 
 
   |
81 | 68, 80 | jca 535 |
. . . . 5
 
  
 
    |
82 | 81 | expcom 437 |
. . . 4
 
  

     |
83 | 82 | adantl 468 |
. . 3
  
  

     |
84 | 12, 63, 66, 83 | ifbothda 3916 |
. 2
    |
85 | 84 | trud 1453 |
1
   |