Step | Hyp | Ref
| Expression |
1 | | breq1 4419 |
. . . . . . . . . . . 12
 
   |
2 | 1 | ralbidv 2839 |
. . . . . . . . . . 11
  

   |
3 | 2 | imbi2d 322 |
. . . . . . . . . 10
          

      




    |
4 | | breq1 4419 |
. . . . . . . . . . . 12
 
   |
5 | 4 | ralbidv 2839 |
. . . . . . . . . . 11
  

   |
6 | 5 | imbi2d 322 |
. . . . . . . . . 10
          

      




    |
7 | | breq1 4419 |
. . . . . . . . . . . 12
   
     |
8 | 7 | ralbidv 2839 |
. . . . . . . . . . 11
    

     |
9 | 8 | imbi2d 322 |
. . . . . . . . . 10
            

      




      |
10 | | breq1 4419 |
. . . . . . . . . . . 12
 
   |
11 | 10 | ralbidv 2839 |
. . . . . . . . . . 11
  

   |
12 | 11 | imbi2d 322 |
. . . . . . . . . 10
          

      




    |
13 | | ssel 3438 |
. . . . . . . . . . . . . 14
    

       |
14 | | eluzle 11200 |
. . . . . . . . . . . . . 14
    
  |
15 | 13, 14 | syl6 34 |
. . . . . . . . . . . . 13
    

   |
16 | 15 | ralrimiv 2812 |
. . . . . . . . . . . 12
    

  |
17 | 16 | adantr 471 |
. . . . . . . . . . 11
 
     
 
  |
18 | 17 | a1i 11 |
. . . . . . . . . 10
        
 
   |
19 | | uzssz 11207 |
. . . . . . . . . . . . 13
     |
20 | | sstr 3452 |
. . . . . . . . . . . . 13
 
        
  |
21 | 19, 20 | mpan2 682 |
. . . . . . . . . . . 12
    
  |
22 | | eluzelz 11197 |
. . . . . . . . . . . . 13
    
  |
23 | | breq1 4419 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
24 | 23 | ralbidv 2839 |
. . . . . . . . . . . . . . . . . . 19
  

   |
25 | 24 | rspcev 3162 |
. . . . . . . . . . . . . . . . . 18
    

  |
26 | 25 | expcom 441 |
. . . . . . . . . . . . . . . . 17
 



   |
27 | 26 | con3rr3 143 |
. . . . . . . . . . . . . . . 16
  
 
   |
28 | | ssel2 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
29 | | zre 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
30 | | zre 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
31 | | letri3 9745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
  
    |
32 | 29, 30, 31 | syl2an 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  
    |
33 | | zleltp1 11016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
       |
34 | | peano2re 9832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
35 | 29, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     |
36 | | ltnle 9739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  
    
     |
37 | 30, 35, 36 | syl2an 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
     
   |
38 | 33, 37 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   
   |
39 | 38 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   
   |
40 | 39 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  
 
      |
41 | 32, 40 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
         |
42 | 28, 41 | sylan2 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
 


      |
43 | | eleq1a 2535 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
44 | 43 | ad2antll 740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
 

   |
45 | 42, 44 | sylbird 243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
 
 
 
    |
46 | 45 | expd 442 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
 

 

    |
47 | | con1 133 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
     |
48 | 46, 47 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 


      |
49 | 48 | com23 81 |
. . . . . . . . . . . . . . . . . . . . 21
  
 


      |
50 | 49 | exp32 614 |
. . . . . . . . . . . . . . . . . . . 20
   

        |
51 | 50 | com34 86 |
. . . . . . . . . . . . . . . . . . 19
  
   
      |
52 | 51 | imp41 602 |
. . . . . . . . . . . . . . . . . 18
    
  
     |
53 | 52 | ralimdva 2808 |
. . . . . . . . . . . . . . . . 17
  
 
 

     |
54 | 53 | ex 440 |
. . . . . . . . . . . . . . . 16
   
 

      |
55 | 27, 54 | sylan9r 668 |
. . . . . . . . . . . . . . 15
  
   
 
 

      |
56 | 55 | pm2.43d 50 |
. . . . . . . . . . . . . 14
  
   
 

     |
57 | 56 | expl 628 |
. . . . . . . . . . . . 13
    
    

    |
58 | 22, 57 | syl 17 |
. . . . . . . . . . . 12
    
   
  

      |
59 | 21, 58 | sylani 664 |
. . . . . . . . . . 11
    
     



 

      |
60 | 59 | a2d 29 |
. . . . . . . . . 10
    
        
 
         

      |
61 | 3, 6, 9, 12, 18, 60 | uzind4 11246 |
. . . . . . . . 9
    
     




   |
62 | | breq1 4419 |
. . . . . . . . . . . . . 14
 
   |
63 | 62 | ralbidv 2839 |
. . . . . . . . . . . . 13
  

   |
64 | 63 | rspcev 3162 |
. . . . . . . . . . . 12
    

  |
65 | 64 | expcom 441 |
. . . . . . . . . . 11
 



   |
66 | 65 | con3rr3 143 |
. . . . . . . . . 10
  
 
   |
67 | 66 | adantl 472 |
. . . . . . . . 9
 
     
  
   |
68 | 61, 67 | sylcom 30 |
. . . . . . . 8
    
     



   |
69 | | ssel 3438 |
. . . . . . . . . 10
    

       |
70 | 69 | con3rr3 143 |
. . . . . . . . 9
         
   |
71 | 70 | adantrd 474 |
. . . . . . . 8
            

   |
72 | 68, 71 | pm2.61i 169 |
. . . . . . 7
 
     

  |
73 | 72 | ex 440 |
. . . . . 6
    
  
   |
74 | 73 | alrimdv 1786 |
. . . . 5
    
  

   |
75 | | eq0 3759 |
. . . . 5

   |
76 | 74, 75 | syl6ibr 235 |
. . . 4
    
  
   |
77 | 76 | necon1ad 2653 |
. . 3
    



   |
78 | 77 | imp 435 |
. 2
 
     

  |
79 | | breq2 4420 |
. . . 4
 
   |
80 | 79 | cbvralv 3031 |
. . 3
 
   |
81 | 80 | rexbii 2901 |
. 2
  
 
  |
82 | 78, 81 | sylib 201 |
1
 
     

  |