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

Metamath Proof Explorer

Theorem negmod0

Description: A is divisible by B iff its negative is. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Fan Zheng, 7-Jun-2016)

Ref Expression
Assertion negmod0 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 mod 𝐵 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 rerpdivcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
2 recn ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( 𝐴 / 𝐵 ) ∈ ℂ )
3 znegclb ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℂ → ( ( 𝐴 / 𝐵 ) ∈ ℤ ↔ - ( 𝐴 / 𝐵 ) ∈ ℤ ) )
4 1 2 3 3syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ∈ ℤ ↔ - ( 𝐴 / 𝐵 ) ∈ ℤ ) )
5 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
7 rpcn ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
8 7 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
9 rpne0 ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
10 9 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ≠ 0 )
11 6 8 10 divnegd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - ( 𝐴 / 𝐵 ) = ( - 𝐴 / 𝐵 ) )
12 11 eleq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( - ( 𝐴 / 𝐵 ) ∈ ℤ ↔ ( - 𝐴 / 𝐵 ) ∈ ℤ ) )
13 4 12 bitrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ∈ ℤ ↔ ( - 𝐴 / 𝐵 ) ∈ ℤ ) )
14 mod0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( 𝐴 / 𝐵 ) ∈ ℤ ) )
15 renegcl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
16 mod0 ⊢ ( ( - 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( - 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 / 𝐵 ) ∈ ℤ ) )
17 15 16 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( - 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 / 𝐵 ) ∈ ℤ ) )
18 13 14 17 3bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 mod 𝐵 ) = 0 ) )