Step | Hyp | Ref
| Expression |
1 | | r2al 2766 |
. . . . . . 7
 

       
                  |
2 | | simpl 459 |
. . . . . . . . . . 11
 
   |
3 | 2 | anim1i 572 |
. . . . . . . . . 10
  

 
   |
4 | 3 | imim1i 60 |
. . . . . . . . 9
  

                         |
5 | 4 | expd 438 |
. . . . . . . 8
  

                         |
6 | 5 | 2alimi 1685 |
. . . . . . 7
      
         
                    |
7 | 1, 6 | sylbi 199 |
. . . . . 6
 

                            |
8 | | r2al 2766 |
. . . . . 6
 

               


            |
9 | 7, 8 | sylibr 216 |
. . . . 5
 

        


           |
10 | | elequ1 1894 |
. . . . . . . . . . . 12
 
   |
11 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
12 | 11 | eqeq2d 2461 |
. . . . . . . . . . . . 13
         
           |
13 | 12 | notbid 296 |
. . . . . . . . . . . 12
         
           |
14 | 10, 13 | imbi12d 322 |
. . . . . . . . . . 11
            
            |
15 | 14 | cbvralv 3019 |
. . . . . . . . . 10
 
          

           |
16 | 15 | ralbii 2819 |
. . . . . . . . 9
 

          


           |
17 | | elequ2 1901 |
. . . . . . . . . . . 12
 
   |
18 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
19 | 18 | eqeq1d 2453 |
. . . . . . . . . . . . 13
         
           |
20 | 19 | notbid 296 |
. . . . . . . . . . . 12
         
           |
21 | 17, 20 | imbi12d 322 |
. . . . . . . . . . 11
            
            |
22 | 21 | ralbidv 2827 |
. . . . . . . . . 10
  

          
            |
23 | 22 | cbvralv 3019 |
. . . . . . . . 9
 

          


           |
24 | | elequ1 1894 |
. . . . . . . . . . . . 13
 
   |
25 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
26 | 25 | eqeq2d 2461 |
. . . . . . . . . . . . . 14
         
           |
27 | 26 | notbid 296 |
. . . . . . . . . . . . 13
         
           |
28 | 24, 27 | imbi12d 322 |
. . . . . . . . . . . 12
  
         
            |
29 | 28 | cbvralv 3019 |
. . . . . . . . . . 11
 
          

           |
30 | 29 | ralbii 2819 |
. . . . . . . . . 10
 

          


           |
31 | | elequ2 1901 |
. . . . . . . . . . . . 13
 
   |
32 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
33 | 32 | eqeq1d 2453 |
. . . . . . . . . . . . . 14
         
           |
34 | 33 | notbid 296 |
. . . . . . . . . . . . 13
         
           |
35 | 31, 34 | imbi12d 322 |
. . . . . . . . . . . 12
  
         
            |
36 | 35 | ralbidv 2827 |
. . . . . . . . . . 11
  

          
            |
37 | 36 | cbvralv 3019 |
. . . . . . . . . 10
 

          


           |
38 | 30, 37 | bitri 253 |
. . . . . . . . 9
 

          


           |
39 | 16, 23, 38 | 3bitri 275 |
. . . . . . . 8
 

          


           |
40 | | ralcom2 2955 |
. . . . . . . 8
 

           

           |
41 | 39, 40 | sylbi 199 |
. . . . . . 7
 

           

           |
42 | 41 | ancri 555 |
. . . . . 6
 

           


          
             |
43 | | r19.26-2 2918 |
. . . . . 6
 

 
                       
          
             |
44 | 42, 43 | sylibr 216 |
. . . . 5
 

           
 
                      |
45 | 9, 44 | syl 17 |
. . . 4
 

        

           
            |
46 | | fvres 5879 |
. . . . . . . . . . 11
             |
47 | | fvres 5879 |
. . . . . . . . . . 11
             |
48 | 46, 47 | eqeqan12d 2467 |
. . . . . . . . . 10
 
         
   
           |
49 | 48 | ad2antrl 734 |
. . . . . . . . 9
 
 

           
                    
   
           |
50 | | ssel 3426 |
. . . . . . . . . . . 12

    |
51 | | ssel 3426 |
. . . . . . . . . . . 12

    |
52 | 50, 51 | anim12d 566 |
. . . . . . . . . . 11

 
      |
53 | | pm3.48 844 |
. . . . . . . . . . . . . 14
  
                                            |
54 | | oridm 517 |
. . . . . . . . . . . . . . 15
                  
          |
55 | | eqcom 2458 |
. . . . . . . . . . . . . . . . 17
        
          |
56 | 55 | notbii 298 |
. . . . . . . . . . . . . . . 16
        
          |
57 | 56 | orbi1i 523 |
. . . . . . . . . . . . . . 15
                  
                    |
58 | 54, 57 | bitr3i 255 |
. . . . . . . . . . . . . 14
        
                    |
59 | 53, 58 | syl6ibr 231 |
. . . . . . . . . . . . 13
  
                                  |
60 | 59 | con2d 119 |
. . . . . . . . . . . 12
  
                            
     |
61 | | eloni 5433 |
. . . . . . . . . . . . 13
   |
62 | | eloni 5433 |
. . . . . . . . . . . . 13
   |
63 | | ordtri3 5459 |
. . . . . . . . . . . . . 14
   
     |
64 | 63 | biimprd 227 |
. . . . . . . . . . . . 13
     
   |
65 | 61, 62, 64 | syl2an 480 |
. . . . . . . . . . . 12
 
       |
66 | 60, 65 | syl9r 74 |
. . . . . . . . . . 11
 
                                
    |
67 | 52, 66 | syl6 34 |
. . . . . . . . . 10

 
                                
     |
68 | 67 | imp32 435 |
. . . . . . . . 9
 
 

           
                    
   |
69 | 49, 68 | sylbid 219 |
. . . . . . . 8
 
 

           
                    
       |
70 | 69 | exp32 610 |
. . . . . . 7

 
                                
         |
71 | 70 | a2d 29 |
. . . . . 6

  

           
          
 
         
         |
72 | 71 | 2alimdv 1765 |
. . . . 5

      
  
                          

            
     |
73 | | r2al 2766 |
. . . . 5
 

 
                         

           
             |
74 | | r2al 2766 |
. . . . 5
 

        
    
               
        |
75 | 72, 73, 74 | 3imtr4g 274 |
. . . 4

 

 
                     
        
        |
76 | 45, 75 | syl5 33 |
. . 3

 

        

            
    |
77 | 76 | imdistani 696 |
. 2
 


           
        
        |
78 | | tz7.48.1 |
. . . 4
 |
79 | | fnssres 5689 |
. . . 4
       |
80 | 78, 79 | mpan 676 |
. . 3

    |
81 | | dffn2 5730 |
. . . 4
 

        |
82 | | dff13 6159 |
. . . . . 6
 
    
           
         
    |
83 | | df-f1 5587 |
. . . . . 6
 
    
        
    |
84 | 82, 83 | bitr3i 255 |
. . . . 5
         
        
              
    |
85 | 84 | simprbi 466 |
. . . 4
         
        
     
     |
86 | 81, 85 | sylanb 475 |
. . 3
    

        
     
     |
87 | 80, 86 | sylan 474 |
. 2
 


        
     
     |
88 | 77, 87 | syl 17 |
1
 


              |