Step | Hyp | Ref
| Expression |
1 | | prmunb 14937 |
. 2
    |
2 | | eqid 2471 |
. . . . 5

    
   |
3 | 2 | prmgaplem4 15103 |
. . . 4
 
   
     
     |
4 | | breq2 4399 |
. . . . . . . . 9
 
   |
5 | | breq1 4398 |
. . . . . . . . 9
 
   |
6 | 4, 5 | anbi12d 725 |
. . . . . . . 8
  
 
    |
7 | 6 | elrab 3184 |
. . . . . . 7
 
  

     |
8 | | simplrl 778 |
. . . . . . . . . 10
    

      
   
  |
9 | | simprrl 782 |
. . . . . . . . . . 11
           |
10 | 9 | adantr 472 |
. . . . . . . . . 10
    

      
   
  |
11 | | simpll 768 |
. . . . . . . . . . . . . . . . . 18
     

        ..^ 
  |
12 | | elfzo2 11950 |
. . . . . . . . . . . . . . . . . . . 20
    ..^           |
13 | | eluz2 11188 |
. . . . . . . . . . . . . . . . . . . . . 22
    
          |
14 | | nnz 10983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
15 | | prmz 14705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

  |
16 | | zltp1le 11010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
       |
17 | 14, 15, 16 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
       |
18 | 17 | exbiri 634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
    |
19 | 18 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
    
    |
20 | 19 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            
    |
21 | 20 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
 
    |
22 | 21 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       

    
   |
23 | 22 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
    
 
    
   |
24 | 23 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
 
          
   |
25 | 24 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     

              |
26 | | prmnn 14704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39

  |
27 | 26 | nnred 10646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38

  |
28 | 27 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       |
29 | | prmnn 14704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40

  |
30 | 29 | nnred 10646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39

  |
31 | 30 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
     |
32 | 31 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
  |
33 | | prmnn 14704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39

  |
34 | 33 | nnred 10646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38

  |
35 | 34 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
  |
36 | | ltleletr 9744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
  
    |
37 | 28, 32, 35, 36 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
      

   |
38 | 37 | exp4b 618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35

   

     |
39 | 38 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
     
     |
40 | 39 | expdcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33


 
 

      |
41 | 40 | com45 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32


 
 

      |
42 | 41 | com14 90 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      
      |
43 | 42 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      


      |
44 | 43 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       


     |
45 | 44 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          
    |
46 | 45 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          

   |
47 | 46 | adantld 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
    
 
   |
48 | 47 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     

              |
49 | 25, 48 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     

                |
50 | 49 | exp41 621 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
 
    
       |
51 | 50 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . . . . . 22
   

       
 
    
       |
52 | 13, 51 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . 21
    
 


          
       |
53 | 52 | 3imp 1224 |
. . . . . . . . . . . . . . . . . . . 20
     
       

    
     |
54 | 12, 53 | sylbi 200 |
. . . . . . . . . . . . . . . . . . 19
    ..^
          
     |
55 | 54 | impcom 437 |
. . . . . . . . . . . . . . . . . 18
     

        ..^ 
    |
56 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
57 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
58 | 56, 57 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . 19
  
 
    |
59 | 58 | elrab 3184 |
. . . . . . . . . . . . . . . . . 18
 
  

     |
60 | 11, 55, 59 | sylanbrc 677 |
. . . . . . . . . . . . . . . . 17
     

        ..^ 
      |
61 | | elfzolt2 11956 |
. . . . . . . . . . . . . . . . . 18
    ..^
  |
62 | 30 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . 21
           |
63 | | ltnle 9731 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
   |
64 | 63 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
65 | 27, 62, 64 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . 20
          

   |
66 | 65 | imp 436 |
. . . . . . . . . . . . . . . . . . 19
     

        |
67 | 66 | pm2.21d 109 |
. . . . . . . . . . . . . . . . . 18
     

      
   |
68 | 61, 67 | sylan2 482 |
. . . . . . . . . . . . . . . . 17
     

        ..^ 

   |
69 | 60, 68 | embantd 55 |
. . . . . . . . . . . . . . . 16
     

        ..^ 
  
   
   |
70 | 69 | ex 441 |
. . . . . . . . . . . . . . 15
          
    ..^   
   
    |
71 | 70 | com23 80 |
. . . . . . . . . . . . . 14
          
  
        ..^
    |
72 | 71 | ex 441 |
. . . . . . . . . . . . 13

           
        ..^
     |
73 | | df-nel 2644 |
. . . . . . . . . . . . . 14

  |
74 | | ax-1 6 |
. . . . . . . . . . . . . . . 16

    ..^
   |
75 | 74 | a1d 25 |
. . . . . . . . . . . . . . 15

  
        ..^
    |
76 | 75 | a1d 25 |
. . . . . . . . . . . . . 14

           
        ..^
     |
77 | 73, 76 | sylbir 218 |
. . . . . . . . . . . . 13
    

      
        ..^
     |
78 | 72, 77 | pm2.61i 169 |
. . . . . . . . . . . 12
           
        ..^
    |
79 | 78 | ralimdv2 2804 |
. . . . . . . . . . 11
            
       ..^     |
80 | 79 | imp 436 |
. . . . . . . . . 10
    

      
   
    ..^    |
81 | 8, 10, 80 | jca32 544 |
. . . . . . . . 9
    

      
   

     ..^      |
82 | 81 | ex 441 |
. . . . . . . 8
            
         ..^       |
83 | 82 | ex 441 |
. . . . . . 7
 
   
 
 
    

     ..^        |
84 | 7, 83 | syl5bi 225 |
. . . . . 6
 
  
         
  
 
 ..^        |
85 | 84 | impd 438 |
. . . . 5
 
         
   

     ..^       |
86 | 85 | reximdv2 2855 |
. . . 4
 
  

    
    
 
    ..^      |
87 | 3, 86 | mpd 15 |
. . 3
 
  
    ..^     |
88 | 87 | rexlimdv3a 2873 |
. 2
  
 
    ..^      |
89 | 1, 88 | mpd 15 |
1
  
    ..^     |