![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > modval | Structured version Visualization version GIF version |
Description: The value of the modulo operation. The modulo congruence notation of number theory, ๐ฝโก๐พ (modulo ๐), can be expressed in our notation as (๐ฝ mod ๐) = (๐พ mod ๐). 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.) |
Ref | Expression |
---|---|
modval | โข ((๐ด โ โ โง ๐ต โ โ+) โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvoveq1 7434 | . . . 4 โข (๐ฅ = ๐ด โ (โโ(๐ฅ / ๐ฆ)) = (โโ(๐ด / ๐ฆ))) | |
2 | 1 | oveq2d 7427 | . . 3 โข (๐ฅ = ๐ด โ (๐ฆ ยท (โโ(๐ฅ / ๐ฆ))) = (๐ฆ ยท (โโ(๐ด / ๐ฆ)))) |
3 | oveq12 7420 | . . 3 โข ((๐ฅ = ๐ด โง (๐ฆ ยท (โโ(๐ฅ / ๐ฆ))) = (๐ฆ ยท (โโ(๐ด / ๐ฆ)))) โ (๐ฅ โ (๐ฆ ยท (โโ(๐ฅ / ๐ฆ)))) = (๐ด โ (๐ฆ ยท (โโ(๐ด / ๐ฆ))))) | |
4 | 2, 3 | mpdan 683 | . 2 โข (๐ฅ = ๐ด โ (๐ฅ โ (๐ฆ ยท (โโ(๐ฅ / ๐ฆ)))) = (๐ด โ (๐ฆ ยท (โโ(๐ด / ๐ฆ))))) |
5 | oveq2 7419 | . . . . 5 โข (๐ฆ = ๐ต โ (๐ด / ๐ฆ) = (๐ด / ๐ต)) | |
6 | 5 | fveq2d 6894 | . . . 4 โข (๐ฆ = ๐ต โ (โโ(๐ด / ๐ฆ)) = (โโ(๐ด / ๐ต))) |
7 | oveq12 7420 | . . . 4 โข ((๐ฆ = ๐ต โง (โโ(๐ด / ๐ฆ)) = (โโ(๐ด / ๐ต))) โ (๐ฆ ยท (โโ(๐ด / ๐ฆ))) = (๐ต ยท (โโ(๐ด / ๐ต)))) | |
8 | 6, 7 | mpdan 683 | . . 3 โข (๐ฆ = ๐ต โ (๐ฆ ยท (โโ(๐ด / ๐ฆ))) = (๐ต ยท (โโ(๐ด / ๐ต)))) |
9 | 8 | oveq2d 7427 | . 2 โข (๐ฆ = ๐ต โ (๐ด โ (๐ฆ ยท (โโ(๐ด / ๐ฆ)))) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
10 | df-mod 13839 | . 2 โข mod = (๐ฅ โ โ, ๐ฆ โ โ+ โฆ (๐ฅ โ (๐ฆ ยท (โโ(๐ฅ / ๐ฆ))))) | |
11 | ovex 7444 | . 2 โข (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต)))) โ V | |
12 | 4, 9, 10, 11 | ovmpo 7570 | 1 โข ((๐ด โ โ โง ๐ต โ โ+) โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โง wa 394 = wceq 1539 โ wcel 2104 โcfv 6542 (class class class)co 7411 โcr 11111 ยท cmul 11117 โ cmin 11448 / cdiv 11875 โ+crp 12978 โcfl 13759 mod cmo 13838 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-iota 6494 df-fun 6544 df-fv 6550 df-ov 7414 df-oprab 7415 df-mpo 7416 df-mod 13839 |
This theorem is referenced by: modvalr 13841 modcl 13842 mod0 13845 modge0 13848 modlt 13849 moddiffl 13851 modfrac 13853 modmulnn 13858 zmodcl 13860 modid 13865 modcyc 13875 modadd1 13877 modmul1 13893 moddi 13908 modsubdir 13909 modirr 13911 iexpcyc 14175 digit2 14203 dvdsmod 16276 divalgmod 16353 modgcd 16478 bezoutlem3 16487 prmdiv 16722 odzdvds 16732 fldivp1 16834 mulgmodid 19029 odmodnn0 19449 odmod 19455 gexdvds 19493 zringlpirlem3 21235 sineq0 26269 efif1olem2 26288 lgseisenlem4 27117 dchrisumlem1 27228 ostth2lem2 27373 sineq0ALT 44000 ltmod 44652 fourierswlem 45244 |
Copyright terms: Public domain | W3C validator |