Step | Hyp | Ref
| Expression |
1 | | simpl21 1035 |
. . . . . 6
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
      |
2 | | simpl22 1036 |
. . . . . 6
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
      |
3 | 1, 2 | jca 519 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
    
       |
4 | | simpl23 1037 |
. . . . . 6
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
      |
5 | | simpl3r 1013 |
. . . . . 6
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
      |
6 | 4, 5 | jca 519 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
    
       |
7 | | simprll 739 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
  ![[,] [,]](_icc.gif)    |
8 | | simprlr 740 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
  ![[,] [,]](_icc.gif)    |
9 | | simp21 990 |
. . . . . . . . . . . . . . . . . . 19
  
   
         
         
      |
10 | 9 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . 18
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
      |
11 | | fveecn 25745 |
. . . . . . . . . . . . . . . . . 18
     
           |
12 | 10, 11 | sylan 458 |
. . . . . . . . . . . . . . . . 17
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
           |
13 | | simp3r 986 |
. . . . . . . . . . . . . . . . . . 19
  
   
         
         
      |
14 | 13 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . 18
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
      |
15 | | fveecn 25745 |
. . . . . . . . . . . . . . . . . 18
     
           |
16 | 14, 15 | sylan 458 |
. . . . . . . . . . . . . . . . 17
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
           |
17 | | mulid2 9045 |
. . . . . . . . . . . . . . . . . . 19
                 |
18 | | mul02 9200 |
. . . . . . . . . . . . . . . . . . 19
             |
19 | 17, 18 | oveqan12d 6059 |
. . . . . . . . . . . . . . . . . 18
                                 |
20 | | addid1 9202 |
. . . . . . . . . . . . . . . . . . 19
                 |
21 | 20 | adantr 452 |
. . . . . . . . . . . . . . . . . 18
                       |
22 | 19, 21 | eqtrd 2436 |
. . . . . . . . . . . . . . . . 17
                               |
23 | 12, 16, 22 | syl2anc 643 |
. . . . . . . . . . . . . . . 16
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         |
24 | | oveq2 6048 |
. . . . . . . . . . . . . . . . . . . . 21
       |
25 | | ax-1cn 9004 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
26 | 25 | subid1i 9328 |
. . . . . . . . . . . . . . . . . . . . 21
   |
27 | 24, 26 | syl6eq 2452 |
. . . . . . . . . . . . . . . . . . . 20
     |
28 | 27 | oveq1d 6055 |
. . . . . . . . . . . . . . . . . . 19
                 |
29 | | oveq1 6047 |
. . . . . . . . . . . . . . . . . . 19
               |
30 | 28, 29 | oveq12d 6058 |
. . . . . . . . . . . . . . . . . 18
                                 |
31 | 30 | eqeq1d 2412 |
. . . . . . . . . . . . . . . . 17
                     
                     |
32 | 31 | ad2antlr 708 |
. . . . . . . . . . . . . . . 16
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                               |
33 | 23, 32 | mpbird 224 |
. . . . . . . . . . . . . . 15
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                           |
34 | 33 | eqeq2d 2415 |
. . . . . . . . . . . . . 14
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                     |
35 | | eqcom 2406 |
. . . . . . . . . . . . . 14
        
          |
36 | 34, 35 | syl6bb 253 |
. . . . . . . . . . . . 13
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                     |
37 | 36 | biimpd 199 |
. . . . . . . . . . . 12
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
           |
38 | 37 | adantrd 455 |
. . . . . . . . . . 11
     
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                           |
39 | 38 | ralimdva 2744 |
. . . . . . . . . 10
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                                                                       |
40 | 39 | impancom 428 |
. . . . . . . . 9
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                
                 |
41 | 9 | ad2antrr 707 |
. . . . . . . . . 10
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                      |
42 | | simp3l 985 |
. . . . . . . . . . 11
  
   
         
         
      |
43 | 42 | ad2antrr 707 |
. . . . . . . . . 10
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                      |
44 | | eqeefv 25746 |
. . . . . . . . . 10
     
      
                |
45 | 41, 43, 44 | syl2anc 643 |
. . . . . . . . 9
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                                  |
46 | 40, 45 | sylibrd 226 |
. . . . . . . 8
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                
   |
47 | 46 | necon3d 2605 |
. . . . . . 7
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                                                
   |
48 | 47 | impr 603 |
. . . . . 6
            
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     
                                                   |
49 | 48 | anasss 629 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
  |
50 | | eqtr2 2422 |
. . . . . . . 8
                                                                             |
51 | 50 | ralimi 2741 |
. . . . . . 7
 
                                               
                                       |
52 | 51 | adantr 452 |
. . . . . 6
                                                                                           |
53 | 52 | ad2antll 710 |
. . . . 5
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
                                        |
