Metamath Proof Explorer


Theorem xrnemnf

Description: An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xrnemnf A * A −∞ A A = +∞

Proof

Step Hyp Ref Expression
1 pm5.61 A A = +∞ A = −∞ ¬ A = −∞ A A = +∞ ¬ A = −∞
2 elxr A * A A = +∞ A = −∞
3 df-3or A A = +∞ A = −∞ A A = +∞ A = −∞
4 2 3 bitri A * A A = +∞ A = −∞
5 df-ne A −∞ ¬ A = −∞
6 4 5 anbi12i A * A −∞ A A = +∞ A = −∞ ¬ A = −∞
7 renemnf A A −∞
8 pnfnemnf +∞ −∞
9 neeq1 A = +∞ A −∞ +∞ −∞
10 8 9 mpbiri A = +∞ A −∞
11 7 10 jaoi A A = +∞ A −∞
12 11 neneqd A A = +∞ ¬ A = −∞
13 12 pm4.71i A A = +∞ A A = +∞ ¬ A = −∞
14 1 6 13 3bitr4i A * A −∞ A A = +∞