Step | Hyp | Ref
| Expression |
1 | | pockthg.4 |
. . 3
       |
2 | | pockthg.1 |
. . . . . . 7
   |
3 | | pockthg.2 |
. . . . . . 7
   |
4 | 2, 3 | nnmulcld 10470 |
. . . . . 6
     |
5 | | nnuz 10997 |
. . . . . 6
     |
6 | 4, 5 | syl6eleq 2549 |
. . . . 5
         |
7 | | eluzp1p1 10987 |
. . . . 5
      
 
          |
8 | 6, 7 | syl 16 |
. . . 4
             |
9 | | df-2 10481 |
. . . . 5
   |
10 | 9 | fveq2i 5792 |
. . . 4
           |
11 | 8, 10 | syl6eleqr 2550 |
. . 3
           |
12 | 1, 11 | eqeltrd 2539 |
. 2
       |
13 | | eluzelre 10972 |
. . . . . . . . 9
    
  |
14 | 12, 13 | syl 16 |
. . . . . . . 8
   |
15 | 14 | adantr 465 |
. . . . . . 7
 

 
  |
16 | 2 | nnred 10438 |
. . . . . . . . 9
   |
17 | 16 | resqcld 12135 |
. . . . . . . 8
       |
18 | 17 | adantr 465 |
. . . . . . 7
 

        |
19 | | prmnn 13868 |
. . . . . . . . . 10

  |
20 | 19 | ad2antrl 727 |
. . . . . . . . 9
 

    |
21 | 20 | nnred 10438 |
. . . . . . . 8
 

    |
22 | 21 | resqcld 12135 |
. . . . . . 7
 

        |
23 | | pockthg.3 |
. . . . . . . . . . 11
   |
24 | 3 | nnred 10438 |
. . . . . . . . . . . 12
   |
25 | 2 | nngt0d 10466 |
. . . . . . . . . . . 12
   |
26 | | ltmul2 10281 |
. . . . . . . . . . . 12
 

          |
27 | 24, 16, 16, 25, 26 | syl112anc 1223 |
. . . . . . . . . . 11
         |
28 | 23, 27 | mpbid 210 |
. . . . . . . . . 10
  
    |
29 | 2, 2 | nnmulcld 10470 |
. . . . . . . . . . 11
     |
30 | | nnltp1le 10801 |
. . . . . . . . . . 11
    
           
    |
31 | 4, 29, 30 | syl2anc 661 |
. . . . . . . . . 10
    
          |
32 | 28, 31 | mpbid 210 |
. . . . . . . . 9
    
    |
33 | 2 | nncnd 10439 |
. . . . . . . . . 10
   |
34 | 33 | sqvald 12106 |
. . . . . . . . 9
         |
35 | 32, 1, 34 | 3brtr4d 4420 |
. . . . . . . 8

      |
36 | 35 | adantr 465 |
. . . . . . 7
 

        |
37 | | pockthg.5 |
. . . . . . . . . . . . 13
   
                         |
38 | 37 | adantr 465 |
. . . . . . . . . . . 12
 

  
 
                         |
39 | | prmnn 13868 |
. . . . . . . . . . . . . . . . . . . 20

  |
40 | 39 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . 19
      
   
  |
41 | 40 | nncnd 10439 |
. . . . . . . . . . . . . . . . . 18
      
   
  |
42 | 41 | exp1d 12104 |
. . . . . . . . . . . . . . . . 17
      
   
      |
43 | | nnge1 10449 |
. . . . . . . . . . . . . . . . . . 19
 


   |
44 | 43 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
      
   

   |
45 | | simprl 755 |
. . . . . . . . . . . . . . . . . . 19
      
   
  |
46 | 2 | nnzd 10847 |
. . . . . . . . . . . . . . . . . . . 20
   |
47 | 46 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
      
   
  |
48 | | 1nn0 10696 |
. . . . . . . . . . . . . . . . . . . 20
 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
      
   
  |
50 | | pcdvdsb 14037 |
. . . . . . . . . . . . . . . . . . 19
   
 
       |
51 | 45, 47, 49, 50 | syl3anc 1219 |
. . . . . . . . . . . . . . . . . 18
      
   
          |
52 | 44, 51 | mpbid 210 |
. . . . . . . . . . . . . . . . 17
      
   
      |
53 | 42, 52 | eqbrtrrd 4412 |
. . . . . . . . . . . . . . . 16
      
   
  |
54 | | simpl1 991 |
. . . . . . . . . . . . . . . . . . . 20
      
   
                          |
55 | 54, 2 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
56 | 54, 3 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
57 | 54, 23 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
      
   
                          |
58 | 54, 1 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
 
    |
59 | | simpl2l 1041 |
. . . . . . . . . . . . . . . . . . 19
      
   
                          |
60 | | simpl2r 1042 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
61 | | simpl3l 1043 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
62 | | simpl3r 1044 |
. . . . . . . . . . . . . . . . . . 19
      
   
                            |
