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	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )