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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( ( abs ‘ 𝐴 ) mod 𝐵 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝐴 = ( abs ‘ 𝐴 ) → ( 𝐴 mod 𝐵 ) = ( ( abs ‘ 𝐴 ) mod 𝐵 ) )
2 1 eqcoms ⊢ ( ( abs ‘ 𝐴 ) = 𝐴 → ( 𝐴 mod 𝐵 ) = ( ( abs ‘ 𝐴 ) mod 𝐵 ) )
3 2 eqeq1d ⊢ ( ( abs ‘ 𝐴 ) = 𝐴 → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( ( abs ‘ 𝐴 ) mod 𝐵 ) = 0 ) )
4 3 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( abs ‘ 𝐴 ) = 𝐴 → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( ( abs ‘ 𝐴 ) mod 𝐵 ) = 0 ) ) )
5 negmod0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 mod 𝐵 ) = 0 ) )
6 oveq1 ⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( abs ‘ 𝐴 ) mod 𝐵 ) = ( - 𝐴 mod 𝐵 ) )
7 6 eqeq1d ⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( ( abs ‘ 𝐴 ) mod 𝐵 ) = 0 ↔ ( - 𝐴 mod 𝐵 ) = 0 ) )
8 7 bibi2d ⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( ( abs ‘ 𝐴 ) mod 𝐵 ) = 0 ) ↔ ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 mod 𝐵 ) = 0 ) ) )
9 5 8 syl5ibrcom ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( ( abs ‘ 𝐴 ) mod 𝐵 ) = 0 ) ) )
10 absor ⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) = 𝐴 ∨ ( abs ‘ 𝐴 ) = - 𝐴 ) )
11 10 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( abs ‘ 𝐴 ) = 𝐴 ∨ ( abs ‘ 𝐴 ) = - 𝐴 ) )
12 4 9 11 mpjaod ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( ( abs ‘ 𝐴 ) mod 𝐵 ) = 0 ) )