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* )