Metamath Proof Explorer

Theorem mod0

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

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

Proof

Step Hyp Ref Expression
1 modval ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = A − B ⁢ A B
2 1 eqeq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = 0 ↔ A − B ⁢ A B = 0
3 recn ⊢ A ∈ ℝ → A ∈ ℂ
4 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A ∈ ℂ
5 rpre ⊢ B ∈ ℝ + → B ∈ ℝ
6 5 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ∈ ℝ
7 refldivcl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ∈ ℝ
8 6 7 remulcld ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B ∈ ℝ
9 8 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B ∈ ℂ
10 4 9 subeq0ad ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A − B ⁢ A B = 0 ↔ A = B ⁢ A B
11 2 10 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = 0 ↔ A = B ⁢ A B
12 7 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ∈ ℂ
13 rpcnne0 ⊢ B ∈ ℝ + → B ∈ ℂ ∧ B ≠ 0
14 13 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ∈ ℂ ∧ B ≠ 0
15 divmul2 ⊢ A ∈ ℂ ∧ A B ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A B ↔ A = B ⁢ A B
16 4 12 14 15 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B = A B ↔ A = B ⁢ A B
17 eqcom ⊢ A B = A B ↔ A B = A B
18 16 17 bitr3di ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A = B ⁢ A B ↔ A B = A B
19 11 18 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = 0 ↔ A B = A B
20 rerpdivcl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ∈ ℝ
21 flidz ⊢ A B ∈ ℝ → A B = A B ↔ A B ∈ ℤ
22 20 21 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B = A B ↔ A B ∈ ℤ
23 19 22 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = 0 ↔ A B ∈ ℤ