Definition df-pi 7302

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 of less-than, "`' <", to turn supremum into infimum; currently we don't have infimum defined separately.)

Assertion

Ref	Expression
df-pi	|- pi = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )

Detailed syntax breakdown of Definition df-pi

Step	Hyp	Ref	Expression
1		cpi 7297	. 2 class pi
2		cc0 5246	. . . . . 6 class 0
3		vx	. . . . . . 7 set x
4	3	cv 957	. . . . . 6 class x
5		clt 5498	. . . . . 6 class <
6	2, 4, 5	wbr 2624	. . . . 5 wff 0 < x
7		csin 7295	. . . . . . 7 class sin
8	4, 7	cfv 3188	. . . . . 6 class (sin` x)
9	8, 2	wceq 958	. . . . 5 wff (sin` x) = 0
10	6, 9	wa 223	. . . 4 wff (0 < x /\ (sin` x) = 0)
11		cr 5245	. . . 4 class RR
12	10, 3, 11	crab 1651	. . 3 class {x e. RR | (0 < x /\ (sin` x) = 0)}
13	5	ccnv 3175	. . 3 class `' <
14	12, 11, 13	csup 4582	. 2 class sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )
15	1, 14	wceq 958	1 wff pi = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )

This definition is referenced by:  pilem3 8668

Copyright terms: Public domain