Proof of Theorem outsideofeq
Step | Hyp | Ref
| Expression |
1 | | simp1 1008 |
. . . . 5
  
   
         
       
        |
2 | | simp21 1041 |
. . . . 5
  
   
         
       
            |
3 | | simp32 1045 |
. . . . 5
  
   
         
       
            |
4 | | simp22 1042 |
. . . . 5
  
   
         
       
            |
5 | | broutsideof2 30889 |
. . . . 5
  
   
           OutsideOf   
     
      |
6 | 1, 2, 3, 4, 5 | syl13anc 1270 |
. . . 4
  
   
         
       
       OutsideOf                |
7 | 6 | anbi1d 711 |
. . 3
  
   
         
       
        OutsideOf      Cgr     
  

      
 Cgr 
     |
8 | | simp33 1046 |
. . . . 5
  
   
         
       
            |
9 | | broutsideof2 30889 |
. . . . 5
  
   
           OutsideOf   
     
      |
10 | 1, 2, 8, 4, 9 | syl13anc 1270 |
. . . 4
  
   
         
       
       OutsideOf                |
11 | 10 | anbi1d 711 |
. . 3
  
   
         
       
        OutsideOf      Cgr     
  

      
 Cgr 
     |
12 | 7, 11 | anbi12d 717 |
. 2
  
   
         
       
         OutsideOf  
   Cgr     OutsideOf      Cgr 
                
 Cgr 
              
 Cgr 
      |
13 | | simpll3 1049 |
. . . . . . 7
   
  

      
 Cgr 
              
 Cgr 
  
          |
14 | | simprl3 1055 |
. . . . . . 7
   
  

      
 Cgr 
              
 Cgr 
  
          |
15 | 13, 14 | jca 535 |
. . . . . 6
   
  

      
 Cgr 
              
 Cgr 
  
                    |
16 | 15 | adantl 468 |
. . . . 5
                         
        
  

      
 Cgr 
              
 Cgr 
          
    

       |
17 | | simpll2 1048 |
. . . . . 6
   
  

      
 Cgr 
              
 Cgr 
  
  |
18 | 17 | adantl 468 |
. . . . 5
                         
        
  

      
 Cgr 
              
 Cgr 
      |
19 | | simp23 1043 |
. . . . . 6
  
   
         
       
            |
20 | | simp31 1044 |
. . . . . 6
  
   
         
       
            |
21 | | simprlr 773 |
. . . . . 6
                         
        
  

      
 Cgr 
              
 Cgr 
       Cgr     |
22 | | simprrr 775 |
. . . . . 6
                         
        
  

      
 Cgr 
              
 Cgr 
       Cgr     |
23 | 1, 2, 3, 2, 8, 19,
20, 21, 22 | cgrtr3and 30762 |
. . . . 5
                         
        
  

      
 Cgr 
              
 Cgr 
       Cgr     |
24 | 16, 18, 23 | jca32 538 |
. . . 4
                         
        
  

      
 Cgr 
              
 Cgr 
        

             
   Cgr       |
25 | | simprll 772 |
. . . . . . . 8
                         
          
 
  
   Cgr           |
26 | | simprlr 773 |
. . . . . . . 8
                         
          
 
  
   Cgr           |
27 | | simprrr 775 |
. . . . . . . 8
                         
          
 
  
   Cgr         Cgr 
   |
28 | | midofsegid 30871 |
. . . . . . . . . 10
  
   
     
   
             
   Cgr   
   |
29 | 1, 2, 4, 3, 8, 28 | syl122anc 1277 |
. . . . . . . . 9
  
   
         
       
          
 
    Cgr 
     |
30 | 29 | adantr 467 |
. . . . . . . 8
                         
          
 
  
   Cgr         

  
   Cgr   
   |
31 | 25, 26, 27, 30 | mp3and 1367 |
. . . . . . 7
                         
          
 
  
   Cgr     
  |
32 | 31 | exp32 610 |
. . . . . 6
  
   
         
       
          
 
       Cgr        |
33 | | simprlr 773 |
. . . . . . . . 9
                         
          
 
  
   Cgr           |
34 | | simprll 772 |
. . . . . . . . 9
                         
          
 
  
   Cgr           |
35 | 1, 2, 8, 4, 3, 33,
34 | btwnexchand 30793 |
. . . . . . . 8
                         
          
 
  
   Cgr           |
36 | | simprrr 775 |
. . . . . . . 8
                         
          
 
  
   Cgr         Cgr 
   |
