Metamath Proof Explorer


Theorem elxrge0

Description: Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion elxrge0 A0+∞A*0A

Proof

Step Hyp Ref Expression
1 df-3an A*0AA+∞A*0AA+∞
2 0xr 0*
3 pnfxr +∞*
4 elicc1 0*+∞*A0+∞A*0AA+∞
5 2 3 4 mp2an A0+∞A*0AA+∞
6 pnfge A*A+∞
7 6 adantr A*0AA+∞
8 7 pm4.71i A*0AA*0AA+∞
9 1 5 8 3bitr4i A0+∞A*0A