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