Definition df-bj-prcpal 33129

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 33128	. 2 class prcpal
2		vx	. . 3 setvar 𝑥
3		cr 9935	. . 3 class ℝ
4	2	cv 1482	. . . . 5 class 𝑥
5		c2 11070	. . . . . 6 class 2
6		cpi 14797	. . . . . 6 class π
7		cmul 9941	. . . . . 6 class ·
8	5, 6, 7	co 6650	. . . . 5 class (2 · π)
9		cmo 12668	. . . . 5 class mod
10	4, 8, 9	co 6650	. . . 4 class (𝑥 mod (2 · π))
11		cle 10075	. . . . . 6 class ≤
12	10, 6, 11	wbr 4653	. . . . 5 wff (𝑥 mod (2 · π)) ≤ π
13		cc0 9936	. . . . 5 class 0
14	12, 13, 8	cif 4086	. . . 4 class if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))
15		cmin 10266	. . . 4 class −
16	10, 14, 15	co 6650	. . 3 class ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π)))
17	2, 3, 16	cmpt 4729	. 2 class (𝑥 ∈ ℝ ↦ ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))))
18	1, 17	wceq 1483	1 wff prcpal = (𝑥 ∈ ℝ ↦ ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))))

This definition is referenced by: (None)