Step | Hyp | Ref
| Expression |
1 | | pockthg.4 |
. . 3
       |
2 | | pockthg.1 |
. . . . . . 7
   |
3 | | pockthg.2 |
. . . . . . 7
   |
4 | 2, 3 | nnmulcld 10679 |
. . . . . 6
     |
5 | | nnuz 11218 |
. . . . . 6
     |
6 | 4, 5 | syl6eleq 2559 |
. . . . 5
         |
7 | | eluzp1p1 11208 |
. . . . 5
      
 
          |
8 | 6, 7 | syl 17 |
. . . 4
             |
9 | | df-2 10690 |
. . . . 5
   |
10 | 9 | fveq2i 5882 |
. . . 4
           |
11 | 8, 10 | syl6eleqr 2560 |
. . 3
           |
12 | 1, 11 | eqeltrd 2549 |
. 2
       |
13 | | eluzelre 11193 |
. . . . . . . . 9
    
  |
14 | 12, 13 | syl 17 |
. . . . . . . 8
   |
15 | 14 | adantr 472 |
. . . . . . 7
 

 
  |
16 | 2 | nnred 10646 |
. . . . . . . . 9
   |
17 | 16 | resqcld 12480 |
. . . . . . . 8
       |
18 | 17 | adantr 472 |
. . . . . . 7
 

        |
19 | | prmnn 14704 |
. . . . . . . . . 10

  |
20 | 19 | ad2antrl 742 |
. . . . . . . . 9
 

    |
21 | 20 | nnred 10646 |
. . . . . . . 8
 

    |
22 | 21 | resqcld 12480 |
. . . . . . 7
 

        |
23 | | pockthg.3 |
. . . . . . . . . . 11
   |
24 | 3 | nnred 10646 |
. . . . . . . . . . . 12
   |
25 | 2 | nngt0d 10675 |
. . . . . . . . . . . 12
   |
26 | | ltmul2 10478 |
. . . . . . . . . . . 12
 

          |
27 | 24, 16, 16, 25, 26 | syl112anc 1296 |
. . . . . . . . . . 11
         |
28 | 23, 27 | mpbid 215 |
. . . . . . . . . 10
  
    |
29 | 2, 2 | nnmulcld 10679 |
. . . . . . . . . . 11
     |
30 | | nnltp1le 11016 |
. . . . . . . . . . 11
    
           
    |
31 | 4, 29, 30 | syl2anc 673 |
. . . . . . . . . 10
    
          |
32 | 28, 31 | mpbid 215 |
. . . . . . . . 9
    
    |
33 | 2 | nncnd 10647 |
. . . . . . . . . 10
   |
34 | 33 | sqvald 12451 |
. . . . . . . . 9
         |
35 | 32, 1, 34 | 3brtr4d 4426 |
. . . . . . . 8

      |
36 | 35 | adantr 472 |
. . . . . . 7
 

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

  
 
                         |
39 | | prmnn 14704 |
. . . . . . . . . . . . . . . . . . . 20

  |
40 | 39 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . 19
      
   
  |
41 | 40 | nncnd 10647 |
. . . . . . . . . . . . . . . . . 18
      
   
  |
42 | 41 | exp1d 12449 |
. . . . . . . . . . . . . . . . 17
      
   
      |
43 | | nnge1 10657 |
. . . . . . . . . . . . . . . . . . 19
 


   |
44 | 43 | ad2antll 743 |
. . . . . . . . . . . . . . . . . 18
      
   

   |
45 | | simprl 772 |
. . . . . . . . . . . . . . . . . . 19
      
   
  |
46 | 2 | nnzd 11062 |
. . . . . . . . . . . . . . . . . . . 20
   |
47 | 46 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
      
   
  |
48 | | 1nn0 10909 |
. . . . . . . . . . . . . . . . . . . 20
 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
      
   
  |
50 | | pcdvdsb 14897 |
. . . . . . . . . . . . . . . . . . 19
   
 
       |
51 | 45, 47, 49, 50 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
      
   
          |
52 | 44, 51 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
      
   
      |
53 | 42, 52 | eqbrtrrd 4418 |
. . . . . . . . . . . . . . . 16
      
   
  |
54 | | simpl1 1033 |
. . . . . . . . . . . . . . . . . . . 20
      
   
                          |
55 | 54, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
56 | 54, 3 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
57 | 54, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
      
   
                          |
58 | 54, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
 
    |
