Definition df-bj-prcpal 32306

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

Assertion

Ref	Expression
df-bj-prcpal	⊢ prcpal = (𝑥 ∈ ℝ ↦ ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))))

Detailed syntax breakdown of Definition df-bj-prcpal

Step	Hyp	Ref	Expression
1		cprcpal 32305	. 2 class prcpal
2		vx	. . 3 setvar 𝑥
3		cr 9814	. . 3 class ℝ
4	2	cv 1474	. . . . 5 class 𝑥
5		c2 10947	. . . . . 6 class 2
6		cpi 14636	. . . . . 6 class π
7		cmul 9820	. . . . . 6 class ·
8	5, 6, 7	co 6549	. . . . 5 class (2 · π)
9		cmo 12530	. . . . 5 class mod
10	4, 8, 9	co 6549	. . . 4 class (𝑥 mod (2 · π))
11		cle 9954	. . . . . 6 class ≤
12	10, 6, 11	wbr 4583	. . . . 5 wff (𝑥 mod (2 · π)) ≤ π
13		cc0 9815	. . . . 5 class 0
14	12, 13, 8	cif 4036	. . . 4 class if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))
15		cmin 10145	. . . 4 class −
16	10, 14, 15	co 6549	. . 3 class ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π)))
17	2, 3, 16	cmpt 4643	. 2 class (𝑥 ∈ ℝ ↦ ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))))
18	1, 17	wceq 1475	1 wff prcpal = (𝑥 ∈ ℝ ↦ ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))))

This definition is referenced by: (None)