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

Theorem modval 11954
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 6282 . . . . 5  |-  ( x  =  A  ->  (
x  /  y )  =  ( A  / 
y ) )
21fveq2d 5861 . . . 4  |-  ( x  =  A  ->  ( |_ `  ( x  / 
y ) )  =  ( |_ `  ( A  /  y ) ) )
32oveq2d 6291 . . 3  |-  ( x  =  A  ->  (
y  x.  ( |_
`  ( x  / 
y ) ) )  =  ( y  x.  ( |_ `  ( A  /  y ) ) ) )
4 oveq12 6284 . . 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 6283 . . . . 5  |-  ( y  =  B  ->  ( A  /  y )  =  ( A  /  B
) )
76fveq2d 5861 . . . 4  |-  ( y  =  B  ->  ( |_ `  ( A  / 
y ) )  =  ( |_ `  ( A  /  B ) ) )
8 oveq12 6284 . . . 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 6291 . 2  |-  ( y  =  B  ->  ( A  -  ( y  x.  ( |_ `  ( A  /  y ) ) ) )  =  ( A  -  ( B  x.  ( |_ `  ( A  /  B
) ) ) ) )
11 df-mod 11953 . 2  |-  mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
12 ovex 6300 . 2  |-  ( A  -  ( B  x.  ( |_ `  ( A  /  B ) ) ) )  e.  _V
135, 10, 11, 12ovmpt2 6413 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 1374    e. wcel 1762   ` cfv 5579  (class class class)co 6275   RRcr 9480    x. cmul 9486    - cmin 9794    / cdiv 10195   RR+crp 11209   |_cfl 11884    mod cmo 11952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-iota 5542  df-fun 5581  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-mod 11953
This theorem is referenced by:  modvalr  11955  modcl  11956  mod0  11959  modge0  11961  modlt  11962  moddiffl  11963  modfrac  11965  modmulnn  11969  zmodcl  11971  modid  11976  modcyc  11987  modadd1  11989  modmul1  11996  moddi  12010  modsubdir  12011  modirr  12013  iexpcyc  12227  digit2  12254  dvdsmod  13891  divalgmod  13912  modgcd  14022  bezoutlem3  14026  prmdiv  14163  odzdvds  14170  fldivp1  14264  odmodnn0  16353  odmod  16359  gexdvds  16393  zringlpirlem3  18271  zlpirlem3  18276  sineq0  22640  efif1olem2  22656  lgseisenlem4  23348  dchrisumlem1  23395  ostth2lem2  23540  gxmodid  24943  ltmod  31135  fourierswlem  31486  sineq0ALT  32692
  Copyright terms: Public domain W3C validator