Step | Hyp | Ref
| Expression |
1 | | isbndx 32107 |
. . 3
           

           |
2 | 1 | anbi1i 700 |
. 2
      
 
      
            |
3 | | anass 654 |
. 2
       

          
       

            |
4 | | r19.2z 3857 |
. . . . 5
  

        

           |
5 | 4 | ancoms 455 |
. . . 4
   
         

          |
6 | | oveq1 6295 |
. . . . . . . 8
                   |
7 | 6 | eqeq2d 2460 |
. . . . . . 7
 
       
           |
8 | | oveq2 6296 |
. . . . . . . 8
                   |
9 | 8 | eqeq2d 2460 |
. . . . . . 7
 
       
           |
10 | 7, 9 | cbvrex2v 3027 |
. . . . . 6
  
        

          |
11 | | 2rp 11304 |
. . . . . . . . . . . . 13
 |
12 | | rpmulcl 11321 |
. . . . . . . . . . . . 13
       |
13 | 11, 12 | mpan 675 |
. . . . . . . . . . . 12

    |
14 | 13 | ad2antll 734 |
. . . . . . . . . . 11
              |
15 | 14 | ad2antrr 731 |
. . . . . . . . . 10
         
  
        
    |
16 | | rpcn 11307 |
. . . . . . . . . . . . . . . . . . 19

  |
17 | | 2cnd 10679 |
. . . . . . . . . . . . . . . . . . 19

  |
18 | | 2ne0 10699 |
. . . . . . . . . . . . . . . . . . . 20
 |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19

  |
20 | | divcan3 10291 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
21 | 20 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . 19
 
       |
22 | 16, 17, 19, 21 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . 18

      |
23 | 22 | oveq2d 6304 |
. . . . . . . . . . . . . . . . 17

                      |
24 | 23 | eqeq2d 2460 |
. . . . . . . . . . . . . . . 16

        
               |
25 | 24 | biimpd 211 |
. . . . . . . . . . . . . . 15

                        |
26 | 25 | ad2antll 734 |
. . . . . . . . . . . . . 14
          
                       |
27 | 26 | adantr 467 |
. . . . . . . . . . . . 13
       

 
         
               |
28 | 27 | imp 431 |
. . . . . . . . . . . 12
         
  
        
              |
29 | | simpr 463 |
. . . . . . . . . . . . 13
         
  
            
              |
30 | | eleq2 2517 |
. . . . . . . . . . . . . . . 16
             
               |
31 | 30 | biimpac 489 |
. . . . . . . . . . . . . . 15
 
            
              |
32 | | 2re 10676 |
. . . . . . . . . . . . . . . . . . 19
 |
33 | | rpre 11305 |
. . . . . . . . . . . . . . . . . . 19

  |
34 | | remulcl 9621 |
. . . . . . . . . . . . . . . . . . 19
 
     |
35 | 32, 33, 34 | sylancr 668 |
. . . . . . . . . . . . . . . . . 18

    |
36 | | blhalf 21413 |
. . . . . . . . . . . . . . . . . . 19
       
   
                                      |
37 | 36 | expr 619 |
. . . . . . . . . . . . . . . . . 18
       
                                          |
38 | 35, 37 | sylan2 477 |
. . . . . . . . . . . . . . . . 17
       
                                        |
39 | 38 | anasss 652 |
. . . . . . . . . . . . . . . 16
                                                |
40 | 39 | imp 431 |
. . . . . . . . . . . . . . 15
       

 
                                     |
41 | 31, 40 | sylan2 477 |
. . . . . . . . . . . . . 14
       

  
             
                        |
42 | 41 | anassrs 653 |
. . . . . . . . . . . . 13
         
  
            
                        |
43 | 29, 42 | eqsstrd 3465 |
. . . . . . . . . . . 12
         
  
            
            |
44 | 28, 43 | syldan 473 |
. . . . . . . . . . 11
         
  
        
            |
45 | 13 | adantl 468 |
. . . . . . . . . . . . . 14
 
     |
46 | | rpxr 11306 |
. . . . . . . . . . . . . . . 16
  
    |
47 | | blssm 21426 |
. . . . . . . . . . . . . . . 16
                      |
48 | 46, 47 | syl3an3 1302 |
. . . . . . . . . . . . . . 15
                      |
49 | 48 | 3expa 1207 |
. . . . . . . . . . . . . 14
       
                |
50 | 45, 49 | sylan2 477 |
. . . . . . . . . . . . 13
       
 
              |
51 | 50 | an32s 812 |
. . . . . . . . . . . 12
       

 
             |
52 | 51 | adantr 467 |
. . . . . . . . . . 11
         
  
        
            |
53 | 44, 52 | eqssd 3448 |
. . . . . . . . . 10
         
  
        
            |
54 | | oveq2 6296 |
. . . . . . . . . . . 12
                       |
55 | 54 | eqeq2d 2460 |
. . . . . . . . . . 11
   
       
             |
56 | 55 | rspcev 3149 |
. . . . . . . . . 10
               
          |
57 | 15, 53, 56 | syl2anc 666 |
. . . . . . . . 9
         
  
        
           |
58 | 57 | ex 436 |
. . . . . . . 8
       

 
          
           |
59 | 58 | ralrimdva 2805 |
. . . . . . 7
          
        
            |
60 | 59 | rexlimdvva 2885 |
. . . . . 6
       

         
           |
61 | 10, 60 | syl5bi 221 |
. . . . 5
       

         
           |
62 | | rexn0 3871 |
. . . . . 6
  
          |
63 | 62 | a1i 11 |
. . . . 5
       

           |
64 | 61, 63 | jcad 536 |
. . . 4
       

         
             |
65 | 5, 64 | impbid2 208 |
. . 3
                  

            |
66 | 65 | pm5.32i 642 |
. 2
        
          
      

           |
67 | 2, 3, 66 | 3bitri 275 |
1
      
      

           |