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 [,) 𝐵 ) )