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↔AB∈ℕ

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↔AB∈ℤ
6 1 2 4 5 syl2an23an ⊢A∈ℕ∧B∈ℕ→B∥A↔AB∈ℤ
7 6 anbi1d ⊢A∈ℕ∧B∈ℕ→B∥A∧0<AB↔AB∈ℤ∧0<AB
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<AB
17 16 biantrud ⊢A∈ℕ∧B∈ℕ→B∥A↔B∥A∧0<AB
18 elnnz ⊢AB∈ℕ↔AB∈ℤ∧0<AB
19 18 a1i ⊢A∈ℕ∧B∈ℕ→AB∈ℕ↔AB∈ℤ∧0<AB
20 7 17 19 3bitr4d ⊢A∈ℕ∧B∈ℕ→B∥A↔AB∈ℕ