Metamath Proof Explorer

Theorem absmod0

Description: A is divisible by B iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion absmod0 ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = 0 ↔ A mod B = 0

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = A → A mod B = A mod B
2 1 eqcoms ⊢ A = A → A mod B = A mod B
3 2 eqeq1d ⊢ A = A → A mod B = 0 ↔ A mod B = 0
4 3 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A = A → A mod B = 0 ↔ A mod B = 0
5 negmod0 ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = 0 ↔ − A mod B = 0
6 oveq1 ⊢ A = − A → A mod B = − A mod B
7 6 eqeq1d ⊢ A = − A → A mod B = 0 ↔ − A mod B = 0
8 7 bibi2d ⊢ A = − A → A mod B = 0 ↔ A mod B = 0 ↔ A mod B = 0 ↔ − A mod B = 0
9 5 8 syl5ibrcom ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A = − A → A mod B = 0 ↔ A mod B = 0
10 absor ⊢ A ∈ ℝ → A = A ∨ A = − A
11 10 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A = A ∨ A = − A
12 4 9 11 mpjaod ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = 0 ↔ A mod B = 0