37 | 1, 2, 3, 8, 35, 36 | endofsegidand 30853 |
. . . . . . 7
                         
          
 
  
   Cgr     
  |
38 | 37 | exp32 610 |
. . . . . 6
  
   
         
       
          
 
       Cgr        |
39 | | simprll 772 |
. . . . . . . . . 10
                         
          
 
  
   Cgr           |
40 | | simprlr 773 |
. . . . . . . . . 10
                         
          
 
  
   Cgr           |
41 | 1, 2, 3, 4, 8, 39,
40 | btwnexchand 30793 |
. . . . . . . . 9
                         
          
 
  
   Cgr           |
42 | | simprrr 775 |
. . . . . . . . . 10
                         
          
 
  
   Cgr         Cgr 
   |
43 | 1, 2, 3, 2, 8, 42 | cgrcomand 30758 |
. . . . . . . . 9
                         
          
 
  
   Cgr         Cgr 
   |
44 | 1, 2, 8, 3, 41, 43 | endofsegidand 30853 |
. . . . . . . 8
                         
          
 
  
   Cgr     
  |
45 | 44 | eqcomd 2457 |
. . . . . . 7
                         
          
 
  
   Cgr     
  |
46 | 45 | exp32 610 |
. . . . . 6
  
   
         
       
          
 
       Cgr        |
47 | | simprr 766 |
. . . . . . . . . . 11
                         
          

        Cgr               |
48 | | simplrr 771 |
. . . . . . . . . . . . 13
     

        Cgr        
   Cgr     |
49 | 48 | adantl 468 |
. . . . . . . . . . . 12
                         
          

        Cgr             Cgr     |
50 | 1, 2, 3, 2, 8, 49 | cgrcomand 30758 |
. . . . . . . . . . 11
                         
          

        Cgr             Cgr     |
51 | 1, 2, 8, 3, 47, 50 | endofsegidand 30853 |
. . . . . . . . . 10
                         
          

        Cgr            |
52 | 51 | eqcomd 2457 |
. . . . . . . . 9
                         
          

        Cgr            |
53 | 52 | expr 620 |
. . . . . . . 8
                         
          
 
  
   Cgr         
   |
54 | | simprr 766 |
. . . . . . . . . 10
                         
          

        Cgr               |
55 | | simplrr 771 |
. . . . . . . . . . 11
     

        Cgr        
   Cgr     |
56 | 55 | adantl 468 |
. . . . . . . . . 10
                         
          

        Cgr             Cgr     |
57 | 1, 2, 3, 8, 54, 56 | endofsegidand 30853 |
. . . . . . . . 9
                         
          

        Cgr            |
58 | 57 | expr 620 |
. . . . . . . 8
                         
          
 
  
   Cgr         
   |
59 | | simprrl 774 |
. . . . . . . . . 10
                         
          
 
  
   Cgr        |
60 | 59 | necomd 2679 |
. . . . . . . . 9
                         
          
 
  
   Cgr        |
61 | | simprll 772 |
. . . . . . . . 9
                         
          
 
  
   Cgr           |
62 | | simprlr 773 |
. . . . . . . . 9
                         
          
 
  
   Cgr           |
63 | | btwnconn1 30868 |
. . . . . . . . . . 11
  
   
     
   
                          |
64 | 1, 2, 4, 3, 8, 63 | syl122anc 1277 |
. . . . . . . . . 10
  
   
         
       
       
  
 
    

       |
65 | 64 | adantr 467 |
. . . . . . . . 9
                         
          
 
  
   Cgr       
 

               |
66 | 60, 61, 62, 65 | mp3and 1367 |
. . . . . . . 8
                         
          
 
  
   Cgr           
    |
67 | 53, 58, 66 | mpjaod 383 |
. . . . . . 7
                         
          
 
  
   Cgr     
  |
68 | 67 | exp32 610 |
. . . . . 6
  
   
         
       
          
 
       Cgr        |
69 | 32, 38, 46, 68 | ccased 958 |
. . . . 5
  
   
         
       
          

              
   Cgr   
    |
70 | 69 | imp32 435 |
. . . 4
                         
          

             
   Cgr        |
71 | 24, 70 | syldan 473 |
. . 3
                         
        
  

      
 Cgr 
              
 Cgr 
      |
72 | 71 | ex 436 |
. 2
  
   
         
       
                    
 Cgr 
              
 Cgr 
  
   |
73 | 12, 72 | sylbid 219 |
1
  
   
         
       
         OutsideOf  
   Cgr     OutsideOf      Cgr 
  
   |