63 | | simprl 755 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
64 | | simprrl 763 |
. . . . . . . . . . . . . . . . . . 19
      
   
                                  |
65 | | simprrr 764 |
. . . . . . . . . . . . . . . . . . 19
      
   
                                      |
66 | 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65 | pockthlem 14068 |
. . . . . . . . . . . . . . . . . 18
      
   
                         
      |
67 | 66 | rexlimdvaa 2938 |
. . . . . . . . . . . . . . . . 17
 

  
                           
        |
68 | 67 | 3expa 1188 |
. . . . . . . . . . . . . . . 16
      
   
 
                       
       |
69 | 53, 68 | embantd 54 |
. . . . . . . . . . . . . . 15
      
   
 
                       
  
      |
70 | 69 | expr 615 |
. . . . . . . . . . . . . 14
     
                              
         |
71 | | id 22 |
. . . . . . . . . . . . . . . . . 18

  |
72 | | prmuz2 13883 |
. . . . . . . . . . . . . . . . . . . 20

      |
73 | | uz2m1nn 11030 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
74 | 72, 73 | syl 16 |
. . . . . . . . . . . . . . . . . . 19

    |
75 | 74 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
 

      |
76 | | pccl 14018 |
. . . . . . . . . . . . . . . . . 18
           |
77 | 71, 75, 76 | syl2anr 478 |
. . . . . . . . . . . . . . . . 17
     
       |
78 | 77 | nn0ge0d 10740 |
. . . . . . . . . . . . . . . 16
     

      |
79 | | breq1 4393 |
. . . . . . . . . . . . . . . 16
 
   
   

      |
80 | 78, 79 | syl5ibrcom 222 |
. . . . . . . . . . . . . . 15
     
     
       |
81 | 80 | a1dd 46 |
. . . . . . . . . . . . . 14
     
                              
         |
82 | | simpr 461 |
. . . . . . . . . . . . . . . 16
     

  |
83 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
     

  |
84 | 82, 83 | pccld 14019 |
. . . . . . . . . . . . . . 15
     
     |
85 | | elnn0 10682 |
. . . . . . . . . . . . . . 15
 
         |
86 | 84, 85 | sylib 196 |
. . . . . . . . . . . . . 14
     
    
    |
87 | 70, 81, 86 | mpjaod 381 |
. . . . . . . . . . . . 13
     
                           
        |
88 | 87 | ralimdva 2824 |
. . . . . . . . . . . 12
 

                               
       |
89 | 38, 88 | mpd 15 |
. . . . . . . . . . 11
 

  

       |
90 | 46 | adantr 465 |
. . . . . . . . . . . 12
 

 
  |
91 | 75 | nnzd 10847 |
. . . . . . . . . . . 12
 

      |
92 | | pc2dvds 14047 |
. . . . . . . . . . . 12
         
        |
93 | 90, 91, 92 | syl2anc 661 |
. . . . . . . . . . 11
 

     

        |
94 | 89, 93 | mpbird 232 |
. . . . . . . . . 10
 

      |
95 | | dvdsle 13680 |
. . . . . . . . . . 11
       
     |
96 | 90, 75, 95 | syl2anc 661 |
. . . . . . . . . 10
 

          |
97 | 94, 96 | mpd 15 |
. . . . . . . . 9
 

      |
98 | 2 | nnnn0d 10737 |
. . . . . . . . . . 11
   |
99 | 98 | adantr 465 |
. . . . . . . . . 10
 

 
  |
100 | 20 | nnnn0d 10737 |
. . . . . . . . . 10
 

    |
101 | | nn0ltlem1 10805 |
. . . . . . . . . 10
 
       |
102 | 99, 100, 101 | syl2anc 661 |
. . . . . . . . 9
 

        |
103 | 97, 102 | mpbird 232 |
. . . . . . . 8
 

    |
104 | 16 | adantr 465 |
. . . . . . . . 9
 

 
  |
105 | 98 | nn0ge0d 10740 |
. . . . . . . . . 10

  |
106 | 105 | adantr 465 |
. . . . . . . . 9
 

 
  |
107 | 100 | nn0ge0d 10740 |
. . . . . . . . 9
 

 
  |
108 | 104, 21, 106, 107 | lt2sqd 12143 |
. . . . . . . 8
 

              |
109 | 103, 108 | mpbid 210 |
. . . . . . 7
 

            |
110 | 15, 18, 22, 36, 109 | lelttrd 9630 |
. . . . . 6
 

        |
111 | 15, 22 | ltnled 9622 |
. . . . . 6
 

          
   |
112 | 110, 111 | mpbid 210 |
. . . . 5
 

     
  |
113 | 112 | expr 615 |
. . . 4
 


       |
114 | 113 | con2d 115 |
. . 3
 

        |
115 | 114 | ralrimiva 2822 |
. 2
      
   |
116 | | isprm5 13900 |
. 2

          
    |
117 | 12, 115, 116 | sylanbrc 664 |
1
   |