Step | Hyp | Ref
| Expression |
1 | | prmex 12096 |
. . . . . 6
 |
2 | 1 | mptex 5738 |
. . . . 5

    |
3 | | 1arith.1 |
. . . . 5
 

    |
4 | 2, 3 | fnmpti 5340 |
. . . 4
 |
5 | 3 | 1arithlem3 12346 |
. . . . . . 7
           |
6 | | nn0ex 9171 |
. . . . . . . 8
 |
7 | 6, 1 | elmap 6671 |
. . . . . . 7
                 |
8 | 5, 7 | sylibr 134 |
. . . . . 6
         |
9 | | 1zzd 9269 |
. . . . . . . 8
   |
10 | | nnz 9261 |
. . . . . . . 8
   |
11 | 9, 10 | fzfigd 10417 |
. . . . . . 7
       |
12 | | ffn 5361 |
. . . . . . . . . 10
               |
13 | | elpreima 5631 |
. . . . . . . . . 10
    
         

            |
14 | 5, 12, 13 | 3syl 17 |
. . . . . . . . 9
                        |
15 | 3 | 1arithlem2 12345 |
. . . . . . . . . . . 12
 
             |
16 | 15 | eleq1d 2246 |
. . . . . . . . . . 11
 
          
    |
17 | | prmz 12094 |
. . . . . . . . . . . . 13

  |
18 | | id 19 |
. . . . . . . . . . . . 13
   |
19 | | dvdsle 11833 |
. . . . . . . . . . . . 13
 
 
   |
20 | 17, 18, 19 | syl2anr 290 |
. . . . . . . . . . . 12
 
 
   |
21 | | pcelnn 12303 |
. . . . . . . . . . . . 13
     
   |
22 | 21 | ancoms 268 |
. . . . . . . . . . . 12
 
   
   |
23 | | prmnn 12093 |
. . . . . . . . . . . . . 14

  |
24 | | nnuz 9552 |
. . . . . . . . . . . . . 14
     |
25 | 23, 24 | eleqtrdi 2270 |
. . . . . . . . . . . . 13

      |
26 | | elfz5 10003 |
. . . . . . . . . . . . 13
           
   |
27 | 25, 10, 26 | syl2anr 290 |
. . . . . . . . . . . 12
 
     
   |
28 | 20, 22, 27 | 3imtr4d 203 |
. . . . . . . . . . 11
 
           |
29 | 16, 28 | sylbid 150 |
. . . . . . . . . 10
 
                 |
30 | 29 | expimpd 363 |
. . . . . . . . 9
                   |
31 | 14, 30 | sylbid 150 |
. . . . . . . 8
                  |
32 | 31 | ssrdv 3161 |
. . . . . . 7
                |
33 | | elfznn 10040 |
. . . . . . . . . . . . . 14
       |
34 | 33 | adantl 277 |
. . . . . . . . . . . . 13
 
       |
35 | | prmdc 12113 |
. . . . . . . . . . . . 13

DECID
  |
36 | 34, 35 | syl 14 |
. . . . . . . . . . . 12
 
     DECID   |
37 | 36 | adantr 276 |
. . . . . . . . . . 11
         DECID   |
38 | 5 | ad2antrr 488 |
. . . . . . . . . . . . . 14
                   |
39 | | simpr 110 |
. . . . . . . . . . . . . 14
           |
40 | 38, 39 | ffvelcdmd 5648 |
. . . . . . . . . . . . 13
                   |
41 | 40 | nn0zd 9362 |
. . . . . . . . . . . 12
                   |
42 | | elnndc 9601 |
. . . . . . . . . . . 12
        
DECID           |
43 | 41, 42 | syl 14 |
. . . . . . . . . . 11
         DECID           |
44 | | dcan2 934 |
. . . . . . . . . . 11
DECID DECID         DECID 
            |
45 | 37, 43, 44 | sylc 62 |
. . . . . . . . . 10
         DECID             |
46 | | simpr 110 |
. . . . . . . . . . . . 13
        
  |
47 | 46 | intnanrd 932 |
. . . . . . . . . . . 12
        
            |
48 | 47 | olcd 734 |
. . . . . . . . . . 11
        
                        |
