Description: Lemma for hasheuni . (Contributed by Thierry Arnoux, 19-Nov-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | hashf2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hashf | |
|
2 | nn0z | |
|
3 | zre | |
|
4 | rexr | |
|
5 | 2 3 4 | 3syl | |
6 | nn0ge0 | |
|
7 | elxrge0 | |
|
8 | 5 6 7 | sylanbrc | |
9 | 8 | ssriv | |
10 | 0xr | |
|
11 | pnfxr | |
|
12 | 0lepnf | |
|
13 | ubicc2 | |
|
14 | 10 11 12 13 | mp3an | |
15 | snssi | |
|
16 | 14 15 | ax-mp | |
17 | 9 16 | unssi | |
18 | fss | |
|
19 | 1 17 18 | mp2an | |