Theorem divides 16212

Description: Define the divides relation. 𝑀 ∥ 𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 30546). As proven in dvdsval3 16214, 𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 16212 and dvdsval2 16213 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 5087	. . 3 ⊢ (𝑀 ∥ 𝑁 ↔ ⟨𝑀, 𝑁⟩ ∈ ∥ )
2		df-dvds 16211	. . . 4 ⊢ ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
3	2	eleq2i 2829	. . 3 ⊢ (⟨𝑀, 𝑁⟩ ∈ ∥ ↔ ⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)})
4	1, 3	bitri 275	. 2 ⊢ (𝑀 ∥ 𝑁 ↔ ⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)})
5		oveq2 7366	. . . . 5 ⊢ (𝑥 = 𝑀 → (𝑛 · 𝑥) = (𝑛 · 𝑀))
6	5	eqeq1d 2739	. . . 4 ⊢ (𝑥 = 𝑀 → ((𝑛 · 𝑥) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑦))
7	6	rexbidv 3162	. . 3 ⊢ (𝑥 = 𝑀 → (∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦))
8		eqeq2 2749	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝑛 · 𝑀) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑁))
9	8	rexbidv 3162	. . 3 ⊢ (𝑦 = 𝑁 → (∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
10	7, 9	opelopab2 5487	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
11	4, 10	bitrid 283	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  ⟨cop 4574   class class class wbr 5086  {copab 5148  (class class class)co 7358   · cmul 11032  ℤcz 12513   ∥ cdvds 16210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-iota 6446  df-fv 6498  df-ov 7361  df-dvds 16211

This theorem is referenced by:  dvdsval2  16213  dvds0lem  16224  dvds1lem  16225  dvds2lem  16226  0dvds  16234  dvdsle  16268  divconjdvds  16273  dvdsexp2im  16285  odd2np1  16299  even2n  16300  oddm1even  16301  opeo  16323  omeo  16324  m1exp1  16334  divalglem4  16354  divalglem9  16359  divalgb  16362  modremain  16366  zeqzmulgcd  16468  bezoutlem4  16500  gcddiv  16509  dvdssqim  16512  dvdsexpim  16513  coprmdvds2  16612  congr  16622  divgcdcoprm0  16623  cncongr2  16626  dvdsnprmd  16648  prmpwdvds  16864  odmulg  19520  gexdvdsi  19547  lgsquadlem2  27363  primrootspoweq0  42556  aks6d1c2  42580  grpods  42644  unitscyglem4  42648  dvdsrabdioph  43253  jm2.26a  43443  coskpi2  46309  cosknegpi  46312  fourierswlem  46673  ppivalnnprm  48085  ppivalnnnprmge6  48086  dfeven2  48122