modmuladdnn0

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	$⊢ (A \in ℕ_{0} \land M \in ℝ^{+}) \to (A \mod M = B \to \exists k \in ℕ_{0} A = k \cdot M + B)$

Proof

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

Metamath Proof Explorer

Theorem modmuladdnn0

Proof