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