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 = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cmo | |- mod |
|
| 1 | vx | |- x |
|
| 2 | cr | |- RR |
|
| 3 | vy | |- y |
|
| 4 | crp | |- RR+ |
|
| 5 | 1 | cv | |- x |
| 6 | cmin | |- - |
|
| 7 | 3 | cv | |- y |
| 8 | cmul | |- x. |
|
| 9 | cfl | |- |_ |
|
| 10 | cdiv | |- / |
|
| 11 | 5 7 10 | co | |- ( x / y ) |
| 12 | 11 9 | cfv | |- ( |_ ` ( x / y ) ) |
| 13 | 7 12 8 | co | |- ( y x. ( |_ ` ( x / y ) ) ) |
| 14 | 5 13 6 | co | |- ( x - ( y x. ( |_ ` ( x / y ) ) ) ) |
| 15 | 1 3 2 4 14 | cmpo | |- ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) ) |
| 16 | 0 15 | wceq | |- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) ) |