Step | Hyp | Ref
| Expression |
1 | | simprl 529 |
. . . 4
  
 
  |
2 | | elq 9611 |
. . . 4

      |
3 | 1, 2 | sylib 122 |
. . 3
  
  
     |
4 | | simpr 110 |
. . . . . . . . . . 11
    

 

   

   |
5 | | simprr 531 |
. . . . . . . . . . . . 13
  
    |
6 | 5 | ad3antrrr 492 |
. . . . . . . . . . . 12
    

 

   
  |
7 | 1 | ad3antrrr 492 |
. . . . . . . . . . . . 13
    

 

   
  |
8 | | 0z 9253 |
. . . . . . . . . . . . . 14
 |
9 | | zq 9615 |
. . . . . . . . . . . . . 14
   |
10 | 8, 9 | mp1i 10 |
. . . . . . . . . . . . 13
    

 

   
  |
11 | | qapne 9628 |
. . . . . . . . . . . . 13
 
  #    |
12 | 7, 10, 11 | syl2anc 411 |
. . . . . . . . . . . 12
    

 

   
 #    |
13 | 6, 12 | mpbird 167 |
. . . . . . . . . . 11
    

 

   
#   |
14 | 4, 13 | eqbrtrrd 4024 |
. . . . . . . . . 10
    

 

   
  #   |
15 | | simpllr 534 |
. . . . . . . . . . . 12
    

 

   
  |
16 | 15 | zcnd 9365 |
. . . . . . . . . . 11
    

 

   
  |
17 | | nnz 9261 |
. . . . . . . . . . . . . 14
   |
18 | 17 | adantl 277 |
. . . . . . . . . . . . 13
      

   |
19 | 18 | adantr 276 |
. . . . . . . . . . . 12
    

 

   
  |
20 | 19 | zcnd 9365 |
. . . . . . . . . . 11
    

 

   
  |
21 | | simplr 528 |
. . . . . . . . . . . 12
    

 

   
  |
22 | 21 | nnap0d 8954 |
. . . . . . . . . . 11
    

 

   
#   |
23 | 16, 20, 22 | divap0bd 8748 |
. . . . . . . . . 10
    

 

   
 #   #    |
24 | 14, 23 | mpbird 167 |
. . . . . . . . 9
    

 

   
#   |
25 | | 0zd 9254 |
. . . . . . . . . 10
    

 

   
  |
26 | | zapne 9316 |
. . . . . . . . . 10
 
  #    |
27 | 15, 25, 26 | syl2anc 411 |
. . . . . . . . 9
    

 

   
 #    |
28 | 24, 27 | mpbid 147 |
. . . . . . . 8
    

 

   
  |
29 | 28 | ex 115 |
. . . . . . 7
      

   
   |
30 | 29 | adantrd 279 |
. . . . . . . 8
      

           |
31 | 30 | exlimdv 1819 |
. . . . . . 7
      

         
   |
32 | | prmuz2 12114 |
. . . . . . . . . . . . . . 15

      |
33 | 32 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
      

       |
34 | 33 | adantr 276 |
. . . . . . . . . . . . 13
    

 

 
      |
35 | | simpllr 534 |
. . . . . . . . . . . . 13
    

 

 
  |
36 | | simpr 110 |
. . . . . . . . . . . . 13
    

 

 
  |
37 | | eqid 2177 |
. . . . . . . . . . . . . . 15
     
    
  |
38 | | pcval.1 |
. . . . . . . . . . . . . . 15
           |
39 | 37, 38 | pcprecl 12272 |
. . . . . . . . . . . . . 14
         
       |
40 | 39 | simpld 112 |
. . . . . . . . . . . . 13
           |
41 | 34, 35, 36, 40 | syl12anc 1236 |
. . . . . . . . . . . 12
    

 

 
  |
42 | 41 | nn0zd 9362 |
. . . . . . . . . . 11
    

 

 
  |
43 | | nnne0 8936 |
. . . . . . . . . . . . . . . 16
   |
44 | 43 | adantl 277 |
. . . . . . . . . . . . . . 15
      

   |
45 | | eqid 2177 |
. . . . . . . . . . . . . . . 16
     
    
  |
46 | | pcval.2 |
. . . . . . . . . . . . . . . 16
           |
47 | 45, 46 | pcprecl 12272 |
. . . . . . . . . . . . . . 15
         
       |
48 | 33, 18, 44, 47 | syl12anc 1236 |
. . . . . . . . . . . . . 14
      

 
       |
49 | 48 | simpld 112 |
. . . . . . . . . . . . 13
      

   |
50 | 49 | adantr 276 |
. . . . . . . . . . . 12
    

 

 
  |
51 | 50 | nn0zd 9362 |
. . . . . . . . . . 11
    

 

 
  |
52 | 42, 51 | zsubcld 9369 |
. . . . . . . . . 10
    

 

 
    |
53 | | biidd 172 |
. . . . . . . . . . 11
   
 

    |
54 | 53 | ceqsexgv 2866 |
. . . . . . . . . 10
        

 

    |
55 | 52, 54 | syl 14 |
. . . . . . . . 9
    

 

 
     

 

    |
56 | | exancom 1608 |
. . . . . . . . 9
     

 
          |
57 | 55, 56 | bitr3di 195 |
. . . . . . . 8
    

 

 
  
           |
