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

Theorem modval 11828
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 6208 . . . . 5  |-  ( x  =  A  ->  (
x  /  y )  =  ( A  / 
y ) )
21fveq2d 5804 . . . 4  |-  ( x  =  A  ->  ( |_ `  ( x  / 
y ) )  =  ( |_ `  ( A  /  y ) ) )
32oveq2d 6217 . . 3  |-  ( x  =  A  ->  (
y  x.  ( |_
`  ( x  / 
y ) ) )  =  ( y  x.  ( |_ `  ( A  /  y ) ) ) )
4 oveq12 6210 . . 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 6209 . . . . 5  |-  ( y  =  B  ->  ( A  /  y )  =  ( A  /  B
) )
76fveq2d 5804 . . . 4  |-  ( y  =  B  ->  ( |_ `  ( A  / 
y ) )  =  ( |_ `  ( A  /  B ) ) )
8 oveq12 6210 . . . 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 6217 . 2  |-  ( y  =  B  ->  ( A  -  ( y  x.  ( |_ `  ( A  /  y ) ) ) )  =  ( A  -  ( B  x.  ( |_ `  ( A  /  B
) ) ) ) )
11 df-mod 11827 . 2  |-  mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
12 ovex 6226 . 2  |-  ( A  -  ( B  x.  ( |_ `  ( A  /  B ) ) ) )  e.  _V
135, 10, 11, 12ovmpt2 6337 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 1370    e. wcel 1758   ` cfv 5527  (class class class)co 6201   RRcr 9393    x. cmul 9399    - cmin 9707    / cdiv 10105   RR+crp 11103   |_cfl 11758    mod cmo 11826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pr 4640
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-opab 4460  df-id 4745  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-iota 5490  df-fun 5529  df-fv 5535  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-mod 11827
This theorem is referenced by:  modvalr  11829  modcl  11830  mod0  11833  modge0  11835  modlt  11836  moddiffl  11837  modfrac  11839  modmulnn  11843  zmodcl  11845  modid  11850  modcyc  11861  modadd1  11863  modmul1  11870  moddi  11884  modsubdir  11885  modirr  11887  iexpcyc  12088  digit2  12115  dvdsmod  13709  divalgmod  13729  modgcd  13839  bezoutlem3  13843  prmdiv  13979  odzdvds  13986  fldivp1  14078  odmodnn0  16165  odmod  16171  gexdvds  16205  zringlpirlem3  18031  zlpirlem3  18036  sineq0  22117  efif1olem2  22133  lgseisenlem4  22825  dchrisumlem1  22872  ostth2lem2  23017  gxmodid  23919  sineq0ALT  32006
  Copyright terms: Public domain W3C validator