Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | erdsze.n | |
|
erdsze.f | |
||
erdszelem.k | |
||
erdszelem.o | |
||
Assertion | erdszelem5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | erdsze.n | |
|
2 | erdsze.f | |
|
3 | erdszelem.k | |
|
4 | erdszelem.o | |
|
5 | 1 2 3 | erdszelem3 | |
6 | 5 | adantl | |
7 | snex | |
|
8 | hashf | |
|
9 | 8 | fdmi | |
10 | 7 9 | eleqtrri | |
11 | 1 2 3 4 | erdszelem4 | |
12 | inelcm | |
|
13 | 10 11 12 | sylancr | |
14 | imadisj | |
|
15 | 14 | necon3bii | |
16 | 13 15 | sylibr | |
17 | eqid | |
|
18 | 17 | erdszelem2 | |
19 | 18 | simpli | |
20 | 18 | simpri | |
21 | nnssre | |
|
22 | 20 21 | sstri | |
23 | ltso | |
|
24 | fisupcl | |
|
25 | 23 24 | mpan | |
26 | 19 22 25 | mp3an13 | |
27 | 16 26 | syl | |
28 | 6 27 | eqeltrd | |