Metamath Proof Explorer

Theorem 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 ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) → ( ( 𝑋 mod 𝑁 ) = 0 ↔ 𝑋 = 0 ) )

Proof

Step Hyp Ref Expression
1 pm3.22 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ) → ( 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
2 1 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) → ( 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
3 mod0mul ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑋 mod 𝑁 ) = 0 → ∃ 𝑧 ∈ ℤ 𝑋 = ( 𝑧 · 𝑁 ) ) )
4 2 3 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) → ( ( 𝑋 mod 𝑁 ) = 0 → ∃ 𝑧 ∈ ℤ 𝑋 = ( 𝑧 · 𝑁 ) ) )
5 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) ∧ 𝑧 ∈ ℤ ) ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → 𝑋 = ( 𝑧 · 𝑁 ) )
6 fveq2 ⊢ ( 𝑋 = ( 𝑧 · 𝑁 ) → ( abs ‘ 𝑋 ) = ( abs ‘ ( 𝑧 · 𝑁 ) ) )
7 6 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → ( abs ‘ 𝑋 ) = ( abs ‘ ( 𝑧 · 𝑁 ) ) )
8 7 breq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → ( ( abs ‘ 𝑋 ) < 𝑁 ↔ ( abs ‘ ( 𝑧 · 𝑁 ) ) < 𝑁 ) )
9 zcn ⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
10 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
11 absmul ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( abs ‘ ( 𝑧 · 𝑁 ) ) = ( ( abs ‘ 𝑧 ) · ( abs ‘ 𝑁 ) ) )
12 9 10 11 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( abs ‘ ( 𝑧 · 𝑁 ) ) = ( ( abs ‘ 𝑧 ) · ( abs ‘ 𝑁 ) ) )
13 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
14 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
15 14 nn0ge0d ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 𝑁 )
16 13 15 absidd ⊢ ( 𝑁 ∈ ℕ → ( abs ‘ 𝑁 ) = 𝑁 )
17 16 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( abs ‘ 𝑁 ) = 𝑁 )
18 17 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( abs ‘ 𝑧 ) · ( abs ‘ 𝑁 ) ) = ( ( abs ‘ 𝑧 ) · 𝑁 ) )
19 12 18 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( abs ‘ ( 𝑧 · 𝑁 ) ) = ( ( abs ‘ 𝑧 ) · 𝑁 ) )
20 19 breq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( abs ‘ ( 𝑧 · 𝑁 ) ) < 𝑁 ↔ ( ( abs ‘ 𝑧 ) · 𝑁 ) < 𝑁 ) )
21 9 abscld ⊢ ( 𝑧 ∈ ℤ → ( abs ‘ 𝑧 ) ∈ ℝ )
22 21 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( abs ‘ 𝑧 ) ∈ ℝ )
23 13 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → 𝑁 ∈ ℝ )
24 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
25 13 24 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
26 25 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
27 ltmuldiv ⊢ ( ( ( abs ‘ 𝑧 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( ( abs ‘ 𝑧 ) · 𝑁 ) < 𝑁 ↔ ( abs ‘ 𝑧 ) < ( 𝑁 / 𝑁 ) ) )
28 22 23 26 27 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( ( abs ‘ 𝑧 ) · 𝑁 ) < 𝑁 ↔ ( abs ‘ 𝑧 ) < ( 𝑁 / 𝑁 ) ) )
29 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
30 10 29 dividd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / 𝑁 ) = 1 )
31 30 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 𝑁 / 𝑁 ) = 1 )
32 31 breq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( abs ‘ 𝑧 ) < ( 𝑁 / 𝑁 ) ↔ ( abs ‘ 𝑧 ) < 1 ) )
33 28 32 bitrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( ( abs ‘ 𝑧 ) · 𝑁 ) < 𝑁 ↔ ( abs ‘ 𝑧 ) < 1 ) )
34 zabs0b ⊢ ( 𝑧 ∈ ℤ → ( ( abs ‘ 𝑧 ) < 1 ↔ 𝑧 = 0 ) )
35 34 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( abs ‘ 𝑧 ) < 1 ↔ 𝑧 = 0 ) )
36 oveq1 ⊢ ( 𝑧 = 0 → ( 𝑧 · 𝑁 ) = ( 0 · 𝑁 ) )
37 10 mul02d ⊢ ( 𝑁 ∈ ℕ → ( 0 · 𝑁 ) = 0 )
38 36 37 sylan9eqr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 = 0 ) → ( 𝑧 · 𝑁 ) = 0 )
39 38 ex ⊢ ( 𝑁 ∈ ℕ → ( 𝑧 = 0 → ( 𝑧 · 𝑁 ) = 0 ) )
40 39 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 = 0 → ( 𝑧 · 𝑁 ) = 0 ) )
41 35 40 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( abs ‘ 𝑧 ) < 1 → ( 𝑧 · 𝑁 ) = 0 ) )
42 33 41 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( ( abs ‘ 𝑧 ) · 𝑁 ) < 𝑁 → ( 𝑧 · 𝑁 ) = 0 ) )
43 20 42 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( abs ‘ ( 𝑧 · 𝑁 ) ) < 𝑁 → ( 𝑧 · 𝑁 ) = 0 ) )
44 43 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → ( ( abs ‘ ( 𝑧 · 𝑁 ) ) < 𝑁 → ( 𝑧 · 𝑁 ) = 0 ) )
45 8 44 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → ( ( abs ‘ 𝑋 ) < 𝑁 → ( 𝑧 · 𝑁 ) = 0 ) )
46 45 expl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑧 ∈ ℤ ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → ( ( abs ‘ 𝑋 ) < 𝑁 → ( 𝑧 · 𝑁 ) = 0 ) ) )
47 46 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ) → ( ( 𝑧 ∈ ℤ ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → ( ( abs ‘ 𝑋 ) < 𝑁 → ( 𝑧 · 𝑁 ) = 0 ) ) )
48 47 com23 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ) → ( ( abs ‘ 𝑋 ) < 𝑁 → ( ( 𝑧 ∈ ℤ ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → ( 𝑧 · 𝑁 ) = 0 ) ) )
49 48 3impia ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → ( 𝑧 · 𝑁 ) = 0 ) )
50 49 impl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) ∧ 𝑧 ∈ ℤ ) ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → ( 𝑧 · 𝑁 ) = 0 )
51 5 50 eqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) ∧ 𝑧 ∈ ℤ ) ∧ 𝑋 = ( 𝑧 · 𝑁 ) ) → 𝑋 = 0 )
52 51 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) ∧ 𝑧 ∈ ℤ ) → ( 𝑋 = ( 𝑧 · 𝑁 ) → 𝑋 = 0 ) )
53 52 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) → ( ∃ 𝑧 ∈ ℤ 𝑋 = ( 𝑧 · 𝑁 ) → 𝑋 = 0 ) )
54 4 53 syld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) → ( ( 𝑋 mod 𝑁 ) = 0 → 𝑋 = 0 ) )
55 oveq1 ⊢ ( 𝑋 = 0 → ( 𝑋 mod 𝑁 ) = ( 0 mod 𝑁 ) )
56 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
57 0mod ⊢ ( 𝑁 ∈ ℝ+ → ( 0 mod 𝑁 ) = 0 )
58 56 57 syl ⊢ ( 𝑁 ∈ ℕ → ( 0 mod 𝑁 ) = 0 )
59 58 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) → ( 0 mod 𝑁 ) = 0 )
60 55 59 sylan9eqr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) ∧ 𝑋 = 0 ) → ( 𝑋 mod 𝑁 ) = 0 )
61 60 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) → ( 𝑋 = 0 → ( 𝑋 mod 𝑁 ) = 0 ) )
62 54 61 impbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ ( abs ‘ 𝑋 ) < 𝑁 ) → ( ( 𝑋 mod 𝑁 ) = 0 ↔ 𝑋 = 0 ) )