Step | Hyp | Ref
| Expression |
1 | | hashf 12522 |
. . . . 5
        |
2 | | ffun 5731 |
. . . . 5
          |
3 | 1, 2 | ax-mp 5 |
. . . 4
 |
4 | | erdszelem.a |
. . . . 5
       |
5 | | erdsze.n |
. . . . . 6
   |
6 | | erdsze.f |
. . . . . 6
           |
7 | | erdszelem.k |
. . . . . 6
                 
               |
8 | | erdszelem.o |
. . . . . 6
 |
9 | 5, 6, 7, 8 | erdszelem5 29918 |
. . . . 5
 
                                 |
10 | 4, 9 | mpdan 674 |
. . . 4
               
             |
11 | | fvelima 5917 |
. . . 4
 
                          
        
                    |
12 | 3, 10, 11 | sylancr 669 |
. . 3
                              |
13 | | eqid 2451 |
. . . . . 6
                         
           |
14 | 13 | erdszelem1 29914 |
. . . . 5
         
        
    
            |
15 | | fzfid 12186 |
. . . . . . . . . . 11
   
    
                           |
16 | | simplr1 1050 |
. . . . . . . . . . 11
   
    
                    
      |
17 | | ssfi 7792 |
. . . . . . . . . . 11
             |
18 | 15, 16, 17 | syl2anc 667 |
. . . . . . . . . 10
   
    
                       |
19 | | hashcl 12538 |
. . . . . . . . . 10
       |
20 | 18, 19 | syl 17 |
. . . . . . . . 9
   
    
                           |
21 | 20 | nn0red 10926 |
. . . . . . . 8
   
    
                           |
22 | | eqid 2451 |
. . . . . . . . . . . . . . 15
                         
           |
23 | 22 | erdszelem2 29915 |
. . . . . . . . . . . . . 14
                                  
            |
24 | 23 | simpri 464 |
. . . . . . . . . . . . 13
          
            |
25 | | nnssre 10613 |
. . . . . . . . . . . . 13
 |
26 | 24, 25 | sstri 3441 |
. . . . . . . . . . . 12
          
            |
27 | 26 | a1i 11 |
. . . . . . . . . . 11
   
    
                                             |
28 | | erdszelem.l |
. . . . . . . . . . . . . . . . . 18
   |
29 | | elfznn 11828 |
. . . . . . . . . . . . . . . . . . . . 21
       |
30 | 4, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
31 | 30 | nnred 10624 |
. . . . . . . . . . . . . . . . . . 19
   |
32 | | erdszelem.b |
. . . . . . . . . . . . . . . . . . . . 21
       |
33 | | elfznn 11828 |
. . . . . . . . . . . . . . . . . . . . 21
       |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
35 | 34 | nnred 10624 |
. . . . . . . . . . . . . . . . . . 19
   |
36 | 31, 35 | ltnled 9782 |
. . . . . . . . . . . . . . . . . 18
 
   |
37 | 28, 36 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
   |
38 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . 17
       |
39 | 37, 38 | nsyl 125 |
. . . . . . . . . . . . . . . 16
       |
40 | 39 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
   
    
                    
      |
41 | 16, 40 | ssneldd 3435 |
. . . . . . . . . . . . . 14
   
    
                    
  |
42 | 32 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
   
    
                    
      |
43 | | hashunsng 12571 |
. . . . . . . . . . . . . . 15
       
                 |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . 14
   
    
                      
                  |
45 | 18, 41, 44 | mp2and 685 |
. . . . . . . . . . . . 13
   
    
                                     |
46 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . . . . 21
       |
47 | 4, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
48 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . . . . 21
       |
49 | 32, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
50 | 31, 35, 28 | ltled 9783 |
. . . . . . . . . . . . . . . . . . . 20

  |
51 | | eluz2 11165 |
. . . . . . . . . . . . . . . . . . . 20
         |
52 | 47, 49, 50, 51 | syl3anbrc 1192 |
. . . . . . . . . . . . . . . . . . 19
       |
53 | | fzss2 11838 |
. . . . . . . . . . . . . . . . . . 19
    
          |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    
      |
55 | 54 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
   
    
                        
      |
56 | 16, 55 | sstrd 3442 |
. . . . . . . . . . . . . . . 16
   
    
                    
      |
57 | | elfz1end 11829 |
. . . . . . . . . . . . . . . . . . 19

      |
58 | 34, 57 | sylib 200 |
. . . . . . . . . . . . . . . . . 18
       |
59 | 58 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
   
    
                    
      |
60 | 59 | snssd 4117 |
. . . . . . . . . . . . . . . 16
   
    
                             |
61 | 56, 60 | unssd 3610 |
. . . . . . . . . . . . . . 15
   
    
                               |
