Step | Hyp | Ref
| Expression |
1 | | zex 10759 |
. . . . . . 7
 |
2 | | prmz 13878 |
. . . . . . . 8

  |
3 | 2 | ssriv 3461 |
. . . . . . 7
 |
4 | 1, 3 | ssexi 4538 |
. . . . . 6
 |
5 | 4 | mptex 6050 |
. . . . 5

    |
6 | | 1arith.1 |
. . . . 5
 

    |
7 | 5, 6 | fnmpti 5640 |
. . . 4
 |
8 | 6 | 1arithlem3 14097 |
. . . . . . 7
           |
9 | | nn0ex 10689 |
. . . . . . . 8
 |
10 | 9, 4 | elmap 7344 |
. . . . . . 7
                 |
11 | 8, 10 | sylibr 212 |
. . . . . 6
         |
12 | | fzfi 11904 |
. . . . . . 7
     |
13 | | ffn 5660 |
. . . . . . . . . 10
               |
14 | | elpreima 5925 |
. . . . . . . . . 10
    
         

            |
15 | 8, 13, 14 | 3syl 20 |
. . . . . . . . 9
                        |
16 | 6 | 1arithlem2 14096 |
. . . . . . . . . . . 12
 
             |
17 | 16 | eleq1d 2520 |
. . . . . . . . . . 11
 
          
    |
18 | | id 22 |
. . . . . . . . . . . . 13
   |
19 | | dvdsle 13689 |
. . . . . . . . . . . . 13
 
 
   |
20 | 2, 18, 19 | syl2anr 478 |
. . . . . . . . . . . 12
 
 
   |
21 | | pcelnn 14047 |
. . . . . . . . . . . . 13
     
   |
22 | 21 | ancoms 453 |
. . . . . . . . . . . 12
 
   
   |
23 | | prmnn 13877 |
. . . . . . . . . . . . . 14

  |
24 | | nnuz 11000 |
. . . . . . . . . . . . . 14
     |
25 | 23, 24 | syl6eleq 2549 |
. . . . . . . . . . . . 13

      |
26 | | nnz 10772 |
. . . . . . . . . . . . 13
   |
27 | | elfz5 11555 |
. . . . . . . . . . . . 13
           
   |
28 | 25, 26, 27 | syl2anr 478 |
. . . . . . . . . . . 12
 
     
   |
29 | 20, 22, 28 | 3imtr4d 268 |
. . . . . . . . . . 11
 
           |
30 | 17, 29 | sylbid 215 |
. . . . . . . . . 10
 
                 |
31 | 30 | expimpd 603 |
. . . . . . . . 9
                   |
32 | 15, 31 | sylbid 215 |
. . . . . . . 8
                  |
33 | 32 | ssrdv 3463 |
. . . . . . 7
                |
34 | | ssfi 7637 |
. . . . . . 7
                            
  |
35 | 12, 33, 34 | sylancr 663 |
. . . . . 6
         
  |
36 | | cnveq 5114 |
. . . . . . . . 9
     
       |
37 | 36 | imaeq1d 5269 |
. . . . . . . 8
         
           |
38 | 37 | eleq1d 2520 |
. . . . . . 7
          
        
   |
39 | | 1arith.2 |
. . . . . . 7
          |
40 | 38, 39 | elrab2 3219 |
. . . . . 6
    
                   |
41 | 11, 35, 40 | sylanbrc 664 |
. . . . 5
       |
42 | 41 | rgen 2892 |
. . . 4
      |
43 | | ffnfv 5971 |
. . . 4
    
         |
44 | 7, 42, 43 | mpbir2an 911 |
. . 3
     |
45 | 16 | adantlr 714 |
. . . . . . . 8
             
   |
46 | 6 | 1arithlem2 14096 |
. . . . . . . . 9
 
             |
47 | 46 | adantll 713 |
. . . . . . . 8
             
   |
48 | 45, 47 | eqeq12d 2473 |
. . . . . . 7
                             |
49 | 48 | ralbidva 2839 |
. . . . . 6
 
                  
        |
50 | 6 | 1arithlem3 14097 |
. . . . . . 7
           |
51 | | ffn 5660 |
. . . . . . . 8
               |
52 | | eqfnfv 5899 |
. . . . . . . 8
                   
                    |
53 | 13, 51, 52 | syl2an 477 |
. . . . . . 7
                            
                   |
54 | 8, 50, 53 | syl2an 477 |
. . . . . 6
 
          
                   |
55 | | nnnn0 10690 |
. . . . . . 7
   |
56 | | nnnn0 10690 |
. . . . . . 7
   |
57 | | pc11 14057 |
. . . . . . 7
 
  

      |
58 | 55, 56, 57 | syl2an 477 |
. . . . . 6
 
  

      |
59 | 49, 54, 58 | 3bitr4d 285 |
. . . . 5
 
             |
60 | 59 | biimpd 207 |
. . . 4
 
             |
61 | 60 | rgen2a 2893 |
. . 3
          
  |
62 | | dff13 6073 |
. . 3
    
     
         
    |
63 | 44, 61, 62 | mpbir2an 911 |
. 2
     |
64 | | cnvimass 5290 |
. . . . . . 7
    
 |
65 | | cnveq 5114 |
. . . . . . . . . . . . . 14
 
   |
66 | 65 | imaeq1d 5269 |
. . . . . . . . . . . . 13
     
       |
67 | 66 | eleq1d 2520 |
. . . . . . . . . . . 12
      
    
   |
68 | 67, 39 | elrab2 3219 |
. . . . . . . . . . 11

           |
69 | 68 | simplbi 460 |
. . . . . . . . . 10
     |
70 | 9, 4 | elmap 7344 |
. . . . . . . . . 10
         |
