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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 ∥ 𝐴 ↔ ( 𝐴 / 𝐵 ) ∈ ℕ ) )

Proof

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