This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zmodcl

Description: Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008)

Ref Expression
Assertion zmodcl ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 mod 𝐵 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2 nnrp ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
3 modval ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
5 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
6 5 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℤ )
7 nndivre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
8 1 7 sylan ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
9 8 flcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℤ )
10 6 9 zmulcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ∈ ℤ )
11 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ∈ ℤ ) → ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) ∈ ℤ )
12 10 11 syldan ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) ∈ ℤ )
13 4 12 eqeltrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 mod 𝐵 ) ∈ ℤ )
14 modge0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 0 ≤ ( 𝐴 mod 𝐵 ) )
15 1 2 14 syl2an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 0 ≤ ( 𝐴 mod 𝐵 ) )
16 elnn0z ⊢ ( ( 𝐴 mod 𝐵 ) ∈ ℕ0 ↔ ( ( 𝐴 mod 𝐵 ) ∈ ℤ ∧ 0 ≤ ( 𝐴 mod 𝐵 ) ) )
17 13 15 16 sylanbrc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 mod 𝐵 ) ∈ ℕ0 )