Metamath Proof Explorer


Theorem hashf2

Description: Lemma for hasheuni . (Contributed by Thierry Arnoux, 19-Nov-2016)

Ref Expression
Assertion hashf2 .:V0+∞

Proof

Step Hyp Ref Expression
1 hashf .:V0+∞
2 nn0z x0x
3 zre xx
4 rexr xx*
5 2 3 4 3syl x0x*
6 nn0ge0 x00x
7 elxrge0 x0+∞x*0x
8 5 6 7 sylanbrc x0x0+∞
9 8 ssriv 00+∞
10 0xr 0*
11 pnfxr +∞*
12 0lepnf 0+∞
13 ubicc2 0*+∞*0+∞+∞0+∞
14 10 11 12 13 mp3an +∞0+∞
15 snssi +∞0+∞+∞0+∞
16 14 15 ax-mp +∞0+∞
17 9 16 unssi 0+∞0+∞
18 fss .:V0+∞0+∞0+∞.:V0+∞
19 1 17 18 mp2an .:V0+∞