54 | | axeuclidlem 25805 |
. . . . 5
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
                                      
               ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                         |
55 | 3, 6, 7, 8, 49, 53, 54 | syl231anc 1204 |
. . . 4
                                ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                                 
               ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                         |
56 | 55 | exp32 589 |
. . 3
  
   
         
              ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                                                                     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                           |
57 | 56 | rexlimdvv 2796 |
. 2
  
   
         
              ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                          |
58 | | brbtwn 25742 |
. . . . 5
     
             
  ![[,] [,]](_icc.gif)                                |
59 | 42, 9, 13, 58 | syl3anc 1184 |
. . . 4
  
   
         
                 ![[,] [,]](_icc.gif)                                |
60 | | simp22 991 |
. . . . 5
  
   
         
         
      |
61 | | simp23 992 |
. . . . 5
  
   
         
         
      |
62 | | brbtwn 25742 |
. . . . 5
     
             
  ![[,] [,]](_icc.gif)                                |
63 | 42, 60, 61, 62 | syl3anc 1184 |
. . . 4
  
   
         
                 ![[,] [,]](_icc.gif)                                |
64 | 59, 63 | 3anbi12d 1255 |
. . 3
  
   
         
             

  
     ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)                                 |
65 | | r19.26 2798 |
. . . . . . 7
 
                                              
 
                         
                            |
66 | 65 | 2rexbii 2693 |
. . . . . 6
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                              
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                           |
67 | | reeanv 2835 |
. . . . . 6
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                        
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
68 | 66, 67 | bitri 241 |
. . . . 5
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                              
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
69 | 68 | anbi1i 677 |
. . . 4
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                   
  
  ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)   
                             |
70 | | r19.41v 2821 |
. . . . . 6
    ![[,] [,]](_icc.gif)                                                    
 
  ![[,] [,]](_icc.gif)   
                                                  |
71 | 70 | rexbii 2691 |
. . . . 5
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                    
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                                                      |
72 | | r19.41v 2821 |
. . . . 5
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                                                   
 
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                                  |
73 | 71, 72 | bitri 241 |
. . . 4
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                    
 
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                                  |
74 | | df-3an 938 |
. . . 4
     ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)   
                         
  
  ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)   
                             |
75 | 69, 73, 74 | 3bitr4i 269 |
. . 3
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                    
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
76 | 64, 75 | syl6bbr 255 |
. 2
  
   
         
             

  
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                        |
77 | | simpl22 1036 |
. . . . . 6
                            
   
            |
78 | | simpl21 1035 |
. . . . . 6
                            
   
            |
79 | | simprl 733 |
. . . . . 6
                            
   
            |
80 | | brbtwn 25742 |
. . . . . 6
     
             
  ![[,] [,]](_icc.gif)                                |
81 | 77, 78, 79, 80 | syl3anc 1184 |
. . . . 5
                            
   
        
 
  ![[,] [,]](_icc.gif)   
                            |
82 | | simpl23 1037 |
. . . . . 6
                            
   
            |
83 | | simprr 734 |
. . . . . 6
                            
   
            |
84 | | brbtwn 25742 |
. . . . . 6
     
                ![[,] [,]](_icc.gif)                                |
85 | 82, 78, 83, 84 | syl3anc 1184 |
. . . . 5
                            
   
        
 
  ![[,] [,]](_icc.gif)   
                            |
86 | | simpl3r 1013 |
. . . . . 6
                            
   
            |
87 | | brbtwn 25742 |
. . . . . 6
     
                ![[,] [,]](_icc.gif)                                |
88 | 86, 79, 83, 87 | syl3anc 1184 |
. . . . 5
                            
   
             ![[,] [,]](_icc.gif)   
                            |
89 | 81, 85, 88 | 3anbi123d 1254 |
. . . 4
                            
   
             
        ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)                                 |
90 | | r19.26-3 2800 |
. . . . . . 7
 
                                                                  
 
                         
                         
                            |
91 | 90 | rexbii 2691 |
. . . . . 6
    ![[,] [,]](_icc.gif)   
                                                                  
   ![[,] [,]](_icc.gif)                                                                                     |
92 | 91 | 2rexbii 2693 |
. . . . 5
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                                                  
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                                     |
93 | | 3reeanv 2836 |
. . . . 5
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                        
                         
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
94 | 92, 93 | bitri 241 |
. . . 4
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                                                  
 
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                         
  ![[,] [,]](_icc.gif)   
                            |
95 | 89, 94 | syl6bbr 255 |
. . 3
                            
   
             
       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                          |
96 | 95 | 2rexbidva 2707 |
. 2
  
   
         
                         

  
                   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                                                          |
97 | 57, 76, 96 | 3imtr4d 260 |
1
  
   
         
             

  

              

  
       |