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

Metamath Proof Explorer

Definition df-pi

Description: Define the constant pi, _pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of _pi in Gleason p. 311. (Contributed by Paul Chapman, 23-Jan-2008) (Revised by AV, 14-Sep-2020)

		Ref	Expression
	Assertion	df-pi	$⊢ π = inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpi	$class π$
1		crp	$class ℝ^{+}$
2		csin	$class \sin$
3	2	ccnv	$class \sin^{-1}$
4		cc0	$class 0$
5	4	csn	$class \{0\}$
6	3 5	cima	$class \sin^{-1} [\{0\}]$
7	1 6	cin	$class (ℝ^{+} \cap \sin^{-1} [\{0\}])$
8		cr	$class ℝ$
9		clt	$class <$
10	7 8 9	cinf	$class inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <)$
11	0 10	wceq	$wff π = inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <)$