62 | | simplr2 1051 |
. . . . . . . . . . . . . . . . . . . . 21
   
    
                      
         |
63 | | f1f 5779 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
64 | 6, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
65 | 64 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
                               |
66 | | elfzuz3 11797 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
67 | | fzss2 11838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
          |
68 | 4, 66, 67 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
      |
69 | 68 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
    
                        
      |
70 | 16, 69 | sstrd 3442 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
                    
      |
71 | | fzssuz 11839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
72 | | uzssz 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
73 | | zssre 10944 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
74 | 72, 73 | sstri 3441 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
75 | 71, 74 | sstri 3441 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
76 | | ltso 9714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
77 | | soss 4773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       |
78 | 75, 76, 77 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
79 | | soisores 6218 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                         



              |
80 | 78, 8, 79 | mpanl12 688 |
. . . . . . . . . . . . . . . . . . . . . 22
                        



              |
81 | 65, 70, 80 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . 21
   
    
                              



              |
82 | 62, 81 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . 20
   
    
                     

              |
83 | 82 | r19.21bi 2757 |
. . . . . . . . . . . . . . . . . . 19
         
                    
                |
84 | 16 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
                    
       |
85 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
                    

  |
87 | 70 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
                    
       |
88 | 75, 87 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
                    
   |
89 | 4 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
                    
       |
90 | 89, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
                    
   |
91 | 90 | nnred 10624 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
                    
   |
92 | 88, 91 | lenltd 9781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
                    
     |
93 | 86, 92 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
                    
   |
94 | 62 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
                    
  
         |
95 | | simplr3 1052 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
    
                    
  |
96 | 95 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
                    
   |
97 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
                    
   |
98 | | isorel 6217 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                            |
99 | | fvres 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
100 | | fvres 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
101 | 99, 100 | breqan12d 4418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
           
   
             |
102 | 101 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                    
   
             |
103 | 98, 102 | bitrd 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                        |
104 | 94, 96, 97, 103 | syl12anc 1266 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
                    
               |
105 | 93, 104 | mtbid 302 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
                    
             |
106 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
                    
             |
107 | 65 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
                    
           |
108 | 107, 87 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
                    
       |
109 | 107, 89 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
                    
       |
110 | 42 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
                    
       |
111 | 107, 110 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
                    
       |
112 | | sotr2 4784 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                                     |
113 | 8, 112 | mpan 676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                          
          
             |
114 | 108, 109,
111, 113 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
                    
                                     |
115 | 105, 106,
114 | mp2and 685 |
. . . . . . . . . . . . . . . . . . . . . 22
         
                    
             |
116 | 115 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . 21
         
                    
               |
117 | | elsni 3993 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
118 | 117 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
119 | 118 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
120 | 119 | imbi2d 318 |
. . . . . . . . . . . . . . . . . . . . 21
    
           
              |
121 | 116, 120 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . . . . . 20
         
                    
   
               |
122 | 121 | ralrimiv 2800 |
. . . . . . . . . . . . . . . . . . 19
         
                    
   

             |
123 | | ralunb 3615 |
. . . . . . . . . . . . . . . . . . 19
 
                   
              
              |
124 | 83, 122, 123 | sylanbrc 670 |
. . . . . . . . . . . . . . . . . 18
         
                    
                     |
125 | 124 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . 17
   
    
                     

                   |
126 | 61 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . . . 22
         
                    
    
      |
127 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
128 | 127 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
                    
       |
129 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
130 | 129 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
131 | 130 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
                    
       |
132 | 35 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
                    
       |
133 | 131, 132 | lenltd 9781 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
                    
         |
134 | 128, 133 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . 22
         
                    
    
  |
135 | 126, 134 | syldan 473 |
. . . . . . . . . . . . . . . . . . . . 21
         
                    
    
  |
136 | 135 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . 20
         
                    
    

             |
137 | 136 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . . 19
   
    
                     
                   |
138 | | elsni 3993 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
139 | 138 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . 21
       |
140 | 139 | imbi1d 319 |
. . . . . . . . . . . . . . . . . . . 20
    
           
              |
141 | 140 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . 19
                     
                     |
142 | 137, 141 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . . . 18
   
    
                       
                     |
143 | 142 | ralrimiv 2800 |
. . . . . . . . . . . . . . . . 17
   
    
                     
                       |
144 | | ralunb 3615 |
. . . . . . . . . . . . . . . . 17
 
                      
 

                     
                    |
145 | 125, 143,
144 | sylanbrc 670 |
. . . . . . . . . . . . . . . 16
   
    
                     
                         |
146 | 42 | snssd 4117 |
. . . . . . . . . . . . . . . . . 18
   
    
                             |
