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