Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-prcpal Structured version   Visualization version   GIF version

Definition df-bj-prcpal 32105
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
StepHypRef Expression
1 cprcpal 32104 . 2 class prcpal
2 vx . . 3 setvar 𝑥
3 cr 9787 . . 3 class
42cv 1473 . . . . 5 class 𝑥
5 c2 10913 . . . . . 6 class 2
6 cpi 14578 . . . . . 6 class π
7 cmul 9793 . . . . . 6 class ·
85, 6, 7co 6523 . . . . 5 class (2 · π)
9 cmo 12481 . . . . 5 class mod
104, 8, 9co 6523 . . . 4 class (𝑥 mod (2 · π))
11 cle 9927 . . . . . 6 class
1210, 6, 11wbr 4573 . . . . 5 wff (𝑥 mod (2 · π)) ≤ π
13 cc0 9788 . . . . 5 class 0
1412, 13, 8cif 4031 . . . 4 class if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))
15 cmin 10113 . . . 4 class
1610, 14, 15co 6523 . . 3 class ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π)))
172, 3, 16cmpt 4633 . 2 class (𝑥 ∈ ℝ ↦ ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))))
181, 17wceq 1474 1 wff prcpal = (𝑥 ∈ ℝ ↦ ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator