Theorem sgnpnf

Description: The signum of +oo is 1. (Contributed by David A. Wheeler, 26-Jun-2016)

	Ref	Expression
Assertion	sgnpnf	$$⊢\mathrm{sgn}\left(\mathrm{+\infty }\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
2		0ltpnf	$$⊢0<\mathrm{+\infty }$$
3		sgnp	$$⊢\left(\mathrm{+\infty }\in {ℝ}^{*}\wedge 0<\mathrm{+\infty }\right)\to \mathrm{sgn}\left(\mathrm{+\infty }\right)=1$$
4	1 2 3	mp2an	$$⊢\mathrm{sgn}\left(\mathrm{+\infty }\right)=1$$