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

Metamath Proof Explorer

Theorem modid2

Description: Identity law for modulo. (Contributed by NM, 29-Dec-2008)

Ref Expression
Assertion modid2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 𝐴 ↔ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 modge0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 0 ≤ ( 𝐴 mod 𝐵 ) )
2 modlt ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) < 𝐵 )
3 1 2 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 0 ≤ ( 𝐴 mod 𝐵 ) ∧ ( 𝐴 mod 𝐵 ) < 𝐵 ) )
4 breq2 ⊢ ( ( 𝐴 mod 𝐵 ) = 𝐴 → ( 0 ≤ ( 𝐴 mod 𝐵 ) ↔ 0 ≤ 𝐴 ) )
5 breq1 ⊢ ( ( 𝐴 mod 𝐵 ) = 𝐴 → ( ( 𝐴 mod 𝐵 ) < 𝐵 ↔ 𝐴 < 𝐵 ) )
6 4 5 anbi12d ⊢ ( ( 𝐴 mod 𝐵 ) = 𝐴 → ( ( 0 ≤ ( 𝐴 mod 𝐵 ) ∧ ( 𝐴 mod 𝐵 ) < 𝐵 ) ↔ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) )
7 3 6 syl5ibcom ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 𝐴 → ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) )
8 modid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 mod 𝐵 ) = 𝐴 )
9 8 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → ( 𝐴 mod 𝐵 ) = 𝐴 ) )
10 7 9 impbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 𝐴 ↔ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) )