71 | 69, 70 | sylib 196 |
. . . . . . . . 9
       |
72 | | fdm 5664 |
. . . . . . . . 9
       |
73 | 71, 72 | syl 16 |
. . . . . . . 8

  |
74 | | zssre 10757 |
. . . . . . . . 9
 |
75 | 3, 74 | sstri 3466 |
. . . . . . . 8
 |
76 | 73, 75 | syl6eqss 3507 |
. . . . . . 7
   |
77 | 64, 76 | syl5ss 3468 |
. . . . . 6
        |
78 | 68 | simprbi 464 |
. . . . . 6
     
  |
79 | | fimaxre2 10382 |
. . . . . 6
      
    
        
  |
80 | 77, 78, 79 | syl2anc 661 |
. . . . 5
           |
81 | | eqid 2451 |
. . . . . . . 8
                               |
82 | 71 | ad2antrr 725 |
. . . . . . . 8
  
        
      |
83 | | simplr 754 |
. . . . . . . . . . 11
  
        
  |
84 | | 0re 9490 |
. . . . . . . . . . 11
 |
85 | | ifcl 3932 |
. . . . . . . . . . 11
 
        |
86 | 83, 84, 85 | sylancl 662 |
. . . . . . . . . 10
  
        
 
     |
87 | | max1 11261 |
. . . . . . . . . . 11
 

 
     |
88 | 84, 83, 87 | sylancr 663 |
. . . . . . . . . 10
  
        
       |
89 | | flge0nn0 11776 |
. . . . . . . . . 10
      
 
   
           |
90 | 86, 88, 89 | syl2anc 661 |
. . . . . . . . 9
  
        
           |
91 | | nn0p1nn 10723 |
. . . . . . . . 9
     
                 |
92 | 90, 91 | syl 16 |
. . . . . . . 8
  
        
             |
93 | 83 | adantr 465 |
. . . . . . . . . . . 12
     
                  
 
  |
94 | 92 | adantr 465 |
. . . . . . . . . . . . 13
     
                  
 
             |
95 | 94 | nnred 10441 |
. . . . . . . . . . . 12
     
                  
 
             |
96 | | simprl 755 |
. . . . . . . . . . . . 13
     
                  
 
  |
97 | 75, 96 | sseldi 3455 |
. . . . . . . . . . . 12
     
                  
 
  |
98 | 86 | adantr 465 |
. . . . . . . . . . . . 13
     
                  
 
 
     |
99 | | max2 11263 |
. . . . . . . . . . . . . 14
 

 
     |
100 | 84, 93, 99 | sylancr 663 |
. . . . . . . . . . . . 13
     
                  
 
       |
101 | | flltp1 11760 |
. . . . . . . . . . . . . 14
                
       |
102 | 98, 101 | syl 16 |
. . . . . . . . . . . . 13
     
                  
 
 
                |
103 | 93, 98, 95, 100, 102 | lelttrd 9633 |
. . . . . . . . . . . 12
     
                  
 
             |
104 | | simprr 756 |
. . . . . . . . . . . 12
     
                  
 
             |
105 | 93, 95, 97, 103, 104 | ltletrd 9635 |
. . . . . . . . . . 11
     
                  
 
  |
106 | 93, 97 | ltnled 9625 |
. . . . . . . . . . 11
     
                  
 

   |
107 | 105, 106 | mpbid 210 |
. . . . . . . . . 10
     
                  
 
  |
108 | 96 | biantrurd 508 |
. . . . . . . . . . . 12
     
                  
 
              |
109 | 82 | adantr 465 |
. . . . . . . . . . . . 13
     
                  
 
      |
110 | | ffn 5660 |
. . . . . . . . . . . . 13
       |
111 | | elpreima 5925 |
. . . . . . . . . . . . 13

     

        |
112 | 109, 110,
111 | 3syl 20 |
. . . . . . . . . . . 12
     
                  
 
     
         |
113 | 108, 112 | bitr4d 256 |
. . . . . . . . . . 11
     
                  
 
             |
114 | | simplr 754 |
. . . . . . . . . . . 12
     
                  
 
         |
115 | | breq1 4396 |
. . . . . . . . . . . . 13
 
   |
116 | 115 | rspccv 3169 |
. . . . . . . . . . . 12
 
               |
117 | 114, 116 | syl 16 |
. . . . . . . . . . 11
     
                  
 
     
   |
118 | 113, 117 | sylbid 215 |
. . . . . . . . . 10
     
                  
 
    
   |
119 | 107, 118 | mtod 177 |
. . . . . . . . 9
     
                  
 
      |
120 | 109, 96 | ffvelrnd 5946 |
. . . . . . . . . . 11
     
                  
 
      |
121 | | elnn0 10685 |
. . . . . . . . . . 11
    
            |
122 | 120, 121 | sylib 196 |
. . . . . . . . . 10
     
                  
 
            |
123 | 122 | ord 377 |
. . . . . . . . 9
     
                  
 
            |
124 | 119, 123 | mpd 15 |
. . . . . . . 8
     
                  
 
      |
125 | 6, 81, 82, 92, 124 | 1arithlem4 14098 |
. . . . . . 7
  
        
       |
126 | 125 | ex 434 |
. . . . . 6
 
         
       |
127 | 126 | rexlimdva 2940 |
. . . . 5
  
      
        |
128 | 80, 127 | mpd 15 |
. . . 4
        |
129 | 128 | rgen 2892 |
. . 3

      |
130 | | dffo3 5960 |
. . 3
    
     

       |
131 | 44, 129, 130 | mpbir2an 911 |
. 2
     |
132 | | df-f1o 5526 |
. 2
                 |
133 | 63, 131, 132 | mpbir2an 911 |
1
     |