Metamath Proof Explorer


Theorem 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 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) ≠ 0 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2 1 adantr ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℝ )
3 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
4 3 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
5 nnne0 ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
6 5 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
7 2 4 6 redivcld ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) ∈ ℝ )
8 7 flcld ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ∈ ℤ )
9 8 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ∈ ℤ )
10 zmodfzo ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
11 10 anim1i ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( ( 𝐴 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) )
12 fzo1fzo0n0 ( ( 𝐴 mod 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ↔ ( ( 𝐴 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) )
13 11 12 sylibr ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( 𝐴 mod 𝑁 ) ∈ ( 1 ..^ 𝑁 ) )
14 nnrp ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
15 1 14 anim12i ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
16 15 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
17 flpmodeq ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) = 𝐴 )
18 16 17 syl ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) = 𝐴 )
19 18 eqcomd ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) )
20 oveq1 ( 𝑥 = ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) → ( 𝑥 · 𝑁 ) = ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) )
21 20 oveq1d ( 𝑥 = ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) → ( ( 𝑥 · 𝑁 ) + 𝑦 ) = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + 𝑦 ) )
22 21 eqeq2d ( 𝑥 = ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) → ( 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ↔ 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + 𝑦 ) ) )
23 oveq2 ( 𝑦 = ( 𝐴 mod 𝑁 ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + 𝑦 ) = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) )
24 23 eqeq2d ( 𝑦 = ( 𝐴 mod 𝑁 ) → ( 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + 𝑦 ) ↔ 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) ) )
25 22 24 rspc2ev ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ∈ ℤ ∧ ( 𝐴 mod 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ∧ 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) )
26 9 13 19 25 syl3anc ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) )
27 26 ex ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) ≠ 0 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) )