modn0mul

Description: If an integer is not 0 modulo a positive integer, this integer must be the sum of the product of another integer and the modulus and a positive integer less than the modulus. (Contributed by AV, 7-Jun-2020)

		Ref	Expression
	Assertion	modn0mul	$⊢ (A \in ℤ \land N \in ℕ) \to (A \mod N \neq 0 \to \exists x \in ℤ \exists y \in (1 ..^N) A = x \cdot N + y)$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ A \in ℤ \to A \in ℝ$
2	1	adantr	$⊢ (A \in ℤ \land N \in ℕ) \to A \in ℝ$
3		nnre	$⊢ N \in ℕ \to N \in ℝ$
4	3	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \in ℝ$
5		nnne0	$⊢ N \in ℕ \to N \neq 0$
6	5	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \neq 0$
7	2 4 6	redivcld	$⊢ (A \in ℤ \land N \in ℕ) \to \frac{A}{N} \in ℝ$
8	7	flcld	$⊢ (A \in ℤ \land N \in ℕ) \to ⌊\frac{A}{N}⌋ \in ℤ$
9	8	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N \neq 0) \to ⌊\frac{A}{N}⌋ \in ℤ$
10		zmodfzo	$⊢ (A \in ℤ \land N \in ℕ) \to A \mod N \in (0 ..^N)$
11	10	anim1i	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N \neq 0) \to (A \mod N \in (0 ..^N) \land A \mod N \neq 0)$
12		fzo1fzo0n0	$⊢ A \mod N \in (1 ..^N) \leftrightarrow (A \mod N \in (0 ..^N) \land A \mod N \neq 0)$
13	11 12	sylibr	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N \neq 0) \to A \mod N \in (1 ..^N)$
14		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
15	1 14	anim12i	$⊢ (A \in ℤ \land N \in ℕ) \to (A \in ℝ \land N \in ℝ^{+})$
16	15	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N \neq 0) \to (A \in ℝ \land N \in ℝ^{+})$
17		flpmodeq	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to ⌊\frac{A}{N}⌋ \cdot N + (A \mod N) = A$
18	16 17	syl	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N \neq 0) \to ⌊\frac{A}{N}⌋ \cdot N + (A \mod N) = A$
19	18	eqcomd	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N \neq 0) \to A = ⌊\frac{A}{N}⌋ \cdot N + (A \mod N)$
20		oveq1	$⊢ x = ⌊\frac{A}{N}⌋ \to x \cdot N = ⌊\frac{A}{N}⌋ \cdot N$
21	20	oveq1d	$⊢ x = ⌊\frac{A}{N}⌋ \to x \cdot N + y = ⌊\frac{A}{N}⌋ \cdot N + y$
22	21	eqeq2d	$⊢ x = ⌊\frac{A}{N}⌋ \to (A = x \cdot N + y \leftrightarrow A = ⌊\frac{A}{N}⌋ \cdot N + y)$
23		oveq2	$⊢ y = A \mod N \to ⌊\frac{A}{N}⌋ \cdot N + y = ⌊\frac{A}{N}⌋ \cdot N + (A \mod N)$
24	23	eqeq2d	$⊢ y = A \mod N \to (A = ⌊\frac{A}{N}⌋ \cdot N + y \leftrightarrow A = ⌊\frac{A}{N}⌋ \cdot N + (A \mod N))$
25	22 24	rspc2ev	$⊢ (⌊\frac{A}{N}⌋ \in ℤ \land A \mod N \in (1 ..^N) \land A = ⌊\frac{A}{N}⌋ \cdot N + (A \mod N)) \to \exists x \in ℤ \exists y \in (1 ..^N) A = x \cdot N + y$
26	9 13 19 25	syl3anc	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N \neq 0) \to \exists x \in ℤ \exists y \in (1 ..^N) A = x \cdot N + y$
27	26	ex	$⊢ (A \in ℤ \land N \in ℕ) \to (A \mod N \neq 0 \to \exists x \in ℤ \exists y \in (1 ..^N) A = x \cdot N + y)$

Metamath Proof Explorer

Theorem modn0mul

Proof