Metamath Proof Explorer

Theorem zmodfz

Description: An integer mod B lies in the first B nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010)

Ref Expression
Assertion zmodfz ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\right)\to {A}\mathrm{mod}{B}\in \left(0\dots {B}-1\right)$

Proof

Step Hyp Ref Expression
1 zmodcl ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\right)\to {A}\mathrm{mod}{B}\in {ℕ}_{0}$
2 1 nn0zd ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\right)\to {A}\mathrm{mod}{B}\in ℤ$
3 1 nn0ge0d ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\right)\to 0\le {A}\mathrm{mod}{B}$
4 zre ${⊢}{A}\in ℤ\to {A}\in ℝ$
5 nnrp ${⊢}{B}\in ℕ\to {B}\in {ℝ}^{+}$
6 modlt ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}<{B}$
7 4 5 6 syl2an ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\right)\to {A}\mathrm{mod}{B}<{B}$
8 0z ${⊢}0\in ℤ$
9 nnz ${⊢}{B}\in ℕ\to {B}\in ℤ$
10 9 adantl ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\right)\to {B}\in ℤ$
11 elfzm11 ${⊢}\left(0\in ℤ\wedge {B}\in ℤ\right)\to \left({A}\mathrm{mod}{B}\in \left(0\dots {B}-1\right)↔\left({A}\mathrm{mod}{B}\in ℤ\wedge 0\le {A}\mathrm{mod}{B}\wedge {A}\mathrm{mod}{B}<{B}\right)\right)$
12 8 10 11 sylancr ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\right)\to \left({A}\mathrm{mod}{B}\in \left(0\dots {B}-1\right)↔\left({A}\mathrm{mod}{B}\in ℤ\wedge 0\le {A}\mathrm{mod}{B}\wedge {A}\mathrm{mod}{B}<{B}\right)\right)$
13 2 3 7 12 mpbir3and ${⊢}\left({A}\in ℤ\wedge {B}\in ℕ\right)\to {A}\mathrm{mod}{B}\in \left(0\dots {B}-1\right)$