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 )