Theorem divides 16186

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3061  ⟨cop 4587   class class class wbr 5099  {copab 5161  (class class class)co 7361   · cmul 11036  ℤcz 12493   ∥ cdvds 16184

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 5242  ax-nul 5252  ax-pr 5378

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-iota 6449  df-fv 6501  df-ov 7364  df-dvds 16185

This theorem is referenced by:  dvdsval2  16187  dvds0lem  16198  dvds1lem  16199  dvds2lem  16200  0dvds  16208  dvdsle  16242  divconjdvds  16247  dvdsexp2im  16259  odd2np1  16273  even2n  16274  oddm1even  16275  opeo  16297  omeo  16298  m1exp1  16308  divalglem4  16328  divalglem9  16333  divalgb  16336  modremain  16340  zeqzmulgcd  16442  bezoutlem4  16474  gcddiv  16483  dvdssqim  16486  dvdsexpim  16487  coprmdvds2  16586  congr  16596  divgcdcoprm0  16597  cncongr2  16600  dvdsnprmd  16622  prmpwdvds  16837  odmulg  19490  gexdvdsi  19517  lgsquadlem2  27353  primrootspoweq0  42439  aks6d1c2  42463  grpods  42527  unitscyglem4  42531  dvdsrabdioph  43130  jm2.26a  43320  coskpi2  46187  cosknegpi  46190  fourierswlem  46551  dfeven2  47972