Proof of Theorem isprm3
Step | Hyp | Ref
| Expression |
1 | | isprm2 11644 |
. 2

             |
2 | | dvdszrcl 11346 |
. . . . . . . . . . 11
 
   |
3 | 2 | simpld 111 |
. . . . . . . . . 10
   |
4 | | 1zzd 8985 |
. . . . . . . . . 10
         |
5 | | zdceq 9030 |
. . . . . . . . . 10
 
 DECID   |
6 | 3, 4, 5 | syl2an2 566 |
. . . . . . . . 9
      
DECID
  |
7 | 2 | simprd 113 |
. . . . . . . . . . 11
   |
8 | 7 | adantl 273 |
. . . . . . . . . 10
         |
9 | | zdceq 9030 |
. . . . . . . . . 10
 
 DECID   |
10 | 3, 8, 9 | syl2an2 566 |
. . . . . . . . 9
      
DECID
  |
11 | | dcor 902 |
. . . . . . . . 9
DECID
DECID
DECID      |
12 | 6, 10, 11 | sylc 62 |
. . . . . . . 8
      
DECID     |
13 | | imandc 857 |
. . . . . . . 8
DECID       
       |
14 | 12, 13 | syl 14 |
. . . . . . 7
           
       |
15 | | eluz2nn 9266 |
. . . . . . . . . . . . . . . 16
    
  |
16 | | nnz 8977 |
. . . . . . . . . . . . . . . . . 18
   |
17 | | dvdsle 11390 |
. . . . . . . . . . . . . . . . . 18
 
 
   |
18 | 16, 17 | sylan 279 |
. . . . . . . . . . . . . . . . 17
 
 
   |
19 | | nnge1 8653 |
. . . . . . . . . . . . . . . . . 18
   |
20 | 19 | adantr 272 |
. . . . . . . . . . . . . . . . 17
 

  |
21 | 18, 20 | jctild 312 |
. . . . . . . . . . . . . . . 16
 
  
    |
22 | 15, 21 | sylan2 282 |
. . . . . . . . . . . . . . 15
 
      
    |
23 | | nnz 8977 |
. . . . . . . . . . . . . . . . . 18
   |
24 | | zre 8962 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
25 | | 1re 7689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
26 | | leltap 8305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 
#    |
27 | 25, 26 | mp3an1 1285 |
. . . . . . . . . . . . . . . . . . . . . . 23
    #    |
28 | 24, 27 | sylan 279 |
. . . . . . . . . . . . . . . . . . . . . 22
    #    |
29 | | 1z 8984 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
30 | | zapne 9029 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  #    |
31 | 29, 30 | mpan2 419 |
. . . . . . . . . . . . . . . . . . . . . . 23
  #
   |
32 | 31 | adantr 272 |
. . . . . . . . . . . . . . . . . . . . . 22
    #    |
33 | 28, 32 | bitrd 187 |
. . . . . . . . . . . . . . . . . . . . 21
       |
34 | 33 | 3adant2 983 |
. . . . . . . . . . . . . . . . . . . 20
 
 
   |
35 | 34 | 3expia 1166 |
. . . . . . . . . . . . . . . . . . 19
 
       |
36 | | zre 8962 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
37 | | leltap 8305 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
#    |
38 | 24, 37 | syl3an1 1232 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
#    |
39 | 36, 38 | syl3an2 1233 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
#    |
40 | | zapne 9029 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  #
   |
41 | 40 | ancoms 266 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  #
   |
42 | 41 | 3adant3 984 |
. . . . . . . . . . . . . . . . . . . . 21
 
  #
   |
43 | 39, 42 | bitrd 187 |
. . . . . . . . . . . . . . . . . . . 20
 
 
   |
44 | 43 | 3expia 1166 |
. . . . . . . . . . . . . . . . . . 19
 
       |
45 | 35, 44 | anim12d 331 |
. . . . . . . . . . . . . . . . . 18
 
  

 
 
     |
46 | 23, 45 | sylan2 282 |
. . . . . . . . . . . . . . . . 17
 
  

 
 
     |
47 | | pm4.38 577 |
. . . . . . . . . . . . . . . . . 18
         

    |
48 | | df-ne 2283 |
. . . . . . . . . . . . . . . . . . . 20

  |
49 | | nesym 2327 |
. . . . . . . . . . . . . . . . . . . 20

  |
50 | 48, 49 | anbi12i 453 |
. . . . . . . . . . . . . . . . . . 19
       |