49 | | df-dc 835 |
. . . . . . . . . . 11
DECID 
        
                        |
50 | 48, 49 | sylibr 134 |
. . . . . . . . . 10
        
DECID             |
51 | | exmiddc 836 |
. . . . . . . . . . 11
DECID     |
52 | 36, 51 | syl 14 |
. . . . . . . . . 10
 
         |
53 | 45, 50, 52 | mpjaodan 798 |
. . . . . . . . 9
 
     DECID             |
54 | | elpreima 5631 |
. . . . . . . . . . . 12
    
         

            |
55 | 5, 12, 54 | 3syl 17 |
. . . . . . . . . . 11
                        |
56 | 55 | dcbid 838 |
. . . . . . . . . 10
 DECID         
DECID              |
57 | 56 | adantr 276 |
. . . . . . . . 9
 
     DECID          DECID              |
58 | 53, 57 | mpbird 167 |
. . . . . . . 8
 
     DECID            |
59 | 58 | ralrimiva 2550 |
. . . . . . 7
      DECID            |
60 | | ssfidc 6928 |
. . . . . . 7
                   
    DECID                   
  |
61 | 11, 32, 59, 60 | syl3anc 1238 |
. . . . . 6
         
  |
62 | | cnveq 4797 |
. . . . . . . . 9
     
       |
63 | 62 | imaeq1d 4965 |
. . . . . . . 8
         
           |
64 | 63 | eleq1d 2246 |
. . . . . . 7
          
        
   |
65 | | 1arith.2 |
. . . . . . 7
          |
66 | 64, 65 | elrab2 2896 |
. . . . . 6
    
                   |
67 | 8, 61, 66 | sylanbrc 417 |
. . . . 5
       |
68 | 67 | rgen 2530 |
. . . 4
      |
69 | | ffnfv 5670 |
. . . 4
    
         |
70 | 4, 68, 69 | mpbir2an 942 |
. . 3
     |
71 | 15 | adantlr 477 |
. . . . . . . 8
             
   |
72 | 3 | 1arithlem2 12345 |
. . . . . . . . 9
 
             |
73 | 72 | adantll 476 |
. . . . . . . 8
             
   |
74 | 71, 73 | eqeq12d 2192 |
. . . . . . 7
                             |
75 | 74 | ralbidva 2473 |
. . . . . 6
 
                  
        |
76 | 3 | 1arithlem3 12346 |
. . . . . . 7
           |
77 | | ffn 5361 |
. . . . . . . 8
               |
78 | | eqfnfv 5609 |
. . . . . . . 8
                   
                    |
79 | 12, 77, 78 | syl2an 289 |
. . . . . . 7
                            
                   |
80 | 5, 76, 79 | syl2an 289 |
. . . . . 6
 
          
                   |
81 | | nnnn0 9172 |
. . . . . . 7
   |
82 | | nnnn0 9172 |
. . . . . . 7
   |
83 | | pc11 12313 |
. . . . . . 7
 
  

      |
84 | 81, 82, 83 | syl2an 289 |
. . . . . 6
 
  

      |
85 | 75, 80, 84 | 3bitr4d 220 |
. . . . 5
 
             |
86 | 85 | biimpd 144 |
. . . 4
 
             |
87 | 86 | rgen2 2563 |
. . 3
          
  |
88 | | dff13 5763 |
. . 3
    
     
         
    |
89 | 70, 87, 88 | mpbir2an 942 |
. 2
     |
90 | | eqid 2177 |
. . . . . 6
                               |
91 | | cnveq 4797 |
. . . . . . . . . . . 12
 
   |
92 | 91 | imaeq1d 4965 |
. . . . . . . . . . 11
     
       |
93 | 92 | eleq1d 2246 |
. . . . . . . . . 10
      
    
   |
94 | 93, 65 | elrab2 2896 |
. . . . . . . . 9

           |
95 | 94 | simplbi 274 |
. . . . . . . 8
     |
96 | 6, 1 | elmap 6671 |
. . . . . . . 8
         |
97 | 95, 96 | sylib 122 |
. . . . . . 7
       |
98 | 97 | ad2antrr 488 |
. . . . . 6
  
        
      |
