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

Metamath Proof Explorer

Theorem pige3

Description: _pi is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion pige3 3 ≤ π

Proof

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