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