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

Theorem modval 11998
Description: The value of the modulo operation. The modulo congruence notation of number theory, J== ( modulo N), can be expressed in our notation as . 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

Proof of Theorem modval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6303 . . . . 5
21fveq2d 5875 . . . 4
32oveq2d 6312 . . 3
4 oveq12 6305 . . 3
53, 4mpdan 668 . 2
6 oveq2 6304 . . . . 5
76fveq2d 5875 . . . 4
8 oveq12 6305 . . . 4
97, 8mpdan 668 . . 3
109oveq2d 6312 . 2
11 df-mod 11997 . 2
12 ovex 6324 . 2
135, 10, 11, 12ovmpt2 6438 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  `cfv 5593  (class class class)co 6296   cr 9512   cmul 9518   cmin 9828   cdiv 10231   crp 11249   cfl 11927   cmo 11996
This theorem is referenced by:  modvalr  11999  modcl  12000  mod0  12003  modge0  12005  modlt  12006  moddiffl  12007  modfrac  12009  modmulnn  12013  zmodcl  12015  modid  12020  modcyc  12031  modadd1  12033  modmul1  12040  moddi  12054  modsubdir  12055  modirr  12057  iexpcyc  12272  digit2  12299  dvdsmod  14043  divalgmod  14064  modgcd  14174  bezoutlem3  14178  prmdiv  14315  odzdvds  14322  fldivp1  14416  odmodnn0  16564  odmod  16570  gexdvds  16604  zringlpirlem3  18511  zlpirlem3  18516  sineq0  22914  efif1olem2  22930  lgseisenlem4  23627  dchrisumlem1  23674  ostth2lem2  23819  gxmodid  25281  ltmod  31644  fourierswlem  32013  sineq0ALT  33737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-mod 11997
  Copyright terms: Public domain W3C validator