Metamath Proof Explorer

Theorem zdiv

Description: Two ways to express " M divides N ". (Contributed by NM, 3-Oct-2008)

Ref Expression
Assertion zdiv ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )

Proof

Step Hyp Ref Expression
1 nnne0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 )
2 1 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → 𝑀 ≠ 0 )
3 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
4 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
5 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
6 divcan3 ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = 𝑘 )
7 6 3coml ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ∧ 𝑘 ∈ ℂ ) → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = 𝑘 )
8 7 3expa ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ 𝑘 ∈ ℂ ) → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = 𝑘 )
9 5 8 sylan2 ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = 𝑘 )
10 9 3adantl2 ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = 𝑘 )
11 oveq1 ⊢ ( ( 𝑀 · 𝑘 ) = 𝑁 → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = ( 𝑁 / 𝑀 ) )
12 10 11 sylan9req ⊢ ( ( ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → 𝑘 = ( 𝑁 / 𝑀 ) )
13 simplr ⊢ ( ( ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → 𝑘 ∈ ℤ )
14 12 13 eqeltrrd ⊢ ( ( ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → ( 𝑁 / 𝑀 ) ∈ ℤ )
15 14 rexlimdva2 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑀 ≠ 0 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 → ( 𝑁 / 𝑀 ) ∈ ℤ ) )
16 divcan2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) → ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 )
17 16 3com12 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑀 ≠ 0 ) → ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 )
18 oveq2 ⊢ ( 𝑘 = ( 𝑁 / 𝑀 ) → ( 𝑀 · 𝑘 ) = ( 𝑀 · ( 𝑁 / 𝑀 ) ) )
19 18 eqeq1d ⊢ ( 𝑘 = ( 𝑁 / 𝑀 ) → ( ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) )
20 19 rspcev ⊢ ( ( ( 𝑁 / 𝑀 ) ∈ ℤ ∧ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 )
21 20 expcom ⊢ ( ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 → ( ( 𝑁 / 𝑀 ) ∈ ℤ → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ) )
22 17 21 syl ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑀 ≠ 0 ) → ( ( 𝑁 / 𝑀 ) ∈ ℤ → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ) )
23 15 22 impbid ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑀 ≠ 0 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )
24 23 3expia ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑀 ≠ 0 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) ) )
25 3 4 24 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≠ 0 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) ) )
26 2 25 mpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )