Description: Define the modulo (remainder) operation. See modval for its value. For example, ( 5 mod 3 ) = 2 and ( -u 7 mod 2 ) = 1 ( ex-mod ). (Contributed by NM, 10-Nov-2008)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-mod | ⊢ mod = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ+ ↦ ( 𝑥 − ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cmo | ⊢ mod | |
| 1 | vx | ⊢ 𝑥 | |
| 2 | cr | ⊢ ℝ | |
| 3 | vy | ⊢ 𝑦 | |
| 4 | crp | ⊢ ℝ+ | |
| 5 | 1 | cv | ⊢ 𝑥 |
| 6 | cmin | ⊢ − | |
| 7 | 3 | cv | ⊢ 𝑦 |
| 8 | cmul | ⊢ · | |
| 9 | cfl | ⊢ ⌊ | |
| 10 | cdiv | ⊢ / | |
| 11 | 5 7 10 | co | ⊢ ( 𝑥 / 𝑦 ) |
| 12 | 11 9 | cfv | ⊢ ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) |
| 13 | 7 12 8 | co | ⊢ ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) |
| 14 | 5 13 6 | co | ⊢ ( 𝑥 − ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) ) |
| 15 | 1 3 2 4 14 | cmpo | ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ+ ↦ ( 𝑥 − ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) ) ) |
| 16 | 0 15 | wceq | ⊢ mod = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ+ ↦ ( 𝑥 − ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) ) ) |