Step |
Hyp |
Ref |
Expression |
1 |
|
zdivgd.1 |
⊢ ( 𝜑 → 𝑀 ∈ ℂ ) |
2 |
|
zdivgd.2 |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
3 |
|
zdivgd.3 |
⊢ ( 𝜑 → 𝑀 ≠ 0 ) |
4 |
|
zcn |
⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ ) |
5 |
4
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ ) |
6 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑀 ∈ ℂ ) |
7 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑀 ≠ 0 ) |
8 |
5 6 7
|
divcan3d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = 𝑘 ) |
9 |
|
oveq1 |
⊢ ( ( 𝑀 · 𝑘 ) = 𝑁 → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = ( 𝑁 / 𝑀 ) ) |
10 |
8 9
|
sylan9req |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → 𝑘 = ( 𝑁 / 𝑀 ) ) |
11 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → 𝑘 ∈ ℤ ) |
12 |
10 11
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → ( 𝑁 / 𝑀 ) ∈ ℤ ) |
13 |
12
|
rexlimdva2 |
⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 → ( 𝑁 / 𝑀 ) ∈ ℤ ) ) |
14 |
2 1 3
|
divcan2d |
⊢ ( 𝜑 → ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) |
15 |
|
oveq2 |
⊢ ( 𝑘 = ( 𝑁 / 𝑀 ) → ( 𝑀 · 𝑘 ) = ( 𝑀 · ( 𝑁 / 𝑀 ) ) ) |
16 |
15
|
eqeq1d |
⊢ ( 𝑘 = ( 𝑁 / 𝑀 ) → ( ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) ) |
17 |
16
|
rspcev |
⊢ ( ( ( 𝑁 / 𝑀 ) ∈ ℤ ∧ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ) |
18 |
17
|
ex |
⊢ ( ( 𝑁 / 𝑀 ) ∈ ℤ → ( ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ) ) |
19 |
14 18
|
syl5com |
⊢ ( 𝜑 → ( ( 𝑁 / 𝑀 ) ∈ ℤ → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ) ) |
20 |
13 19
|
impbid |
⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) ) |