58 | 57 | ex 115 |
. . . . . . 7
      

 
  
            |
59 | 29, 31, 58 | pm5.21ndd 705 |
. . . . . 6
      

               |
60 | 59 | rexbidva 2474 |
. . . . 5
        
 
     
      |
61 | 60 | rexbidva 2474 |
. . . 4
  
       
     

     |
62 | | rexcom4 2760 |
. . . . . 6
      

 
  

       |
63 | 62 | rexbii 2484 |
. . . . 5
  
              

    |
64 | | rexcom4 2760 |
. . . . 5
     
           

    |
65 | 63, 64 | bitri 184 |
. . . 4
  
              

    |
66 | 61, 65 | bitrdi 196 |
. . 3
  
             

     |
67 | 3, 66 | mpbid 147 |
. 2
  
        

    |
68 | | eqid 2177 |
. . . . . . . . . . 11
  
   
              |
69 | | eqid 2177 |
. . . . . . . . . . 11
  
   
              |
70 | | simp11l 1108 |
. . . . . . . . . . 11
    
  
 
      
 
       
                  |
71 | | simp11r 1109 |
. . . . . . . . . . 11
    
  
 
      
 
       
                  |
72 | | simp12 1028 |
. . . . . . . . . . 11
    
  
 
      
 
       
                    |
73 | | simp13l 1112 |
. . . . . . . . . . 11
    
  
 
      
 
       
                    |
74 | | simp2 998 |
. . . . . . . . . . 11
    
  
 
      
 
       
                    |
75 | | simp3l 1025 |
. . . . . . . . . . 11
    
  
 
      
 
       
                    |
76 | 38, 46, 68, 69, 70, 71, 72, 73, 74, 75 | pceulem 12277 |
. . . . . . . . . 10
    
  
 
      
 
       
                               
   
      |
77 | | simp13r 1113 |
. . . . . . . . . 10
    
  
 
      
 
       
                    |
78 | | simp3r 1026 |
. . . . . . . . . 10
    
  
 
      
 
       
                             
   
      |
79 | 76, 77, 78 | 3eqtr4d 2220 |
. . . . . . . . 9
    
  
 
      
 
       
                  |
80 | 79 | 3exp 1202 |
. . . . . . . 8
      
 
                        
   
         |
81 | 80 | rexlimdvv 2601 |
. . . . . . 7
      
 
         
             
   
        |
82 | 81 | 3exp 1202 |
. . . . . 6
                  
             
   
          |
83 | 82 | adantrl 478 |
. . . . 5
  
           
 
   
             
   
          |
84 | 83 | rexlimdvv 2601 |
. . . 4
  
       

   
 
 
       
                   |
85 | 84 | impd 254 |
. . 3
  
        

  
   
             
   
         |
86 | 85 | alrimivv 1875 |
. 2
  
            

  
   
             
   
         |
87 | | eqeq1 2184 |
. . . . . 6
   

    |
88 | 87 | anbi2d 464 |
. . . . 5
          

     |
89 | 88 | 2rexbidv 2502 |
. . . 4
  
 
 
  
    

     |
90 | | oveq1 5876 |
. . . . . . . . 9
       |
91 | 90 | eqeq2d 2189 |
. . . . . . . 8
 
 
     |
92 | | breq2 4004 |
. . . . . . . . . . . . 13
     
       |
93 | 92 | rabbidv 2726 |
. . . . . . . . . . . 12
      
    
   |
94 | 93 | supeq1d 6980 |
. . . . . . . . . . 11
       
               |
95 | 38, 94 | eqtrid 2222 |
. . . . . . . . . 10
             |
96 | 95 | oveq1d 5884 |
. . . . . . . . 9
 
    
   
      |
97 | 96 | eqeq2d 2189 |
. . . . . . . 8
   
               |
98 | 91, 97 | anbi12d 473 |
. . . . . . 7
          
                |
99 | 98 | rexbidv 2478 |
. . . . . 6
  

      
                  |
100 | | oveq2 5877 |
. . . . . . . . 9
       |
101 | 100 | eqeq2d 2189 |
. . . . . . . 8
 
 
     |
102 | | breq2 4004 |
. . . . . . . . . . . . 13
     
       |
103 | 102 | rabbidv 2726 |
. . . . . . . . . . . 12
      
    
   |
104 | 103 | supeq1d 6980 |
. . . . . . . . . . 11
       
               |
105 | 46, 104 | eqtrid 2222 |
. . . . . . . . . 10
             |
106 | 105 | oveq2d 5885 |
. . . . . . . . 9
    
           
   
                |
107 | 106 | eqeq2d 2189 |
. . . . . . . 8
     
           
         
   
       |
108 | 101, 107 | anbi12d 473 |
. . . . . . 7
                    
             
   
        |
109 | 108 | cbvrexvw 2708 |
. . . . . 6
  
 
       
    
   
             
   
       |
110 | 99, 109 | bitrdi 196 |
. . . . 5
  

      
               
   
        |
111 | 110 | cbvrexvw 2708 |
. . . 4
  

 
  
    
             
   
       |
112 | 89, 111 | bitrdi 196 |
. . 3
  
 
 
  
    
             
   
        |
113 | 112 | eu4 2088 |
. 2
       

 
     
 
             

  
   
             
   
          |
114 | 67, 86, 113 | sylanbrc 417 |
1
  
        

    |