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 ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpi	⊢ π
1		crp	⊢ ℝ+
2		csin	⊢ sin
3	2	ccnv	⊢ ◡ sin
4		cc0	⊢ 0
5	4	csn	⊢ { 0 }
6	3 5	cima	⊢ ( ◡ sin “ { 0 } )
7	1 6	cin	⊢ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) )
8		cr	⊢ ℝ
9		clt	⊢ <
10	7 8 9	cinf	⊢ inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < )
11	0 10	wceq	⊢ π = inf ( ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) , ℝ , < )