Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
pine0
Next ⟩
ine1
Metamath Proof Explorer
Ascii
Structured
Theorem
pine0
Description:
_pi
is nonzero.
(Contributed by
SN
, 25-Apr-2025)
Ref
Expression
Assertion
pine0
⊢
π ≠ 0
Proof
Step
Hyp
Ref
Expression
1
pire
⊢
π ∈ ℝ
2
pipos
⊢
0 < π
3
1
2
gt0ne0ii
⊢
π ≠ 0