Metamath Proof Explorer

Theorem nndivdvds

Description: Strong form of dvdsval2 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion nndivdvds ⊢ A ∈ ℕ ∧ B ∈ ℕ → B ∥ A ↔ A B ∈ ℕ

Proof

Step Hyp Ref Expression
1 nnz ⊢ B ∈ ℕ → B ∈ ℤ
2 nnne0 ⊢ B ∈ ℕ → B ≠ 0
3 nnz ⊢ A ∈ ℕ → A ∈ ℤ
4 3 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ → A ∈ ℤ
5 dvdsval2 ⊢ B ∈ ℤ ∧ B ≠ 0 ∧ A ∈ ℤ → B ∥ A ↔ A B ∈ ℤ
6 1 2 4 5 syl2an23an ⊢ A ∈ ℕ ∧ B ∈ ℕ → B ∥ A ↔ A B ∈ ℤ
7 6 anbi1d ⊢ A ∈ ℕ ∧ B ∈ ℕ → B ∥ A ∧ 0 < A B ↔ A B ∈ ℤ ∧ 0 < A B
8 nnre ⊢ A ∈ ℕ → A ∈ ℝ
9 8 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ → A ∈ ℝ
10 nnre ⊢ B ∈ ℕ → B ∈ ℝ
11 10 adantl ⊢ A ∈ ℕ ∧ B ∈ ℕ → B ∈ ℝ
12 nngt0 ⊢ A ∈ ℕ → 0 < A
13 12 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ → 0 < A
14 nngt0 ⊢ B ∈ ℕ → 0 < B
15 14 adantl ⊢ A ∈ ℕ ∧ B ∈ ℕ → 0 < B
16 9 11 13 15 divgt0d ⊢ A ∈ ℕ ∧ B ∈ ℕ → 0 < A B
17 16 biantrud ⊢ A ∈ ℕ ∧ B ∈ ℕ → B ∥ A ↔ B ∥ A ∧ 0 < A B
18 elnnz ⊢ A B ∈ ℕ ↔ A B ∈ ℤ ∧ 0 < A B
19 18 a1i ⊢ A ∈ ℕ ∧ B ∈ ℕ → A B ∈ ℕ ↔ A B ∈ ℤ ∧ 0 < A B
20 7 17 19 3bitr4d ⊢ A ∈ ℕ ∧ B ∈ ℕ → B ∥ A ↔ A B ∈ ℕ