Step | Hyp | Ref
| Expression |
1 | | simpl21 1066 |
. . . . . 6
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
      |
2 | | simpl22 1067 |
. . . . . 6
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
      |
3 | 1, 2 | jca 532 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
    
       |
4 | | simpl23 1068 |
. . . . . 6
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
      |
5 | | simpl3r 1044 |
. . . . . 6
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
      |
6 | 4, 5 | jca 532 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
    
       |
7 | | simprll 761 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
  ![[,] [,]](_icc.gif)    |
8 | | simprlr 762 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
  ![[,] [,]](_icc.gif)    |
9 | | simp21 1021 |
. . . . . . . . . . . . . . . . . . 19
  
   
         
         
      |
10 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
      |
11 | | fveecn 23301 |
. . . . . . . . . . . . . . . . . 18
     
           |
12 | 10, 11 | sylan 471 |
. . . . . . . . . . . . . . . . 17
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
           |
13 | | simp3r 1017 |
. . . . . . . . . . . . . . . . . . 19
  
   
         
         
      |
14 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
      |
15 | | fveecn 23301 |
. . . . . . . . . . . . . . . . . 18
     
           |
16 | 14, 15 | sylan 471 |
. . . . . . . . . . . . . . . . 17
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
           |
17 | | mulid2 9496 |
. . . . . . . . . . . . . . . . . . 19
                 |
18 | | mul02 9659 |
. . . . . . . . . . . . . . . . . . 19
             |
19 | 17, 18 | oveqan12d 6220 |
. . . . . . . . . . . . . . . . . 18
                                 |
20 | | addid1 9661 |
. . . . . . . . . . . . . . . . . . 19
                 |
21 | 20 | adantr 465 |
. . . . . . . . . . . . . . . . . 18
                       |
22 | 19, 21 | eqtrd 2495 |
. . . . . . . . . . . . . . . . 17
                               |
23 | 12, 16, 22 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         |
24 | | oveq2 6209 |
. . . . . . . . . . . . . . . . . . . . 21
       |
25 | | 1m0e1 10544 |
. . . . . . . . . . . . . . . . . . . . 21
   |
26 | 24, 25 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . 20
     |
27 | 26 | oveq1d 6216 |
. . . . . . . . . . . . . . . . . . 19
                 |
28 | | oveq1 6208 |
. . . . . . . . . . . . . . . . . . 19
               |
29 | 27, 28 | oveq12d 6219 |
. . . . . . . . . . . . . . . . . 18
                                 |
30 | 29 | eqeq1d 2456 |
. . . . . . . . . . . . . . . . 17
                     
                     |
31 | 30 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                               |
32 | 23, 31 | mpbird 232 |
. . . . . . . . . . . . . . 15
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                           |
33 | 32 | eqeq2d 2468 |
. . . . . . . . . . . . . 14
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                     |
34 | | eqcom 2463 |
. . . . . . . . . . . . . 14
        
          |
35 | 33, 34 | syl6bb 261 |
. . . . . . . . . . . . 13
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                     |
36 | 35 | biimpd 207 |
. . . . . . . . . . . 12
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
           |
37 | 36 | adantrd 468 |
. . . . . . . . . . 11
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                           |
38 | 37 | ralimdva 2832 |
. . . . . . . . . 10
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                                                                       |
39 | 38 | impancom 440 |
. . . . . . . . 9
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                
                 |
40 | 9 | ad2antrr 725 |
. . . . . . . . . 10
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                      |
41 | | simp3l 1016 |
. . . . . . . . . . 11
  
   
         
         
      |
42 | 41 | ad2antrr 725 |
. . . . . . . . . 10
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                      |
43 | | eqeefv 23302 |
. . . . . . . . . 10
     
      
                |
44 | 40, 42, 43 | syl2anc 661 |
. . . . . . . . 9
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                                  |
45 | 39, 44 | sylibrd 234 |
. . . . . . . 8
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                
   |
46 | 45 | necon3d 2676 |
. . . . . . 7
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                
   |
47 | 46 | impr 619 |
. . . . . 6
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     
                                                   |
48 | 47 | anasss 647 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
  |
49 | | eqtr2 2481 |
. . . . . . . 8
                                                                             |
50 | 49 | ralimi 2819 |
. . . . . . 7
 
                                               
                                       |
51 | 50 | adantr 465 |
. . . . . 6
                                                                                           |
52 | 51 | ad2antll 728 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
                                        |
53 | | axeuclidlem 23361 |
. . . . 5
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
                                      
               ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                         |
