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 ( ( ℝ⁺ ∩ ( ^◡ 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 } ) ) , ℝ , < )