# Metamath Proof Explorer

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

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

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to {i}\in ℤ$
2 1 adantr ${⊢}\left(\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\wedge {A}={i}\cdot {M}+{B}\right)\to {i}\in ℤ$
3 nn0cn ${⊢}{A}\in {ℕ}_{0}\to {A}\in ℂ$
4 3 adantr ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to {A}\in ℂ$
5 4 ad2antrr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to {A}\in ℂ$
6 nn0re ${⊢}{A}\in {ℕ}_{0}\to {A}\in ℝ$
7 modcl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}\in ℝ$
8 6 7 sylan ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}\in ℝ$
9 8 recnd ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}\in ℂ$
10 9 adantr ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\to {A}\mathrm{mod}{M}\in ℂ$
11 eleq1 ${⊢}{A}\mathrm{mod}{M}={B}\to \left({A}\mathrm{mod}{M}\in ℂ↔{B}\in ℂ\right)$
12 11 adantl ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\to \left({A}\mathrm{mod}{M}\in ℂ↔{B}\in ℂ\right)$
13 10 12 mpbid ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\to {B}\in ℂ$
14 13 adantr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to {B}\in ℂ$
15 zcn ${⊢}{i}\in ℤ\to {i}\in ℂ$
16 15 adantl ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to {i}\in ℂ$
17 rpcn ${⊢}{M}\in {ℝ}^{+}\to {M}\in ℂ$
18 17 adantl ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to {M}\in ℂ$
19 18 ad2antrr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to {M}\in ℂ$
20 16 19 mulcld ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to {i}\cdot {M}\in ℂ$
21 5 14 20 subadd2d ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \left({A}-{B}={i}\cdot {M}↔{i}\cdot {M}+{B}={A}\right)$
22 eqcom ${⊢}{A}={i}\cdot {M}+{B}↔{i}\cdot {M}+{B}={A}$
23 21 22 syl6rbbr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \left({A}={i}\cdot {M}+{B}↔{A}-{B}={i}\cdot {M}\right)$
24 3 ad2antrr ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\to {A}\in ℂ$
25 24 13 subcld ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\to {A}-{B}\in ℂ$
26 25 adantr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to {A}-{B}\in ℂ$
27 rpcnne0 ${⊢}{M}\in {ℝ}^{+}\to \left({M}\in ℂ\wedge {M}\ne 0\right)$
28 27 adantl ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to \left({M}\in ℂ\wedge {M}\ne 0\right)$
29 28 ad2antrr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \left({M}\in ℂ\wedge {M}\ne 0\right)$
30 divmul3 ${⊢}\left({A}-{B}\in ℂ\wedge {i}\in ℂ\wedge \left({M}\in ℂ\wedge {M}\ne 0\right)\right)\to \left(\frac{{A}-{B}}{{M}}={i}↔{A}-{B}={i}\cdot {M}\right)$
31 26 16 29 30 syl3anc ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \left(\frac{{A}-{B}}{{M}}={i}↔{A}-{B}={i}\cdot {M}\right)$
32 oveq2 ${⊢}{B}={A}\mathrm{mod}{M}\to {A}-{B}={A}-\left({A}\mathrm{mod}{M}\right)$
33 32 oveq1d ${⊢}{B}={A}\mathrm{mod}{M}\to \frac{{A}-{B}}{{M}}=\frac{{A}-\left({A}\mathrm{mod}{M}\right)}{{M}}$
34 33 eqcoms ${⊢}{A}\mathrm{mod}{M}={B}\to \frac{{A}-{B}}{{M}}=\frac{{A}-\left({A}\mathrm{mod}{M}\right)}{{M}}$
35 34 adantl ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\to \frac{{A}-{B}}{{M}}=\frac{{A}-\left({A}\mathrm{mod}{M}\right)}{{M}}$
36 35 adantr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \frac{{A}-{B}}{{M}}=\frac{{A}-\left({A}\mathrm{mod}{M}\right)}{{M}}$
37 moddiffl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \frac{{A}-\left({A}\mathrm{mod}{M}\right)}{{M}}=⌊\frac{{A}}{{M}}⌋$
38 6 37 sylan ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to \frac{{A}-\left({A}\mathrm{mod}{M}\right)}{{M}}=⌊\frac{{A}}{{M}}⌋$
39 38 ad2antrr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \frac{{A}-\left({A}\mathrm{mod}{M}\right)}{{M}}=⌊\frac{{A}}{{M}}⌋$
40 36 39 eqtrd ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \frac{{A}-{B}}{{M}}=⌊\frac{{A}}{{M}}⌋$
41 40 eqeq1d ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \left(\frac{{A}-{B}}{{M}}={i}↔⌊\frac{{A}}{{M}}⌋={i}\right)$
42 23 31 41 3bitr2d ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \left({A}={i}\cdot {M}+{B}↔⌊\frac{{A}}{{M}}⌋={i}\right)$
43 nn0ge0 ${⊢}{A}\in {ℕ}_{0}\to 0\le {A}$
44 6 43 jca ${⊢}{A}\in {ℕ}_{0}\to \left({A}\in ℝ\wedge 0\le {A}\right)$
45 rpregt0 ${⊢}{M}\in {ℝ}^{+}\to \left({M}\in ℝ\wedge 0<{M}\right)$
46 divge0 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({M}\in ℝ\wedge 0<{M}\right)\right)\to 0\le \frac{{A}}{{M}}$
47 44 45 46 syl2an ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to 0\le \frac{{A}}{{M}}$
48 6 adantr ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to {A}\in ℝ$
49 rpre ${⊢}{M}\in {ℝ}^{+}\to {M}\in ℝ$
50 49 adantl ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to {M}\in ℝ$
51 rpne0 ${⊢}{M}\in {ℝ}^{+}\to {M}\ne 0$
52 51 adantl ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to {M}\ne 0$
53 48 50 52 redivcld ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to \frac{{A}}{{M}}\in ℝ$
54 0z ${⊢}0\in ℤ$
55 flge ${⊢}\left(\frac{{A}}{{M}}\in ℝ\wedge 0\in ℤ\right)\to \left(0\le \frac{{A}}{{M}}↔0\le ⌊\frac{{A}}{{M}}⌋\right)$
56 53 54 55 sylancl ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to \left(0\le \frac{{A}}{{M}}↔0\le ⌊\frac{{A}}{{M}}⌋\right)$
57 47 56 mpbid ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to 0\le ⌊\frac{{A}}{{M}}⌋$
58 breq2 ${⊢}⌊\frac{{A}}{{M}}⌋={i}\to \left(0\le ⌊\frac{{A}}{{M}}⌋↔0\le {i}\right)$
59 57 58 syl5ibcom ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to \left(⌊\frac{{A}}{{M}}⌋={i}\to 0\le {i}\right)$
60 59 ad2antrr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \left(⌊\frac{{A}}{{M}}⌋={i}\to 0\le {i}\right)$
61 42 60 sylbid ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\to \left({A}={i}\cdot {M}+{B}\to 0\le {i}\right)$
62 61 imp ${⊢}\left(\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\wedge {A}={i}\cdot {M}+{B}\right)\to 0\le {i}$
63 elnn0z ${⊢}{i}\in {ℕ}_{0}↔\left({i}\in ℤ\wedge 0\le {i}\right)$
64 2 62 63 sylanbrc ${⊢}\left(\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\wedge {A}={i}\cdot {M}+{B}\right)\to {i}\in {ℕ}_{0}$
65 oveq1 ${⊢}{k}={i}\to {k}\cdot {M}={i}\cdot {M}$
66 65 oveq1d ${⊢}{k}={i}\to {k}\cdot {M}+{B}={i}\cdot {M}+{B}$
67 66 eqeq2d ${⊢}{k}={i}\to \left({A}={k}\cdot {M}+{B}↔{A}={i}\cdot {M}+{B}\right)$
68 67 adantl ${⊢}\left(\left(\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\wedge {A}={i}\cdot {M}+{B}\right)\wedge {k}={i}\right)\to \left({A}={k}\cdot {M}+{B}↔{A}={i}\cdot {M}+{B}\right)$
69 simpr ${⊢}\left(\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\wedge {A}={i}\cdot {M}+{B}\right)\to {A}={i}\cdot {M}+{B}$
70 64 68 69 rspcedvd ${⊢}\left(\left(\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\wedge {i}\in ℤ\right)\wedge {A}={i}\cdot {M}+{B}\right)\to \exists {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+{B}$
71 nn0z ${⊢}{A}\in {ℕ}_{0}\to {A}\in ℤ$
72 modmuladdim ${⊢}\left({A}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}={B}\to \exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={i}\cdot {M}+{B}\right)$
73 71 72 sylan ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}={B}\to \exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={i}\cdot {M}+{B}\right)$
74 73 imp ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\to \exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}{A}={i}\cdot {M}+{B}$
75 70 74 r19.29a ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={B}\right)\to \exists {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+{B}$
76 75 ex ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}={B}\to \exists {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={k}\cdot {M}+{B}\right)$