Theorem pige0

Description: _pi is nonnegative. (Contributed by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	pige0	⊢ 0 ≤ π

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		pire	⊢ π ∈ ℝ
3		pipos	⊢ 0 < π
4	1 2 3	ltleii	⊢ 0 ≤ π