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	$$⊢\mathrm{\pi }=sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)$$

Detailed syntax breakdown

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