Step | Hyp | Ref
| Expression |
1 | | dvdsprmpweq 12333 |
. . . 4
                |
2 | 1 | imp 124 |
. . 3
  
      
      |
3 | | simplr 528 |
. . . . . . . . 9
    
           
  |
4 | 3 | nn0zd 9372 |
. . . . . . . 8
    
           
  |
5 | | simp3 999 |
. . . . . . . . . 10
     |
6 | 5 | ad3antrrr 492 |
. . . . . . . . 9
    
           
  |
7 | 6 | nn0zd 9372 |
. . . . . . . 8
    
           
  |
8 | | zlelttric 9297 |
. . . . . . . 8
 
 
   |
9 | 4, 7, 8 | syl2anc 411 |
. . . . . . 7
    
            
   |
10 | | breq1 4006 |
. . . . . . . . . . . . . . . 16
         
           |
11 | 10 | adantl 277 |
. . . . . . . . . . . . . . 15
    
     
                |
12 | | prmnn 12109 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
13 | 12 | nnnn0d 9228 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
14 | 13 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . 21
     |
15 | 14 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
  


  |
16 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . 20
  


  |
17 | 15, 16 | nn0expcld 10676 |
. . . . . . . . . . . . . . . . . . 19
  

       |
18 | 17 | nn0zd 9372 |
. . . . . . . . . . . . . . . . . 18
  

       |
19 | 12 | nncnd 8932 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
20 | 19 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . 21
     |
21 | 20 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
  


  |
22 | 12 | nnap0d 8964 |
. . . . . . . . . . . . . . . . . . . . . 22

#   |
23 | 22 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . 21
   #   |
24 | 23 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
  

 #   |
25 | | nn0z 9272 |
. . . . . . . . . . . . . . . . . . . . 21

  |
26 | 25 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
  


  |
27 | 21, 24, 26 | expap0d 10659 |
. . . . . . . . . . . . . . . . . . 19
  

     #   |
28 | | 0zd 9264 |
. . . . . . . . . . . . . . . . . . . 20
  

   |
29 | | zapne 9326 |
. . . . . . . . . . . . . . . . . . . 20
     
      #        |
30 | 18, 28, 29 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
  

      #        |
31 | 27, 30 | mpbid 147 |
. . . . . . . . . . . . . . . . . 18
  

       |
32 | 5 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
  


  |
33 | 15, 32 | nn0expcld 10676 |
. . . . . . . . . . . . . . . . . . 19
  

       |
34 | 33 | nn0zd 9372 |
. . . . . . . . . . . . . . . . . 18
  

       |
35 | | dvdsval2 11796 |
. . . . . . . . . . . . . . . . . 18
                   
   
             |
36 | 18, 31, 34, 35 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
  

         
             |
37 | 32 | nn0zd 9372 |
. . . . . . . . . . . . . . . . . . . . 21
  


  |
38 | 21, 24, 26, 37 | expsubapd 10664 |
. . . . . . . . . . . . . . . . . . . 20
  

    
              |
39 | 38 | eqcomd 2183 |
. . . . . . . . . . . . . . . . . . 19
  

                   |
40 | 39 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . 18
  

                     |
41 | 21 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 
  |
42 | 24 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 
#   |
43 | | nn0cn 9185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
44 | 43 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
45 | 44 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  


  |
46 | | nn0cn 9185 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
47 | 46 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  


  |
48 | 45, 47 | subcld 8267 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

     |
49 | 48 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 
    |
50 | 44, 46 | anim12i 338 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  

     |
51 | 50 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
 
    |
52 | | negsubdi2 8215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
        |
53 | 51, 52 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
 
       |
54 | 5 | anim1ci 341 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  

     |
55 | | ltsubnn0 9319 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       |
56 | 54, 55 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  

       |
57 | 56 | imp 124 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
 
    |
58 | 53, 57 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 
     |
59 | | expineg2 10528 |
. . . . . . . . . . . . . . . . . . . . . . 23
   #         
                 |
60 | 41, 42, 49, 58, 59 | syl22anc 1239 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
                 |
61 | 60 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
            
      |
62 | 12 | nnred 8931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
63 | 62 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
64 | 63 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  


  |
65 | 64 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
 
  |
66 | 65, 57 | reexpcld 10670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
 
        |
67 | | nn0z 9272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
68 | 67 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
69 | 68, 25 | anim12i 338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  

     |
70 | | znnsub 9303 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       |
71 | 69, 70 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  

       |
72 | 71 | biimpa 296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
 
    |
73 | | prmgt1 12131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
74 | 73 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
75 | 74 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  


  |
76 | 75 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
 
  |
77 | | expgt1 10557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
 
        |
78 | 65, 72, 76, 77 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
 
        |
79 | 66, 78 | jca 306 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
 
                |
80 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
       
          |
81 | 80 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
                    |
82 | 80 | breq2d 4015 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
                    |
83 | 81, 82 | anbi12d 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
                
  
                 |
84 | 79, 83 | syl5ibrcom 157 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
 
  
        
             |
85 | 53, 84 | mpd 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 
            
     |
86 | | recnz 9345 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                     |
87 | 85, 86 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
           |
88 | 87 | pm2.21d 619 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
             |
89 | 61, 88 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . 20
    
 
      
   |
90 | 89 | ex 115 |
. . . . . . . . . . . . . . . . . . 19
  

        
    |
91 | 90 | com23 78 |
. . . . . . . . . . . . . . . . . 18
  

        
    |
92 | 40, 91 | sylbid 150 |
. . . . . . . . . . . . . . . . 17
  

            
    |
93 | 36, 92 | sylbid 150 |
. . . . . . . . . . . . . . . 16
  

          
    |
94 | 93 | adantr 276 |
. . . . . . . . . . . . . . 15
    
     
         
    |
95 | 11, 94 | sylbid 150 |
. . . . . . . . . . . . . 14
    
     
    

    |
96 | 95 | ex 115 |
. . . . . . . . . . . . 13
  

           
     |
97 | 96 | com23 78 |
. . . . . . . . . . . 12
  

           
     |
98 | 97 | ex 115 |
. . . . . . . . . . 11
              
      |
99 | 98 | com23 78 |
. . . . . . . . . 10
              
      |
100 | 99 | imp41 353 |
. . . . . . . . 9
    
            
   |
101 | 100 | com12 30 |
. . . . . . . 8
                     |
102 | 101 | jao1i 796 |
. . . . . . 7
 
     
     

        |
103 | 9, 102 | mpcom 36 |
. . . . . 6
    
              |
104 | | simpr 110 |
. . . . . 6
    
           
      |
105 | 103, 104 | jca 306 |
. . . . 5
    
            
       |
106 | 105 | ex 115 |
. . . 4
    
          
         |
107 | 106 | reximdva 2579 |
. . 3
  
       
    

        |
108 | 2, 107 | mpd 13 |
. 2
  
      

       |
109 | 108 | ex 115 |
1
                  |