Definition df-pi 7494

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 7489	. 2 class pi
2		cc0 5379	. . . . . 6 class 0
3		vx	. . . . . . 7 set x
4	3	cv 988	. . . . . 6 class x
5		clt 5631	. . . . . 6 class <
6	2, 4, 5	wbr 2687	. . . . 5 wff 0 < x
7		csin 7487	. . . . . . 7 class sin
8	4, 7	cfv 3260	. . . . . 6 class (sin` x)
9	8, 2	wceq 989	. . . . 5 wff (sin` x) = 0
10	6, 9	wa 221	. . . 4 wff (0 < x /\ (sin` x) = 0)
11		cr 5378	. . . 4 class RR
12	10, 3, 11	crab 1692	. . 3 class {x e. RR | (0 < x /\ (sin` x) = 0)}
13	5	ccnv 3247	. . 3 class `' <
14	12, 11, 13	csup 4707	. 2 class sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )
15	1, 14	wceq 989	1 wff pi = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )

This definition is referenced by:  pilem3 8919

Copyright terms: Public domain