Step |
Hyp |
Ref |
Expression |
1 |
|
zcn |
⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ ) |
2 |
1
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → 𝐵 ∈ ℂ ) |
3 |
|
zcn |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ ) |
4 |
3
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → 𝐴 ∈ ℂ ) |
5 |
|
nncn |
⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℂ ) |
6 |
|
nnne0 |
⊢ ( 𝐷 ∈ ℕ → 𝐷 ≠ 0 ) |
7 |
5 6
|
jca |
⊢ ( 𝐷 ∈ ℕ → ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) |
8 |
7
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) |
9 |
|
divass |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐵 · 𝐴 ) / 𝐷 ) = ( 𝐵 · ( 𝐴 / 𝐷 ) ) ) |
10 |
2 4 8 9
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( 𝐵 · 𝐴 ) / 𝐷 ) = ( 𝐵 · ( 𝐴 / 𝐷 ) ) ) |
11 |
10
|
3comr |
⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐵 · 𝐴 ) / 𝐷 ) = ( 𝐵 · ( 𝐴 / 𝐷 ) ) ) |
12 |
11
|
adantr |
⊢ ( ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 / 𝐷 ) ∈ ℤ ) → ( ( 𝐵 · 𝐴 ) / 𝐷 ) = ( 𝐵 · ( 𝐴 / 𝐷 ) ) ) |
13 |
|
zmulcl |
⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 / 𝐷 ) ∈ ℤ ) → ( 𝐵 · ( 𝐴 / 𝐷 ) ) ∈ ℤ ) |
14 |
13
|
3ad2antl3 |
⊢ ( ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 / 𝐷 ) ∈ ℤ ) → ( 𝐵 · ( 𝐴 / 𝐷 ) ) ∈ ℤ ) |
15 |
12 14
|
eqeltrd |
⊢ ( ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 / 𝐷 ) ∈ ℤ ) → ( ( 𝐵 · 𝐴 ) / 𝐷 ) ∈ ℤ ) |