99 | | simplr 528 |
. . . . . . 7
  
        
  |
100 | 99 | peano2nnd 8923 |
. . . . . 6
  
        
    |
101 | 99 | adantr 276 |
. . . . . . . . . . 11
     
         
 
  |
102 | 101 | nnred 8921 |
. . . . . . . . . 10
     
         
 
  |
103 | | peano2re 8083 |
. . . . . . . . . . 11
     |
104 | 102, 103 | syl 14 |
. . . . . . . . . 10
     
         
 
    |
105 | 23 | ad2antrl 490 |
. . . . . . . . . . 11
     
         
 
  |
106 | 105 | nnred 8921 |
. . . . . . . . . 10
     
         
 
  |
107 | 102 | ltp1d 8876 |
. . . . . . . . . 10
     
         
 
    |
108 | | simprr 531 |
. . . . . . . . . 10
     
         
 
    |
109 | 102, 104,
106, 107, 108 | ltletrd 8370 |
. . . . . . . . 9
     
         
 
  |
110 | 101 | nnzd 9363 |
. . . . . . . . . 10
     
         
 
  |
111 | 17 | ad2antrl 490 |
. . . . . . . . . 10
     
         
 
  |
112 | | zltnle 9288 |
. . . . . . . . . 10
 
 
   |
113 | 110, 111,
112 | syl2anc 411 |
. . . . . . . . 9
     
         
 

   |
114 | 109, 113 | mpbid 147 |
. . . . . . . 8
     
         
 
  |
115 | | simprl 529 |
. . . . . . . . . . 11
     
         
 
  |
116 | 115 | biantrurd 305 |
. . . . . . . . . 10
     
         
 
              |
117 | 97 | ad3antrrr 492 |
. . . . . . . . . . 11
     
         
 
      |
118 | | ffn 5361 |
. . . . . . . . . . 11
       |
119 | | elpreima 5631 |
. . . . . . . . . . 11

     

        |
120 | 117, 118,
119 | 3syl 17 |
. . . . . . . . . 10
     
         
 
     
         |
121 | 116, 120 | bitr4d 191 |
. . . . . . . . 9
     
         
 
             |
122 | | breq1 4003 |
. . . . . . . . . . 11
 
   |
123 | 122 | rspccv 2838 |
. . . . . . . . . 10
 
               |
124 | 123 | ad2antlr 489 |
. . . . . . . . 9
     
         
 
     
   |
125 | 121, 124 | sylbid 150 |
. . . . . . . 8
     
         
 
    
   |
126 | 114, 125 | mtod 663 |
. . . . . . 7
     
         
 
      |
127 | 117, 115 | ffvelcdmd 5648 |
. . . . . . . . 9
     
         
 
      |
128 | | elnn0 9167 |
. . . . . . . . 9
    
            |
129 | 127, 128 | sylib 122 |
. . . . . . . 8
     
         
 
            |
130 | 129 | ord 724 |
. . . . . . 7
     
         
 
            |
131 | 126, 130 | mpd 13 |
. . . . . 6
     
         
 
      |
132 | 3, 90, 98, 100, 131 | 1arithlem4 12347 |
. . . . 5
  
        
       |
133 | | cnvimass 4987 |
. . . . . . 7
    
 |
134 | 97 | fdmd 5368 |
. . . . . . . 8

  |
135 | | prmssnn 12095 |
. . . . . . . 8
 |
136 | 134, 135 | eqsstrdi 3207 |
. . . . . . 7
   |
137 | 133, 136 | sstrid 3166 |
. . . . . 6
        |
138 | 94 | simprbi 275 |
. . . . . 6
     
  |
139 | | fiubnn 10794 |
. . . . . 6
      
    
        
  |
140 | 137, 138,
139 | syl2anc 411 |
. . . . 5
           |
141 | 132, 140 | r19.29a 2620 |
. . . 4
        |
142 | 141 | rgen 2530 |
. . 3

      |
143 | | dffo3 5659 |
. . 3
    
     

       |
144 | 70, 142, 143 | mpbir2an 942 |
. 2
     |
145 | | df-f1o 5219 |
. 2
                 |
146 | 89, 144, 145 | mpbir2an 942 |
1
     |