Step | Hyp | Ref
| Expression |
1 | | hashf 13125 |
. . . . 5
|
2 | | ffun 6048 |
. . . . 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 31177 |
. . . . 5
|
10 | 4, 9 | mpdan 702 |
. . . 4
|
11 | | fvelima 6248 |
. . . 4
|
12 | 3, 10, 11 | sylancr 695 |
. . 3
|
13 | | eqid 2622 |
. . . . . 6
|
14 | 13 | erdszelem1 31173 |
. . . . 5
|
15 | | fzfid 12772 |
. . . . . . . . . . 11
|
16 | | simplr1 1103 |
. . . . . . . . . . 11
|
17 | | ssfi 8180 |
. . . . . . . . . . 11
|
18 | 15, 16, 17 | syl2anc 693 |
. . . . . . . . . 10
|
19 | | hashcl 13147 |
. . . . . . . . . 10
|
20 | 18, 19 | syl 17 |
. . . . . . . . 9
|
21 | 20 | nn0red 11352 |
. . . . . . . 8
|
22 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
23 | 22 | erdszelem2 31174 |
. . . . . . . . . . . . . 14
|
24 | 23 | simpri 478 |
. . . . . . . . . . . . 13
|
25 | | nnssre 11024 |
. . . . . . . . . . . . 13
|
26 | 24, 25 | sstri 3612 |
. . . . . . . . . . . 12
|
27 | 26 | a1i 11 |
. . . . . . . . . . 11
|
28 | | erdszelem.l |
. . . . . . . . . . . . . . . . . 18
|
29 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | 4, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 30 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | erdszelem.b |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 34 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 31, 35 | ltnled 10184 |
. . . . . . . . . . . . . . . . . 18
|
37 | 28, 36 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
38 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . 17
|
39 | 37, 38 | nsyl 135 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
41 | 16, 40 | ssneldd 3606 |
. . . . . . . . . . . . . 14
|
42 | 32 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
43 | | hashunsng 13181 |
. . . . . . . . . . . . . . 15
|
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . 14
|
45 | 18, 41, 44 | mp2and 715 |
. . . . . . . . . . . . 13
|
46 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | 4, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
48 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . 21
|
49 | 32, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
50 | 31, 35, 28 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | 47, 49, 50, 51 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . 19
|
53 | | fzss2 12381 |
. . . . . . . . . . . . . . . . . . 19
|
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
55 | 54 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
56 | 16, 55 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
|
57 | | elfz1end 12371 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 34, 57 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
|
59 | 58 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
60 | 59 | snssd 4340 |
. . . . . . . . . . . . . . . 16
|
61 | 56, 60 | unssd 3789 |
. . . . . . . . . . . . . . 15
|
62 | | simplr2 1104 |
. . . . . . . . . . . . . . . . . . . . 21
|
63 | | f1f 6101 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
64 | 6, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | 64 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
66 | | elfzuz3 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
67 | | fzss2 12381 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
68 | 4, 66, 67 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
69 | 68 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
70 | 16, 69 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . . . 22
|
71 | | fzssuz 12382 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
72 | | uzssz 11707 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
73 | | zssre 11384 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
74 | 72, 73 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
75 | 71, 74 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
76 | | ltso 10118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
77 | | soss 5053 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
78 | 75, 76, 77 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
79 | | soisores 6577 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
80 | 78, 8, 79 | mpanl12 718 |
. . . . . . . . . . . . . . . . . . . . . 22
|
81 | 65, 70, 80 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
82 | 62, 81 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
83 | 82 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 16 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
85 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
87 | 70 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
88 | 75, 87 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
89 | 4 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
90 | 89, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
91 | 90 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
92 | 88, 91 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
93 | 86, 92 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
94 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
95 | | simplr3 1105 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
96 | 95 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
97 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
98 | | isorel 6576 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
99 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
100 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
101 | 99, 100 | breqan12d 4669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
103 | 98, 102 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
104 | 94, 96, 97, 103 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
105 | 93, 104 | mtbid 314 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
106 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
107 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
108 | 107, 87 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
109 | 107, 89 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
110 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
111 | 107, 110 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
112 | | sotr2 5064 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
113 | 8, 112 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
114 | 108, 109,
111, 113 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
115 | 105, 106,
114 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . . 22
|
116 | 115 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
|
117 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
118 | 117 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
119 | 118 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . 22
|
120 | 119 | imbi2d 330 |
. . . . . . . . . . . . . . . . . . . . 21
|
121 | 116, 120 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . 20
|
122 | 121 | ralrimiv 2965 |
. . . . . . . . . . . . . . . . . . 19
|
123 | | ralunb 3794 |
. . . . . . . . . . . . . . . . . . 19
|
124 | 83, 122, 123 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . 18
|
125 | 124 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
|
126 | 61 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . 22
|
127 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
128 | 127 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
129 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
130 | 129 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
131 | 130 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
132 | 35 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
133 | 131, 132 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
134 | 128, 133 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
|
135 | 126, 134 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . 21
|
136 | 135 | pm2.21d 118 |
. . . . . . . . . . . . . . . . . . . 20
|
137 | 136 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . 19
|
138 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . 22
|
139 | 138 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
|
140 | 139 | imbi1d 331 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | 140 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . 19
|
142 | 137, 141 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . 18
|
143 | 142 | ralrimiv 2965 |
. . . . . . . . . . . . . . . . 17
|
144 | | ralunb 3794 |
. . . . . . . . . . . . . . . . 17
|
145 | 125, 143,
144 | sylanbrc 698 |
. . . . . . . . . . . . . . . 16
|
146 | 42 | snssd 4340 |
. . . . . . . . . . . . . . . . . 18
|
147 | 70, 146 | unssd 3789 |
. . . . . . . . . . . . . . . . 17
|
148 | | soisores 6577 |
. . . . . . . . . . . . . . . . . 18
|
149 | 78, 8, 148 | mpanl12 718 |
. . . . . . . . . . . . . . . . 17
|
150 | 65, 147, 149 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
151 | 145, 150 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
152 | | ssun2 3777 |
. . . . . . . . . . . . . . . 16
|
153 | | snssg 4327 |
. . . . . . . . . . . . . . . . 17
|
154 | 59, 153 | syl 17 |
. . . . . . . . . . . . . . . 16
|
155 | 152, 154 | mpbiri 248 |
. . . . . . . . . . . . . . 15
|
156 | 22 | erdszelem1 31173 |
. . . . . . . . . . . . . . 15
|
157 | 61, 151, 155, 156 | syl3anbrc 1246 |
. . . . . . . . . . . . . 14
|
158 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
159 | | snex 4908 |
. . . . . . . . . . . . . . . . 17
|
160 | 158, 159 | unex 6956 |
. . . . . . . . . . . . . . . 16
|
161 | 1 | fdmi 6052 |
. . . . . . . . . . . . . . . 16
|
162 | 160, 161 | eleqtrri 2700 |
. . . . . . . . . . . . . . 15
|
163 | | funfvima 6492 |
. . . . . . . . . . . . . . 15
|
164 | 3, 162, 163 | mp2an 708 |
. . . . . . . . . . . . . 14
|
165 | 157, 164 | syl 17 |
. . . . . . . . . . . . 13
|
166 | 45, 165 | eqeltrrd 2702 |
. . . . . . . . . . . 12
|
167 | | ne0i 3921 |
. . . . . . . . . . . 12
|
168 | 166, 167 | syl 17 |
. . . . . . . . . . 11
|
169 | 23 | simpli 474 |
. . . . . . . . . . . 12
|
170 | | fimaxre2 10969 |
. . . . . . . . . . . 12
|
171 | 27, 169, 170 | sylancl 694 |
. . . . . . . . . . 11
|
172 | | suprub 10984 |
. . . . . . . . . . 11
|
173 | 27, 168, 171, 166, 172 | syl31anc 1329 |
. . . . . . . . . 10
|
174 | 5, 6, 7 | erdszelem3 31175 |
. . . . . . . . . . . 12
|
175 | 32, 174 | syl 17 |
. . . . . . . . . . 11
|
176 | 175 | ad2antrr 762 |
. . . . . . . . . 10
|
177 | 173, 176 | breqtrrd 4681 |
. . . . . . . . 9
|
178 | 5, 6, 7, 8 | erdszelem6 31178 |
. . . . . . . . . . . . 13
|
179 | 178, 32 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
180 | 179 | ad2antrr 762 |
. . . . . . . . . . 11
|
181 | 180 | nnnn0d 11351 |
. . . . . . . . . 10
|
182 | | nn0ltp1le 11435 |
. . . . . . . . . 10
|
183 | 20, 181, 182 | syl2anc 693 |
. . . . . . . . 9
|
184 | 177, 183 | mpbird 247 |
. . . . . . . 8
|
185 | 21, 184 | ltned 10173 |
. . . . . . 7
|
186 | 185 | ex 450 |
. . . . . 6
|
187 | | neeq1 2856 |
. . . . . . 7
|
188 | 187 | imbi2d 330 |
. . . . . 6
|
189 | 186, 188 | syl5ibcom 235 |
. . . . 5
|
190 | 14, 189 | sylan2b 492 |
. . . 4
|
191 | 190 | rexlimdva 3031 |
. . 3
|
192 | 12, 191 | mpd 15 |
. 2
|
193 | 192 | necon2bd 2810 |
1
|