147 | 70, 146 | unssd 3610 |
. . . . . . . . . . . . . . . . 17
   
    
                               |
148 | | soisores 6218 |
. . . . . . . . . . . . . . . . . 18
     
             
     
      
               
                          |
149 | 78, 8, 148 | mpanl12 688 |
. . . . . . . . . . . . . . . . 17
                         
              
                           |
150 | 65, 147, 149 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
   
    
                           
              
                           |
151 | 145, 150 | mpbird 236 |
. . . . . . . . . . . . . . 15
   
    
                          
                 |
152 | | ssun2 3598 |
. . . . . . . . . . . . . . . 16
       |
153 | | snssg 4105 |
. . . . . . . . . . . . . . . . 17
     
             |
154 | 59, 153 | syl 17 |
. . . . . . . . . . . . . . . 16
   
    
                         
         |
155 | 152, 154 | mpbiri 237 |
. . . . . . . . . . . . . . 15
   
    
                    
      |
156 | 22 | erdszelem1 29914 |
. . . . . . . . . . . . . . 15
                      
         
                           |
157 | 61, 151, 155, 156 | syl3anbrc 1192 |
. . . . . . . . . . . . . 14
   
    
                                             |
158 | | vex 3048 |
. . . . . . . . . . . . . . . . 17
 |
159 | | snex 4641 |
. . . . . . . . . . . . . . . . 17
 
 |
160 | 158, 159 | unex 6589 |
. . . . . . . . . . . . . . . 16
     |
161 | 1 | fdmi 5734 |
. . . . . . . . . . . . . . . 16
 |
162 | 160, 161 | eleqtrri 2528 |
. . . . . . . . . . . . . . 15
     |
163 | | funfvima 6140 |
. . . . . . . . . . . . . . 15
 
    
                                         
              |
164 | 3, 162, 163 | mp2an 678 |
. . . . . . . . . . . . . 14
                                         
             |
165 | 157, 164 | syl 17 |
. . . . . . . . . . . . 13
   
    
                                                     |
166 | 45, 165 | eqeltrrd 2530 |
. . . . . . . . . . . 12
   
    
                                                   |
167 | | ne0i 3737 |
. . . . . . . . . . . 12
                                                     |
168 | 166, 167 | syl 17 |
. . . . . . . . . . 11
   
    
                                             |
169 | 23 | simpli 460 |
. . . . . . . . . . . 12
          
            |
170 | | fimaxre2 10552 |
. . . . . . . . . . . 12
                       
           
           
           
              |
171 | 27, 169, 170 | sylancl 668 |
. . . . . . . . . . 11
   
    
                     
           
              |
172 | | suprub 10570 |
. . . . . . . . . . 11
                        
           
                                  
                             
                                  |
173 | 27, 168, 171, 166, 172 | syl31anc 1271 |
. . . . . . . . . 10
   
    
                                       
               |
174 | 5, 6, 7 | erdszelem3 29916 |
. . . . . . . . . . . 12
                     
               |
175 | 32, 174 | syl 17 |
. . . . . . . . . . 11
                                 |
176 | 175 | ad2antrr 732 |
. . . . . . . . . 10
   
    
                                                     |
177 | 173, 176 | breqtrrd 4429 |
. . . . . . . . 9
   
    
                                 |
178 | 5, 6, 7, 8 | erdszelem6 29919 |
. . . . . . . . . . . . 13
           |
179 | 178, 32 | ffvelrnd 6023 |
. . . . . . . . . . . 12
       |
180 | 179 | ad2antrr 732 |
. . . . . . . . . . 11
   
    
                           |
181 | 180 | nnnn0d 10925 |
. . . . . . . . . 10
   
    
                           |
182 | | nn0ltp1le 10994 |
. . . . . . . . . 10
               
   
             |
183 | 20, 181, 182 | syl2anc 667 |
. . . . . . . . 9
   
    
                         
   
             |
184 | 177, 183 | mpbird 236 |
. . . . . . . 8
   
    
                               |
185 | 21, 184 | ltned 9771 |
. . . . . . 7
   
    
                               |
186 | 185 | ex 436 |
. . . . . 6
 
    
                                 |
187 | | neeq1 2686 |
. . . . . . 7
                 
           |
188 | 187 | imbi2d 318 |
. . . . . 6
                                                     |
189 | 186, 188 | syl5ibcom 224 |
. . . . 5
 
    
                                           |
190 | 14, 189 | sylan2b 478 |
. . . 4
 
                                      
            |
191 | 190 | rexlimdva 2879 |
. . 3
          
                            
            |
192 | 12, 191 | mpd 15 |
. 2
                       |
193 | 192 | necon2bd 2640 |
1
         
             |