Metamath Proof Explorer


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 ∧ 𝑁 ∈ ℤ ) → ( 𝑀𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )