MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  divides Structured version   Visualization version   GIF version

Theorem divides 16292
Description: Define the divides relation. 𝑀𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 30475). As proven in dvdsval3 16294, 𝑀𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 16292 and dvdsval2 16293 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.
StepHypRef Expression
1 df-br 5144 . . 3 (𝑀𝑁 ↔ ⟨𝑀, 𝑁⟩ ∈ ∥ )
2 df-dvds 16291 . . . 4 ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
32eleq2i 2833 . . 3 (⟨𝑀, 𝑁⟩ ∈ ∥ ↔ ⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)})
41, 3bitri 275 . 2 (𝑀𝑁 ↔ ⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)})
5 oveq2 7439 . . . . 5 (𝑥 = 𝑀 → (𝑛 · 𝑥) = (𝑛 · 𝑀))
65eqeq1d 2739 . . . 4 (𝑥 = 𝑀 → ((𝑛 · 𝑥) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑦))
76rexbidv 3179 . . 3 (𝑥 = 𝑀 → (∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦))
8 eqeq2 2749 . . . 4 (𝑦 = 𝑁 → ((𝑛 · 𝑀) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑁))
98rexbidv 3179 . . 3 (𝑦 = 𝑁 → (∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
107, 9opelopab2 5546 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
114, 10bitrid 283 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wrex 3070  cop 4632   class class class wbr 5143  {copab 5205  (class class class)co 7431   · cmul 11160  cz 12613  cdvds 16290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-iota 6514  df-fv 6569  df-ov 7434  df-dvds 16291
This theorem is referenced by:  dvdsval2  16293  dvds0lem  16304  dvds1lem  16305  dvds2lem  16306  0dvds  16314  dvdsle  16347  divconjdvds  16352  dvdsexp2im  16364  odd2np1  16378  even2n  16379  oddm1even  16380  opeo  16402  omeo  16403  m1exp1  16413  divalglem4  16433  divalglem9  16438  divalgb  16441  modremain  16445  zeqzmulgcd  16547  bezoutlem4  16579  gcddiv  16588  dvdssqim  16591  dvdsexpim  16592  coprmdvds2  16691  congr  16701  divgcdcoprm0  16702  cncongr2  16705  dvdsnprmd  16727  prmpwdvds  16942  odmulg  19574  gexdvdsi  19601  lgsquadlem2  27425  primrootspoweq0  42107  aks6d1c2  42131  grpods  42195  unitscyglem4  42199  dvdsrabdioph  42821  jm2.26a  43012  coskpi2  45881  cosknegpi  45884  fourierswlem  46245  dfeven2  47636
  Copyright terms: Public domain W3C validator