Definition df-pi 13808

Description: Define pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of pi in [Gleason] p. 311. (We use the inverse of less-than, "", to turn supremum into infimum; currently we don't have infimum defined separately.) (Contributed by Paul Chapman, 23-Jan-2008.)

Assertion

Ref	Expression
df-pi

Detailed syntax breakdown of Definition df-pi

Step	Hyp	Ref	Expression
1		cpi 13802	. 2
2		crp 11249	. . . 4
3		csin 13799	. . . . . 6
4	3	ccnv 5003	. . . . 5
5		cc0 9513	. . . . . 6
6	5	csn 4029	. . . . 5
7	4, 6	cima 5007	. . . 4
8	2, 7	cin 3474	. . 3
9		cr 9512	. . 3
10		clt 9649	. . . 4
11	10	ccnv 5003	. . 3
12	8, 9, 11	csup 7920	. 2
13	1, 12	wceq 1395	1

This definition is referenced by:  pilem2  22847  pilem3  22848