Definition df-bj-prcpal 33129

Description: Define the function prcpal. (Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
df-bj-prcpal	|- prcpal = ( x e. RR |-> ( ( x mod ( 2 x. pi ) ) - if ( ( x mod ( 2 x. pi ) ) <_ pi , 0 , ( 2 x. pi ) ) ) )

Detailed syntax breakdown of Definition df-bj-prcpal

Step	Hyp	Ref	Expression
1		cprcpal 33128	. 2 class prcpal
2		vx	. . 3 setvar x
3		cr 9935	. . 3 class RR
4	2	cv 1482	. . . . 5 class x
5		c2 11070	. . . . . 6 class 2
6		cpi 14797	. . . . . 6 class pi
7		cmul 9941	. . . . . 6 class x.
8	5, 6, 7	co 6650	. . . . 5 class ( 2 x. pi )
9		cmo 12668	. . . . 5 class mod
10	4, 8, 9	co 6650	. . . 4 class ( x mod ( 2 x. pi ) )
11		cle 10075	. . . . . 6 class <_
12	10, 6, 11	wbr 4653	. . . . 5 wff ( x mod ( 2 x. pi ) ) <_ pi
13		cc0 9936	. . . . 5 class 0
14	12, 13, 8	cif 4086	. . . 4 class if ( ( x mod ( 2 x. pi ) ) <_ pi , 0 , ( 2 x. pi ) )
15		cmin 10266	. . . 4 class -
16	10, 14, 15	co 6650	. . 3 class ( ( x mod ( 2 x. pi ) ) - if ( ( x mod ( 2 x. pi ) ) <_ pi , 0 , ( 2 x. pi ) ) )
17	2, 3, 16	cmpt 4729	. 2 class ( x e. RR |-> ( ( x mod ( 2 x. pi ) ) - if ( ( x mod ( 2 x. pi ) ) <_ pi , 0 , ( 2 x. pi ) ) ) )
18	1, 17	wceq 1483	1 wff prcpal = ( x e. RR |-> ( ( x mod ( 2 x. pi ) ) - if ( ( x mod ( 2 x. pi ) ) <_ pi , 0 , ( 2 x. pi ) ) ) )

This definition is referenced by: (None)