Metamath Proof Explorer


Theorem xnn0xrge0

Description: An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion xnn0xrge0 A0*A0+∞

Proof

Step Hyp Ref Expression
1 elxnn0 A0*A0A=+∞
2 nn0re A0A
3 2 rexrd A0A*
4 nn0ge0 A00A
5 elxrge0 A0+∞A*0A
6 3 4 5 sylanbrc A0A0+∞
7 0xr 0*
8 pnfxr +∞*
9 0lepnf 0+∞
10 ubicc2 0*+∞*0+∞+∞0+∞
11 7 8 9 10 mp3an +∞0+∞
12 eleq1 A=+∞A0+∞+∞0+∞
13 11 12 mpbiri A=+∞A0+∞
14 6 13 jaoi A0A=+∞A0+∞
15 1 14 sylbi A0*A0+∞