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

Metamath Proof Explorer

Theorem modelico

Description: Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014)

Ref Expression
Assertion modelico ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) ∈ ( 0 [,) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 modcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) ∈ ℝ )
2 modge0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 0 ≤ ( 𝐴 mod 𝐵 ) )
3 modlt ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) < 𝐵 )
4 0re ⊢ 0 ∈ ℝ
5 rpxr ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ* )
6 5 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ* )
7 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 mod 𝐵 ) ∈ ( 0 [,) 𝐵 ) ↔ ( ( 𝐴 mod 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 mod 𝐵 ) ∧ ( 𝐴 mod 𝐵 ) < 𝐵 ) ) )
8 4 6 7 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) ∈ ( 0 [,) 𝐵 ) ↔ ( ( 𝐴 mod 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 mod 𝐵 ) ∧ ( 𝐴 mod 𝐵 ) < 𝐵 ) ) )
9 1 2 3 8 mpbir3and ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) ∈ ( 0 [,) 𝐵 ) )