MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  modval Structured version   Unicode version

Theorem modval 11980
Description: The value of the modulo operation. The modulo congruence notation of number theory,  J  ==  K ( modulo  N ), can be expressed in our notation as  ( J  mod  N )  =  ( K  mod  N ). Definition 1 in Knuth, The Art of Computer Programming, Vol. I (1972), p. 38. Knuth uses "mod" for the operation and "modulo" for the congruence. Unlike Knuth, we restrict the second argument to positive reals to simplify certain theorems. (This also gives us future flexibility to extend it to any one of several different conventions for a zero or negative second argument, should there be an advantage in doing so.) (Contributed by NM, 10-Nov-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
Assertion
Ref Expression
modval  |-  ( ( A  e.  RR  /\  B  e.  RR+ )  -> 
( A  mod  B
)  =  ( A  -  ( B  x.  ( |_ `  ( A  /  B ) ) ) ) )

Proof of Theorem modval
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6288 . . . . 5  |-  ( x  =  A  ->  (
x  /  y )  =  ( A  / 
y ) )
21fveq2d 5860 . . . 4  |-  ( x  =  A  ->  ( |_ `  ( x  / 
y ) )  =  ( |_ `  ( A  /  y ) ) )
32oveq2d 6297 . . 3  |-  ( x  =  A  ->  (
y  x.  ( |_
`  ( x  / 
y ) ) )  =  ( y  x.  ( |_ `  ( A  /  y ) ) ) )
4 oveq12 6290 . . 3  |-  ( ( x  =  A  /\  ( y  x.  ( |_ `  ( x  / 
y ) ) )  =  ( y  x.  ( |_ `  ( A  /  y ) ) ) )  ->  (
x  -  ( y  x.  ( |_ `  ( x  /  y
) ) ) )  =  ( A  -  ( y  x.  ( |_ `  ( A  / 
y ) ) ) ) )
53, 4mpdan 668 . 2  |-  ( x  =  A  ->  (
x  -  ( y  x.  ( |_ `  ( x  /  y
) ) ) )  =  ( A  -  ( y  x.  ( |_ `  ( A  / 
y ) ) ) ) )
6 oveq2 6289 . . . . 5  |-  ( y  =  B  ->  ( A  /  y )  =  ( A  /  B
) )
76fveq2d 5860 . . . 4  |-  ( y  =  B  ->  ( |_ `  ( A  / 
y ) )  =  ( |_ `  ( A  /  B ) ) )
8 oveq12 6290 . . . 4  |-  ( ( y  =  B  /\  ( |_ `  ( A  /  y ) )  =  ( |_ `  ( A  /  B
) ) )  -> 
( y  x.  ( |_ `  ( A  / 
y ) ) )  =  ( B  x.  ( |_ `  ( A  /  B ) ) ) )
97, 8mpdan 668 . . 3  |-  ( y  =  B  ->  (
y  x.  ( |_
`  ( A  / 
y ) ) )  =  ( B  x.  ( |_ `  ( A  /  B ) ) ) )
109oveq2d 6297 . 2  |-  ( y  =  B  ->  ( A  -  ( y  x.  ( |_ `  ( A  /  y ) ) ) )  =  ( A  -  ( B  x.  ( |_ `  ( A  /  B
) ) ) ) )
11 df-mod 11979 . 2  |-  mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
12 ovex 6309 . 2  |-  ( A  -  ( B  x.  ( |_ `  ( A  /  B ) ) ) )  e.  _V
135, 10, 11, 12ovmpt2 6423 1  |-  ( ( A  e.  RR  /\  B  e.  RR+ )  -> 
( A  mod  B
)  =  ( A  -  ( B  x.  ( |_ `  ( A  /  B ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383    e. wcel 1804   ` cfv 5578  (class class class)co 6281   RRcr 9494    x. cmul 9500    - cmin 9810    / cdiv 10213   RR+crp 11231   |_cfl 11909    mod cmo 11978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-iota 5541  df-fun 5580  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-mod 11979
This theorem is referenced by:  modvalr  11981  modcl  11982  mod0  11985  modge0  11987  modlt  11988  moddiffl  11989  modfrac  11991  modmulnn  11995  zmodcl  11997  modid  12002  modcyc  12013  modadd1  12015  modmul1  12022  moddi  12036  modsubdir  12037  modirr  12039  iexpcyc  12254  digit2  12281  dvdsmod  14025  divalgmod  14046  modgcd  14156  bezoutlem3  14160  prmdiv  14297  odzdvds  14304  fldivp1  14398  odmodnn0  16543  odmod  16549  gexdvds  16583  zringlpirlem3  18489  zlpirlem3  18494  sineq0  22892  efif1olem2  22908  lgseisenlem4  23605  dchrisumlem1  23652  ostth2lem2  23797  gxmodid  25259  ltmod  31598  fourierswlem  31967  sineq0ALT  33605
  Copyright terms: Public domain W3C validator