Metamath Proof Explorer

Description: Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021)

Ref Expression
Assertion modmuladd ${⊢}\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}={B}↔\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+{B}\right)$

Proof

Step Hyp Ref Expression
1 zre ${⊢}{A}\in ℤ\to {A}\in ℝ$
2 1 adantr ${⊢}\left({A}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to {A}\in ℝ$
3 rpre ${⊢}{M}\in {ℝ}^{+}\to {M}\in ℝ$
4 3 adantl ${⊢}\left({A}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to {M}\in ℝ$
5 rpne0 ${⊢}{M}\in {ℝ}^{+}\to {M}\ne 0$
6 5 adantl ${⊢}\left({A}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to {M}\ne 0$
7 2 4 6 redivcld ${⊢}\left({A}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to \frac{{A}}{{M}}\in ℝ$
8 7 flcld ${⊢}\left({A}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{M}}⌋\in ℤ$
9 8 3adant2 ${⊢}\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{M}}⌋\in ℤ$
10 oveq1 ${⊢}{k}=⌊\frac{{A}}{{M}}⌋\to {k}\cdot {M}=⌊\frac{{A}}{{M}}⌋\cdot {M}$
11 10 oveq1d ${⊢}{k}=⌊\frac{{A}}{{M}}⌋\to {k}\cdot {M}+\left({A}\mathrm{mod}{M}\right)=⌊\frac{{A}}{{M}}⌋\cdot {M}+\left({A}\mathrm{mod}{M}\right)$
12 11 eqeq2d ${⊢}{k}=⌊\frac{{A}}{{M}}⌋\to \left({A}={k}\cdot {M}+\left({A}\mathrm{mod}{M}\right)↔{A}=⌊\frac{{A}}{{M}}⌋\cdot {M}+\left({A}\mathrm{mod}{M}\right)\right)$
13 12 adantl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\wedge {k}=⌊\frac{{A}}{{M}}⌋\right)\to \left({A}={k}\cdot {M}+\left({A}\mathrm{mod}{M}\right)↔{A}=⌊\frac{{A}}{{M}}⌋\cdot {M}+\left({A}\mathrm{mod}{M}\right)\right)$
14 1 anim1i ${⊢}\left({A}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)$
15 14 3adant2 ${⊢}\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)$
16 flpmodeq ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{M}}⌋\cdot {M}+\left({A}\mathrm{mod}{M}\right)={A}$
17 15 16 syl ${⊢}\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{M}}⌋\cdot {M}+\left({A}\mathrm{mod}{M}\right)={A}$
18 17 eqcomd ${⊢}\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\to {A}=⌊\frac{{A}}{{M}}⌋\cdot {M}+\left({A}\mathrm{mod}{M}\right)$
19 9 13 18 rspcedvd ${⊢}\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\to \exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+\left({A}\mathrm{mod}{M}\right)$
20 oveq2 ${⊢}{B}={A}\mathrm{mod}{M}\to {k}\cdot {M}+{B}={k}\cdot {M}+\left({A}\mathrm{mod}{M}\right)$
21 20 eqeq2d ${⊢}{B}={A}\mathrm{mod}{M}\to \left({A}={k}\cdot {M}+{B}↔{A}={k}\cdot {M}+\left({A}\mathrm{mod}{M}\right)\right)$
22 21 eqcoms ${⊢}{A}\mathrm{mod}{M}={B}\to \left({A}={k}\cdot {M}+{B}↔{A}={k}\cdot {M}+\left({A}\mathrm{mod}{M}\right)\right)$
23 22 rexbidv ${⊢}{A}\mathrm{mod}{M}={B}\to \left(\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+{B}↔\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+\left({A}\mathrm{mod}{M}\right)\right)$
24 19 23 syl5ibrcom ${⊢}\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}={B}\to \exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+{B}\right)$
25 oveq1 ${⊢}{A}={k}\cdot {M}+{B}\to {A}\mathrm{mod}{M}=\left({k}\cdot {M}+{B}\right)\mathrm{mod}{M}$
26 simpr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\wedge {k}\in ℤ\right)\to {k}\in ℤ$
27 simpl3 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\wedge {k}\in ℤ\right)\to {M}\in {ℝ}^{+}$
28 simpl2 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\wedge {k}\in ℤ\right)\to {B}\in \left[0,{M}\right)$
29 muladdmodid ${⊢}\left({k}\in ℤ\wedge {M}\in {ℝ}^{+}\wedge {B}\in \left[0,{M}\right)\right)\to \left({k}\cdot {M}+{B}\right)\mathrm{mod}{M}={B}$
30 26 27 28 29 syl3anc ${⊢}\left(\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\wedge {k}\in ℤ\right)\to \left({k}\cdot {M}+{B}\right)\mathrm{mod}{M}={B}$
31 25 30 sylan9eqr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\wedge {k}\in ℤ\right)\wedge {A}={k}\cdot {M}+{B}\right)\to {A}\mathrm{mod}{M}={B}$
32 31 rexlimdva2 ${⊢}\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\to \left(\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+{B}\to {A}\mathrm{mod}{M}={B}\right)$
33 24 32 impbid ${⊢}\left({A}\in ℤ\wedge {B}\in \left[0,{M}\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}={B}↔\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+{B}\right)$