modlt0b

Description: An integer with an absolute value less than a positive integer is 0 modulo the positive integer iff it is 0. (Contributed by AV, 21-Nov-2025)

		Ref	Expression
	Assertion	modlt0b	$⊢ (N \in ℕ \land X \in ℤ \land \|X\| < N) \to (X \mod N = 0 \leftrightarrow X = 0)$

Proof

Step	Hyp	Ref	Expression
1		pm3.22	$⊢ (N \in ℕ \land X \in ℤ) \to (X \in ℤ \land N \in ℕ)$
2	1	3adant3	$⊢ (N \in ℕ \land X \in ℤ \land \|X\| < N) \to (X \in ℤ \land N \in ℕ)$
3		mod0mul	$⊢ (X \in ℤ \land N \in ℕ) \to (X \mod N = 0 \to \exists z \in ℤ X = z \cdot N)$
4	2 3	syl	$⊢ (N \in ℕ \land X \in ℤ \land \|X\| < N) \to (X \mod N = 0 \to \exists z \in ℤ X = z \cdot N)$
5		simpr	$⊢ (((N \in ℕ \land X \in ℤ \land \|X\| < N) \land z \in ℤ) \land X = z \cdot N) \to X = z \cdot N$
6		fveq2	$⊢ X = z \cdot N \to \|X\| = \|z \cdot N\|$
7	6	adantl	$⊢ ((N \in ℕ \land z \in ℤ) \land X = z \cdot N) \to \|X\| = \|z \cdot N\|$
8	7	breq1d	$⊢ ((N \in ℕ \land z \in ℤ) \land X = z \cdot N) \to (\|X\| < N \leftrightarrow \|z \cdot N\| < N)$
9		zcn	$⊢ z \in ℤ \to z \in ℂ$
10		nncn	$⊢ N \in ℕ \to N \in ℂ$
11		absmul	$⊢ (z \in ℂ \land N \in ℂ) \to \|z \cdot N\| = \|z\| \|N\|$
12	9 10 11	syl2anr	$⊢ (N \in ℕ \land z \in ℤ) \to \|z \cdot N\| = \|z\| \|N\|$
13		nnre	$⊢ N \in ℕ \to N \in ℝ$
14		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
15	14	nn0ge0d	$⊢ N \in ℕ \to 0 \leq N$
16	13 15	absidd	$⊢ N \in ℕ \to \|N\| = N$
17	16	adantr	$⊢ (N \in ℕ \land z \in ℤ) \to \|N\| = N$
18	17	oveq2d	$⊢ (N \in ℕ \land z \in ℤ) \to \|z\| \|N\| = \|z\| \cdot N$
19	12 18	eqtrd	$⊢ (N \in ℕ \land z \in ℤ) \to \|z \cdot N\| = \|z\| \cdot N$
20	19	breq1d	$⊢ (N \in ℕ \land z \in ℤ) \to (\|z \cdot N\| < N \leftrightarrow \|z\| \cdot N < N)$
21	9	abscld	$⊢ z \in ℤ \to \|z\| \in ℝ$
22	21	adantl	$⊢ (N \in ℕ \land z \in ℤ) \to \|z\| \in ℝ$
23	13	adantr	$⊢ (N \in ℕ \land z \in ℤ) \to N \in ℝ$
24		nngt0	$⊢ N \in ℕ \to 0 < N$
25	13 24	jca	$⊢ N \in ℕ \to (N \in ℝ \land 0 < N)$
26	25	adantr	$⊢ (N \in ℕ \land z \in ℤ) \to (N \in ℝ \land 0 < N)$
27		ltmuldiv	$⊢ (\|z\| \in ℝ \land N \in ℝ \land (N \in ℝ \land 0 < N)) \to (\|z\| \cdot N < N \leftrightarrow \|z\| < \frac{N}{N})$
28	22 23 26 27	syl3anc	$⊢ (N \in ℕ \land z \in ℤ) \to (\|z\| \cdot N < N \leftrightarrow \|z\| < \frac{N}{N})$
29		nnne0	$⊢ N \in ℕ \to N \neq 0$
30	10 29	dividd	$⊢ N \in ℕ \to \frac{N}{N} = 1$
31	30	adantr	$⊢ (N \in ℕ \land z \in ℤ) \to \frac{N}{N} = 1$
32	31	breq2d	$⊢ (N \in ℕ \land z \in ℤ) \to (\|z\| < \frac{N}{N} \leftrightarrow \|z\| < 1)$
33	28 32	bitrd	$⊢ (N \in ℕ \land z \in ℤ) \to (\|z\| \cdot N < N \leftrightarrow \|z\| < 1)$
34		zabs0b	$⊢ z \in ℤ \to (\|z\| < 1 \leftrightarrow z = 0)$
35	34	adantl	$⊢ (N \in ℕ \land z \in ℤ) \to (\|z\| < 1 \leftrightarrow z = 0)$
36		oveq1	$⊢ z = 0 \to z \cdot N = 0 \cdot N$
37	10	mul02d	$⊢ N \in ℕ \to 0 \cdot N = 0$
38	36 37	sylan9eqr	$⊢ (N \in ℕ \land z = 0) \to z \cdot N = 0$
39	38	ex	$⊢ N \in ℕ \to (z = 0 \to z \cdot N = 0)$
40	39	adantr	$⊢ (N \in ℕ \land z \in ℤ) \to (z = 0 \to z \cdot N = 0)$
41	35 40	sylbid	$⊢ (N \in ℕ \land z \in ℤ) \to (\|z\| < 1 \to z \cdot N = 0)$
42	33 41	sylbid	$⊢ (N \in ℕ \land z \in ℤ) \to (\|z\| \cdot N < N \to z \cdot N = 0)$
43	20 42	sylbid	$⊢ (N \in ℕ \land z \in ℤ) \to (\|z \cdot N\| < N \to z \cdot N = 0)$
44	43	adantr	$⊢ ((N \in ℕ \land z \in ℤ) \land X = z \cdot N) \to (\|z \cdot N\| < N \to z \cdot N = 0)$
45	8 44	sylbid	$⊢ ((N \in ℕ \land z \in ℤ) \land X = z \cdot N) \to (\|X\| < N \to z \cdot N = 0)$
46	45	expl	$⊢ N \in ℕ \to ((z \in ℤ \land X = z \cdot N) \to (\|X\| < N \to z \cdot N = 0))$
47	46	adantr	$⊢ (N \in ℕ \land X \in ℤ) \to ((z \in ℤ \land X = z \cdot N) \to (\|X\| < N \to z \cdot N = 0))$
48	47	com23	$⊢ (N \in ℕ \land X \in ℤ) \to (\|X\| < N \to ((z \in ℤ \land X = z \cdot N) \to z \cdot N = 0))$
49	48	3impia	$⊢ (N \in ℕ \land X \in ℤ \land \|X\| < N) \to ((z \in ℤ \land X = z \cdot N) \to z \cdot N = 0)$
50	49	impl	$⊢ (((N \in ℕ \land X \in ℤ \land \|X\| < N) \land z \in ℤ) \land X = z \cdot N) \to z \cdot N = 0$
51	5 50	eqtrd	$⊢ (((N \in ℕ \land X \in ℤ \land \|X\| < N) \land z \in ℤ) \land X = z \cdot N) \to X = 0$
52	51	ex	$⊢ ((N \in ℕ \land X \in ℤ \land \|X\| < N) \land z \in ℤ) \to (X = z \cdot N \to X = 0)$
53	52	rexlimdva	$⊢ (N \in ℕ \land X \in ℤ \land \|X\| < N) \to (\exists z \in ℤ X = z \cdot N \to X = 0)$
54	4 53	syld	$⊢ (N \in ℕ \land X \in ℤ \land \|X\| < N) \to (X \mod N = 0 \to X = 0)$
55		oveq1	$⊢ X = 0 \to X \mod N = 0 \mod N$
56		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
57		0mod	$⊢ N \in ℝ^{+} \to 0 \mod N = 0$
58	56 57	syl	$⊢ N \in ℕ \to 0 \mod N = 0$
59	58	3ad2ant1	$⊢ (N \in ℕ \land X \in ℤ \land \|X\| < N) \to 0 \mod N = 0$
60	55 59	sylan9eqr	$⊢ ((N \in ℕ \land X \in ℤ \land \|X\| < N) \land X = 0) \to X \mod N = 0$
61	60	ex	$⊢ (N \in ℕ \land X \in ℤ \land \|X\| < N) \to (X = 0 \to X \mod N = 0)$
62	54 61	impbid	$⊢ (N \in ℕ \land X \in ℤ \land \|X\| < N) \to (X \mod N = 0 \leftrightarrow X = 0)$

Metamath Proof Explorer

Theorem modlt0b

Proof