Metamath Proof Explorer


Theorem elxrge02

Description: Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016)

Ref Expression
Assertion elxrge02 A 0 +∞ A = 0 A + A = +∞

Proof

Step Hyp Ref Expression
1 0xr 0 *
2 pnfxr +∞ *
3 0lepnf 0 +∞
4 eliccioo 0 * +∞ * 0 +∞ A 0 +∞ A = 0 A 0 +∞ A = +∞
5 1 2 3 4 mp3an A 0 +∞ A = 0 A 0 +∞ A = +∞
6 biid A = 0 A = 0
7 ioorp 0 +∞ = +
8 7 eleq2i A 0 +∞ A +
9 biid A = +∞ A = +∞
10 6 8 9 3orbi123i A = 0 A 0 +∞ A = +∞ A = 0 A + A = +∞
11 5 10 bitri A 0 +∞ A = 0 A + A = +∞