Metamath Proof Explorer


Theorem xnn0xr

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

Ref Expression
Assertion xnn0xr A0*A*

Proof

Step Hyp Ref Expression
1 elxnn0 A0*A0A=+∞
2 nn0re A0A
3 2 rexrd A0A*
4 pnfxr +∞*
5 eleq1 A=+∞A*+∞*
6 4 5 mpbiri A=+∞A*
7 3 6 jaoi A0A=+∞A*
8 1 7 sylbi A0*A*