Theorem divides 16288

Description: Define the divides relation. 𝑀 ∥ 𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 30484). As proven in dvdsval3 16290, 𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 16288 and dvdsval2 16289 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.)

Assertion

Ref	Expression
divides	⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))

Distinct variable groups:   𝑛,𝑀   𝑛,𝑁

Proof of Theorem divides

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-br 5148	. . 3 ⊢ (𝑀 ∥ 𝑁 ↔ ⟨𝑀, 𝑁⟩ ∈ ∥ )
2		df-dvds 16287	. . . 4 ⊢ ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
3	2	eleq2i 2830	. . 3 ⊢ (⟨𝑀, 𝑁⟩ ∈ ∥ ↔ ⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)})
4	1, 3	bitri 275	. 2 ⊢ (𝑀 ∥ 𝑁 ↔ ⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)})
5		oveq2 7438	. . . . 5 ⊢ (𝑥 = 𝑀 → (𝑛 · 𝑥) = (𝑛 · 𝑀))
6	5	eqeq1d 2736	. . . 4 ⊢ (𝑥 = 𝑀 → ((𝑛 · 𝑥) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑦))
7	6	rexbidv 3176	. . 3 ⊢ (𝑥 = 𝑀 → (∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦))
8		eqeq2 2746	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝑛 · 𝑀) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑁))
9	8	rexbidv 3176	. . 3 ⊢ (𝑦 = 𝑁 → (∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
10	7, 9	opelopab2 5550	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
11	4, 10	bitrid 283	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∃wrex 3067  ⟨cop 4636   class class class wbr 5147  {copab 5209  (class class class)co 7430   · cmul 11157  ℤcz 12610   ∥ cdvds 16286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-iota 6515  df-fv 6570  df-ov 7433  df-dvds 16287

This theorem is referenced by:  dvdsval2  16289  dvds0lem  16300  dvds1lem  16301  dvds2lem  16302  0dvds  16310  dvdsle  16343  divconjdvds  16348  dvdsexp2im  16360  odd2np1  16374  even2n  16375  oddm1even  16376  opeo  16398  omeo  16399  m1exp1  16409  divalglem4  16429  divalglem9  16434  divalgb  16437  modremain  16441  zeqzmulgcd  16543  bezoutlem4  16575  gcddiv  16584  dvdssqim  16587  dvdsexpim  16588  coprmdvds2  16687  congr  16697  divgcdcoprm0  16698  cncongr2  16701  dvdsnprmd  16723  prmpwdvds  16937  odmulg  19588  gexdvdsi  19615  lgsquadlem2  27439  primrootspoweq0  42087  aks6d1c2  42111  grpods  42175  unitscyglem4  42179  dvdsrabdioph  42797  jm2.26a  42988  coskpi2  45821  cosknegpi  45824  fourierswlem  46185  dfeven2  47573