54 | 3, 6, 7, 8, 48, 52, 53 | syl231anc 1239 |
. . . 4
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
               ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                         |
55 | 54 | exp32 605 |
. . 3
  
   
         
              ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                                                                     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                           |
56 | 55 | rexlimdvv 2953 |
. 2
  
   
         
              ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                          |
57 | | brbtwn 23298 |
. . . . 5
     
             
  ![[,] [,]](_icc.gif)                                |
58 | 41, 9, 13, 57 | syl3anc 1219 |
. . . 4
  
   
         
                 ![[,] [,]](_icc.gif)                                |
59 | | simp22 1022 |
. . . . 5
  
   
         
         
      |
60 | | simp23 1023 |
. . . . 5
  
   
         
         
      |
61 | | brbtwn 23298 |
. . . . 5
     
             
  ![[,] [,]](_icc.gif)                                |
62 | 41, 59, 60, 61 | syl3anc 1219 |
. . . 4
  
   
         
                 ![[,] [,]](_icc.gif)                                |
63 | 58, 62 | 3anbi12d 1291 |
. . 3
  
   
         
             

  
     ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)                                 |
64 | | r19.26 2955 |
. . . . . . 7
 
                                              
 
                         
                            |
65 | 64 | 2rexbii 2863 |
. . . . . 6
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                              
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                           |
66 | | reeanv 2994 |
. . . . . 6
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                        
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
67 | 65, 66 | bitri 249 |
. . . . 5
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                              
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
68 | 67 | anbi1i 695 |
. . . 4
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                   
  
  ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)   
                             |
69 | | r19.41v 2979 |
. . . . . 6
    ![[,] [,]](_icc.gif)                                                    
 
  ![[,] [,]](_icc.gif)   
                                                  |
70 | 69 | rexbii 2862 |
. . . . 5
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                    
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                                                      |
71 | | r19.41v 2979 |
. . . . 5
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                                                   
 
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                                  |
72 | 70, 71 | bitri 249 |
. . . 4
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                    
 
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                                  |
73 | | df-3an 967 |
. . . 4
     ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)   
                         
  
  ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)   
                             |
74 | 68, 72, 73 | 3bitr4i 277 |
. . 3
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                    
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
75 | 63, 74 | syl6bbr 263 |
. 2
  
   
         
             

  
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                        |
76 | | simpl22 1067 |
. . . . . 6
                            
   
            |
77 | | simpl21 1066 |
. . . . . 6
                            
   
            |
78 | | simprl 755 |
. . . . . 6
                            
   
            |
79 | | brbtwn 23298 |
. . . . . 6
     
             
  ![[,] [,]](_icc.gif)                                |
80 | 76, 77, 78, 79 | syl3anc 1219 |
. . . . 5
                            
   
        
 
  ![[,] [,]](_icc.gif)   
                            |
81 | | simpl23 1068 |
. . . . . 6
                            
   
            |
82 | | simprr 756 |
. . . . . 6
                            
   
            |
83 | | brbtwn 23298 |
. . . . . 6
     
                ![[,] [,]](_icc.gif)                                |
84 | 81, 77, 82, 83 | syl3anc 1219 |
. . . . 5
                            
   
        
 
  ![[,] [,]](_icc.gif)   
                            |
85 | | simpl3r 1044 |
. . . . . 6
                            
   
            |
86 | | brbtwn 23298 |
. . . . . 6
     
                ![[,] [,]](_icc.gif)                                |
87 | 85, 78, 82, 86 | syl3anc 1219 |
. . . . 5
                            
   
             ![[,] [,]](_icc.gif)   
                            |
88 | 80, 84, 87 | 3anbi123d 1290 |
. . . 4
                            
   
             
        ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)                                 |
89 | | r19.26-3 2957 |
. . . . . . 7
 
                                                                  
 
                         
                         
                            |
90 | 89 | rexbii 2862 |
. . . . . 6
    ![[,] [,]](_icc.gif)   
                                                                  
   ![[,] [,]](_icc.gif)                                                                                     |
91 | 90 | 2rexbii 2863 |
. . . . 5
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                                                  
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                                     |
92 | | 3reeanv 2995 |
. . . . 5
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                        
                         
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
93 | 91, 92 | bitri 249 |
. . . 4
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                                                  
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
94 | 88, 93 | syl6bbr 263 |
. . 3
                            
   
             
       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                          |
95 | 94 | 2rexbidva 2874 |
. 2
  
   
         
                         

  
                   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                          |
96 | 56, 75, 95 | 3imtr4d 268 |
1
  
   
         
             

  

              

  
       |