![]() |
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 6899 | . . . 4 ⊢ (𝑥 = 𝐴 → (⌊‘(𝑥 / 𝑦)) = (⌊‘(𝐴 / 𝑦))) | |
2 | 1 | oveq2d 6892 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑦 · (⌊‘(𝑥 / 𝑦))) = (𝑦 · (⌊‘(𝐴 / 𝑦)))) |
3 | oveq12 6885 | . . 3 ⊢ ((𝑥 = 𝐴 ∧ (𝑦 · (⌊‘(𝑥 / 𝑦))) = (𝑦 · (⌊‘(𝐴 / 𝑦)))) → (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))) = (𝐴 − (𝑦 · (⌊‘(𝐴 / 𝑦))))) | |
4 | 2, 3 | mpdan 679 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))) = (𝐴 − (𝑦 · (⌊‘(𝐴 / 𝑦))))) |
5 | oveq2 6884 | . . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 / 𝑦) = (𝐴 / 𝐵)) | |
6 | 5 | fveq2d 6413 | . . . 4 ⊢ (𝑦 = 𝐵 → (⌊‘(𝐴 / 𝑦)) = (⌊‘(𝐴 / 𝐵))) |
7 | oveq12 6885 | . . . 4 ⊢ ((𝑦 = 𝐵 ∧ (⌊‘(𝐴 / 𝑦)) = (⌊‘(𝐴 / 𝐵))) → (𝑦 · (⌊‘(𝐴 / 𝑦))) = (𝐵 · (⌊‘(𝐴 / 𝐵)))) | |
8 | 6, 7 | mpdan 679 | . . 3 ⊢ (𝑦 = 𝐵 → (𝑦 · (⌊‘(𝐴 / 𝑦))) = (𝐵 · (⌊‘(𝐴 / 𝐵)))) |
9 | 8 | oveq2d 6892 | . 2 ⊢ (𝑦 = 𝐵 → (𝐴 − (𝑦 · (⌊‘(𝐴 / 𝑦)))) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) |
10 | df-mod 12920 | . 2 ⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))) | |
11 | ovex 6908 | . 2 ⊢ (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵)))) ∈ V | |
12 | 4, 9, 10, 11 | ovmpt2 7028 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ‘cfv 6099 (class class class)co 6876 ℝcr 10221 · cmul 10227 − cmin 10554 / cdiv 10974 ℝ+crp 12070 ⌊cfl 12842 mod cmo 12919 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-sep 4973 ax-nul 4981 ax-pr 5095 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ral 3092 df-rex 3093 df-rab 3096 df-v 3385 df-sbc 3632 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-br 4842 df-opab 4904 df-id 5218 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-iota 6062 df-fun 6101 df-fv 6107 df-ov 6879 df-oprab 6880 df-mpt2 6881 df-mod 12920 |
This theorem is referenced by: modvalr 12922 modcl 12923 mod0 12926 modge0 12929 modlt 12930 moddiffl 12932 modfrac 12934 modmulnn 12939 zmodcl 12941 modid 12946 modcyc 12956 modadd1 12958 modmul1 12974 moddi 12989 modsubdir 12990 modirr 12992 iexpcyc 13219 digit2 13247 dvdsmod 15386 divalgmod 15462 modgcd 15585 bezoutlem3 15590 prmdiv 15820 odzdvds 15830 fldivp1 15931 mulgmodid 17891 odmodnn0 18269 odmod 18275 gexdvds 18309 zringlpirlem3 20153 sineq0 24612 efif1olem2 24628 lgseisenlem4 25452 dchrisumlem1 25527 ostth2lem2 25672 sineq0ALT 39921 ltmod 40602 fourierswlem 41178 |
Copyright terms: Public domain | W3C validator |