Proof of Theorem ztprmneprm
Step | Hyp | Ref
| Expression |
1 | | elznn0nn 10951 |
. . 3

       |
2 | | elnn0 10871 |
. . . . 5

    |
3 | | elnn1uz2 11235 |
. . . . . . 7

        |
4 | | oveq1 6297 |
. . . . . . . . . . . 12
 
     |
5 | 4 | adantr 467 |
. . . . . . . . . . 11
    
      |
6 | 5 | eqeq1d 2453 |
. . . . . . . . . 10
    
 

     |
7 | | prmz 14626 |
. . . . . . . . . . . . . . . 16

  |
8 | 7 | zcnd 11041 |
. . . . . . . . . . . . . . 15

  |
9 | 8 | mulid2d 9661 |
. . . . . . . . . . . . . 14

    |
10 | 9 | adantr 467 |
. . . . . . . . . . . . 13
       |
11 | 10 | eqeq1d 2453 |
. . . . . . . . . . . 12
     
   |
12 | 11 | biimpd 211 |
. . . . . . . . . . 11
     
   |
13 | 12 | adantl 468 |
. . . . . . . . . 10
    
      |
14 | 6, 13 | sylbid 219 |
. . . . . . . . 9
    
 

   |
15 | 14 | ex 436 |
. . . . . . . 8
           |
16 | | prmuz2 14642 |
. . . . . . . . . . . 12

      |
17 | 16 | adantr 467 |
. . . . . . . . . . 11
         |
18 | | nprm 14638 |
. . . . . . . . . . 11
          

   |
19 | 17, 18 | sylan2 477 |
. . . . . . . . . 10
      
      |
20 | | eleq1 2517 |
. . . . . . . . . . . . 13
     
   |
21 | 20 | notbid 296 |
. . . . . . . . . . . 12
     
   |
22 | | pm2.24 113 |
. . . . . . . . . . . . . . 15

    |
23 | 22 | adantl 468 |
. . . . . . . . . . . . . 14
   
   |
24 | 23 | adantl 468 |
. . . . . . . . . . . . 13
      
      |
25 | 24 | com12 32 |
. . . . . . . . . . . 12
       
 
   |
26 | 21, 25 | syl6bi 232 |
. . . . . . . . . . 11
            
 
    |
27 | 26 | com3l 84 |
. . . . . . . . . 10
         
 
 

    |
28 | 19, 27 | mpcom 37 |
. . . . . . . . 9
      
        |
29 | 28 | ex 436 |
. . . . . . . 8
    
 
   
    |
30 | 15, 29 | jaoi 381 |
. . . . . . 7
            
    |
31 | 3, 30 | sylbi 199 |
. . . . . 6
           |
32 | | oveq1 6297 |
. . . . . . . . 9
 
     |
33 | 32 | eqeq1d 2453 |
. . . . . . . 8
   
     |
34 | | prmnn 14625 |
. . . . . . . . . . . . . 14

  |
35 | 34 | nnred 10624 |
. . . . . . . . . . . . 13

  |
36 | | mul02lem2 9810 |
. . . . . . . . . . . . 13
     |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12

    |
38 | 37 | adantr 467 |
. . . . . . . . . . 11
       |
39 | 38 | eqeq1d 2453 |
. . . . . . . . . 10
     
   |
40 | | prmnn 14625 |
. . . . . . . . . . . 12

  |
41 | | elnnne0 10883 |
. . . . . . . . . . . . 13

    |
42 | | eqneqall 2634 |
. . . . . . . . . . . . . . . 16
     |
43 | 42 | eqcoms 2459 |
. . . . . . . . . . . . . . 15
     |
44 | 43 | com12 32 |
. . . . . . . . . . . . . 14
 
   |
45 | 44 | adantl 468 |
. . . . . . . . . . . . 13
       |
46 | 41, 45 | sylbi 199 |
. . . . . . . . . . . 12
 
   |
47 | 40, 46 | syl 17 |
. . . . . . . . . . 11

    |
48 | 47 | adantl 468 |
. . . . . . . . . 10
   
   |
49 | 39, 48 | sylbid 219 |
. . . . . . . . 9
     
   |
50 | 49 | com12 32 |
. . . . . . . 8
         |
51 | 33, 50 | syl6bi 232 |
. . . . . . 7
           |
52 | 51 | com23 81 |
. . . . . 6
           |
53 | 31, 52 | jaoi 381 |
. . . . 5
 
  

       |
54 | 2, 53 | sylbi 199 |
. . . 4

     
    |
55 | | elnnz 10947 |
. . . . . 6
 
      |
56 | | lt0neg1 10120 |
. . . . . . . 8
 
    |
57 | 34 | nngt0d 10653 |
. . . . . . . . . . . . . . . 16

  |
58 | 57 | adantr 467 |
. . . . . . . . . . . . . . 15
     |
59 | | simpr 463 |
. . . . . . . . . . . . . . 15
     |
60 | 58, 59 | anim12ci 571 |
. . . . . . . . . . . . . 14
      
    |
61 | 60 | orcd 394 |
. . . . . . . . . . . . 13
      
   
    |
62 | | simprl 764 |
. . . . . . . . . . . . . 14
      
  |
63 | 35 | adantr 467 |
. . . . . . . . . . . . . . 15
     |
64 | 63 | adantr 467 |
. . . . . . . . . . . . . 14
      
  |
65 | 62, 64 | mul2lt0bi 11402 |
. . . . . . . . . . . . 13
      
 
    
     |
66 | 61, 65 | mpbird 236 |
. . . . . . . . . . . 12
      
    |
67 | 66 | ex 436 |
. . . . . . . . . . 11
           |
68 | | breq1 4405 |
. . . . . . . . . . . . . . 15
     
   |
69 | 68 | adantl 468 |
. . . . . . . . . . . . . 14
         
   |
70 | | nnnn0 10876 |
. . . . . . . . . . . . . . . . . 18
   |
71 | | nn0nlt0 10896 |
. . . . . . . . . . . . . . . . . . 19

  |
72 | 71 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . 18

    |
73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
     |
74 | 40, 73 | syl 17 |
. . . . . . . . . . . . . . . 16

    |
75 | 74 | adantl 468 |
. . . . . . . . . . . . . . 15
       |
76 | 75 | adantr 467 |
. . . . . . . . . . . . . 14
       
   |
77 | 69, 76 | sylbid 219 |
. . . . . . . . . . . . 13
         
   |
78 | 77 | ex 436 |
. . . . . . . . . . . 12
             |
79 | 78 | com23 81 |
. . . . . . . . . . 11
     
  
    |
80 | 67, 79 | syld 45 |
. . . . . . . . . 10
        
    |
81 | 80 | com12 32 |
. . . . . . . . 9
        
    |
82 | 81 | ex 436 |
. . . . . . . 8
             |
83 | 56, 82 | sylbird 239 |
. . . . . . 7
 
      
     |
84 | 83 | adantld 469 |
. . . . . 6
     
 
   
     |
85 | 55, 84 | syl5bi 221 |
. . . . 5
              |
86 | 85 | imp 431 |
. . . 4
     

       |
87 | 54, 86 | jaoi 381 |
. . 3
  

            |
88 | 1, 87 | sylbi 199 |
. 2
           |
89 | 88 | 3impib 1206 |
1
 
   
   |