51 | | ioran 724 |
. . . . . . . . . . . . . . . . . . 19
   
   |
52 | 50, 51 | bitr4i 186 |
. . . . . . . . . . . . . . . . . 18
       |
53 | 47, 52 | syl6bb 195 |
. . . . . . . . . . . . . . . . 17
         
     |
54 | 46, 53 | syl6 33 |
. . . . . . . . . . . . . . . 16
 
  

 

      |
55 | 16, 15, 54 | syl2an 285 |
. . . . . . . . . . . . . . 15
 
      

 

      |
56 | 22, 55 | syld 45 |
. . . . . . . . . . . . . 14
 
       

      |
57 | 56 | imp 123 |
. . . . . . . . . . . . 13
          

     |
58 | | eluzelz 9237 |
. . . . . . . . . . . . . . 15
    
  |
59 | | zltp1le 9012 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
60 | 29, 59 | mpan 418 |
. . . . . . . . . . . . . . . . . . 19
 
     |
61 | | df-2 8689 |
. . . . . . . . . . . . . . . . . . . 20
   |
62 | 61 | breq1i 3902 |
. . . . . . . . . . . . . . . . . . 19

    |
63 | 60, 62 | syl6bbr 197 |
. . . . . . . . . . . . . . . . . 18
 
   |
64 | 63 | adantr 272 |
. . . . . . . . . . . . . . . . 17
 
     |
65 | | zltlem1 9015 |
. . . . . . . . . . . . . . . . 17
 
       |
66 | 64, 65 | anbi12d 462 |
. . . . . . . . . . . . . . . 16
 
  
 
      |
67 | | peano2zm 8996 |
. . . . . . . . . . . . . . . . 17
 
   |
68 | | 2z 8986 |
. . . . . . . . . . . . . . . . . 18
 |
69 | | elfz 9689 |
. . . . . . . . . . . . . . . . . 18
 

         
      |
70 | 68, 69 | mp3an2 1286 |
. . . . . . . . . . . . . . . . 17
  
      
  
      |
71 | 67, 70 | sylan2 282 |
. . . . . . . . . . . . . . . 16
 
        
      |
72 | 66, 71 | bitr4d 190 |
. . . . . . . . . . . . . . 15
 
  
          |
73 | 16, 58, 72 | syl2an 285 |
. . . . . . . . . . . . . 14
 
      
          |
74 | 73 | adantr 272 |
. . . . . . . . . . . . 13
          
          |
75 | 57, 74 | bitr3d 189 |
. . . . . . . . . . . 12
           
   
     |
76 | 75 | anasss 394 |
. . . . . . . . . . 11
  
                  |
77 | 76 | expcom 115 |
. . . . . . . . . 10
          
   
      |
78 | 77 | pm5.32d 443 |
. . . . . . . . 9
           
    
      |
79 | | fzssuz 9738 |
. . . . . . . . . . . . 13
           |
80 | | 2eluzge1 9273 |
. . . . . . . . . . . . . 14
     |
81 | | uzss 9248 |
. . . . . . . . . . . . . 14
    
          |
82 | 80, 81 | ax-mp 7 |
. . . . . . . . . . . . 13
         |
83 | 79, 82 | sstri 3072 |
. . . . . . . . . . . 12
           |
84 | | nnuz 9263 |
. . . . . . . . . . . 12
     |
85 | 83, 84 | sseqtr4i 3098 |
. . . . . . . . . . 11
       |
86 | 85 | sseli 3059 |
. . . . . . . . . 10
         |
87 | 86 | pm4.71ri 387 |
. . . . . . . . 9
      
    
     |
88 | 78, 87 | syl6bbr 197 |
. . . . . . . 8
           
   
     |
89 | 88 | notbid 639 |
. . . . . . 7
           
   
     |
90 | 14, 89 | bitrd 187 |
. . . . . 6
           
   
     |
91 | 90 | pm5.74da 437 |
. . . . 5
    
 
    

   
      |
92 | | bi2.04 247 |
. . . . 5
      


      |
93 | | con2b 641 |
. . . . 5
 
             
   |
94 | 91, 92, 93 | 3bitr3g 221 |
. . . 4
    
      
    
 
    |
95 | 94 | ralbidv2 2413 |
. . 3
    
 

             |
96 | 95 | pm5.32i 447 |
. 2
      

   
               |
97 | 1, 96 | bitri 183 |
1

               |