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

Metamath Proof Explorer

Theorem neghalfpirx

Description: -u _pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018)

		Ref	Expression
	Assertion	neghalfpirx	$⊢ - \frac{π}{2} \in ℝ^{*}$

Step	Hyp	Ref	Expression
1		neghalfpire	$⊢ - \frac{π}{2} \in ℝ$
2	1	rexri	$⊢ - \frac{π}{2} \in ℝ^{*}$