This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0mnfxrd

Description: Nonnegative integers or minus infinity are extended real numbers. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypothesis nn0mnfxrd.1 
|- ( ph -> A e. ( NN0 u. { -oo } ) )
Assertion nn0mnfxrd 
|- ( ph -> A e. RR* )

Proof

Step Hyp Ref Expression
1 nn0mnfxrd.1 
 |-  ( ph -> A e. ( NN0 u. { -oo } ) )
2 nn0re 
 |-  ( A e. NN0 -> A e. RR )
3 2 rexrd 
 |-  ( A e. NN0 -> A e. RR* )
4 3 adantl 
 |-  ( ( ph /\ A e. NN0 ) -> A e. RR* )
5 mnfxr 
 |-  -oo e. RR*
6 eleq1 
 |-  ( A = -oo -> ( A e. RR* <-> -oo e. RR* ) )
7 5 6 mpbiri 
 |-  ( A = -oo -> A e. RR* )
8 7 adantl 
 |-  ( ( ph /\ A = -oo ) -> A e. RR* )
9 elunsn 
 |-  ( A e. ( NN0 u. { -oo } ) -> ( A e. ( NN0 u. { -oo } ) <-> ( A e. NN0 \/ A = -oo ) ) )
10 9 ibi 
 |-  ( A e. ( NN0 u. { -oo } ) -> ( A e. NN0 \/ A = -oo ) )
11 1 10 syl 
 |-  ( ph -> ( A e. NN0 \/ A = -oo ) )
12 4 8 11 mpjaodan 
 |-  ( ph -> A e. RR* )