59 | | simpl2l 1083 |
. . . . . . . . . . . . . . . . . . 19
      
   
                          |
60 | | simpl2r 1084 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
61 | | simpl3l 1085 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
62 | | simpl3r 1086 |
. . . . . . . . . . . . . . . . . . 19
      
   
                            |
63 | | simprl 772 |
. . . . . . . . . . . . . . . . . . 19
      
   
                       
  |
64 | | simprrl 782 |
. . . . . . . . . . . . . . . . . . 19
      
   
                                  |
65 | | simprrr 783 |
. . . . . . . . . . . . . . . . . . 19
      
   
                                      |
66 | 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65 | pockthlem 14928 |
. . . . . . . . . . . . . . . . . 18
      
   
                         
      |
67 | 66 | rexlimdvaa 2872 |
. . . . . . . . . . . . . . . . 17
 

  
                           
        |
68 | 67 | 3expa 1231 |
. . . . . . . . . . . . . . . 16
      
   
 
                       
       |
69 | 53, 68 | embantd 55 |
. . . . . . . . . . . . . . 15
      
   
 
                       
  
      |
70 | 69 | expr 626 |
. . . . . . . . . . . . . 14
     
                              
         |
71 | | id 22 |
. . . . . . . . . . . . . . . . . 18

  |
72 | | prmuz2 14721 |
. . . . . . . . . . . . . . . . . . . 20

      |
73 | | uz2m1nn 11256 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . 19

    |
75 | 74 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . 18
 

      |
76 | | pccl 14878 |
. . . . . . . . . . . . . . . . . 18
           |
77 | 71, 75, 76 | syl2anr 486 |
. . . . . . . . . . . . . . . . 17
     
       |
78 | 77 | nn0ge0d 10952 |
. . . . . . . . . . . . . . . 16
     

      |
79 | | breq1 4398 |
. . . . . . . . . . . . . . . 16
 
   
   

      |
80 | 78, 79 | syl5ibrcom 230 |
. . . . . . . . . . . . . . 15
     
     
       |
81 | 80 | a1dd 46 |
. . . . . . . . . . . . . 14
     
                              
         |
82 | | simpr 468 |
. . . . . . . . . . . . . . . 16
     

  |
83 | 2 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
     

  |
84 | 82, 83 | pccld 14879 |
. . . . . . . . . . . . . . 15
     
     |
85 | | elnn0 10895 |
. . . . . . . . . . . . . . 15
 
         |
86 | 84, 85 | sylib 201 |
. . . . . . . . . . . . . 14
     
    
    |
87 | 70, 81, 86 | mpjaod 388 |
. . . . . . . . . . . . 13
     
                           
        |
88 | 87 | ralimdva 2805 |
. . . . . . . . . . . 12
 

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

  

       |
90 | 46 | adantr 472 |
. . . . . . . . . . . 12
 

 
  |
91 | 75 | nnzd 11062 |
. . . . . . . . . . . 12
 

      |
92 | | pc2dvds 14907 |
. . . . . . . . . . . 12
         
        |
93 | 90, 91, 92 | syl2anc 673 |
. . . . . . . . . . 11
 

     

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

      |
95 | | dvdsle 14427 |
. . . . . . . . . . 11
       
     |
96 | 90, 75, 95 | syl2anc 673 |
. . . . . . . . . 10
 

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

      |
98 | 2 | nnnn0d 10949 |
. . . . . . . . . . 11
   |
99 | 98 | adantr 472 |
. . . . . . . . . 10
 

 
  |
100 | 20 | nnnn0d 10949 |
. . . . . . . . . 10
 

    |
101 | | nn0ltlem1 11020 |
. . . . . . . . . 10
 
       |
102 | 99, 100, 101 | syl2anc 673 |
. . . . . . . . 9
 

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

    |
104 | 16 | adantr 472 |
. . . . . . . . 9
 

 
  |
105 | 98 | nn0ge0d 10952 |
. . . . . . . . . 10

  |
106 | 105 | adantr 472 |
. . . . . . . . 9
 

 
  |
107 | 100 | nn0ge0d 10952 |
. . . . . . . . 9
 

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

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

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

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

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

     
  |
113 | 112 | expr 626 |
. . . 4
 


       |
114 | 113 | con2d 119 |
. . 3
 

        |
115 | 114 | ralrimiva 2809 |
. 2
      
   |
116 | | isprm5 14730 |
. 2

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