Theorem dvdsval2

Description: One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013)

	Ref	Expression
Assertion	dvdsval2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		divides	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 ) )
2	1	3adant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 ) )
3		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
4	3	3ad2ant3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
5	4	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → 𝑁 ∈ ℂ )
6		zcn	⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
7	6	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
8		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
9	8	3ad2ant1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℂ )
10	9	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → 𝑀 ∈ ℂ )
11		simpl2	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → 𝑀 ≠ 0 )
12	5 7 10 11	divmul3d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 / 𝑀 ) = 𝑘 ↔ 𝑁 = ( 𝑘 · 𝑀 ) ) )
13		eqcom	⊢ ( 𝑁 = ( 𝑘 · 𝑀 ) ↔ ( 𝑘 · 𝑀 ) = 𝑁 )
14	12 13	bitrdi	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 / 𝑀 ) = 𝑘 ↔ ( 𝑘 · 𝑀 ) = 𝑁 ) )
15	14	biimprd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 · 𝑀 ) = 𝑁 → ( 𝑁 / 𝑀 ) = 𝑘 ) )
16	15	impr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 𝑀 ) = 𝑁 ) ) → ( 𝑁 / 𝑀 ) = 𝑘 )
17		simprl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 𝑀 ) = 𝑁 ) ) → 𝑘 ∈ ℤ )
18	16 17	eqeltrd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 𝑀 ) = 𝑁 ) ) → ( 𝑁 / 𝑀 ) ∈ ℤ )
19	18	rexlimdvaa	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 → ( 𝑁 / 𝑀 ) ∈ ℤ ) )
20		simpr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 / 𝑀 ) ∈ ℤ ) → ( 𝑁 / 𝑀 ) ∈ ℤ )
21		simp2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → 𝑀 ≠ 0 )
22	4 9 21	divcan1d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 / 𝑀 ) · 𝑀 ) = 𝑁 )
23	22	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 / 𝑀 ) ∈ ℤ ) → ( ( 𝑁 / 𝑀 ) · 𝑀 ) = 𝑁 )
24		oveq1	⊢ ( 𝑘 = ( 𝑁 / 𝑀 ) → ( 𝑘 · 𝑀 ) = ( ( 𝑁 / 𝑀 ) · 𝑀 ) )
25	24	eqeq1d	⊢ ( 𝑘 = ( 𝑁 / 𝑀 ) → ( ( 𝑘 · 𝑀 ) = 𝑁 ↔ ( ( 𝑁 / 𝑀 ) · 𝑀 ) = 𝑁 ) )
26	25	rspcev	⊢ ( ( ( 𝑁 / 𝑀 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑀 ) · 𝑀 ) = 𝑁 ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 )
27	20 23 26	syl2anc	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 / 𝑀 ) ∈ ℤ ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 )
28	27	ex	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 / 𝑀 ) ∈ ℤ → ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 ) )
29	19 28	impbid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑀 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )
30	2 29	bitrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )