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

Theorem divides 14966
 Description: Define the divides relation. 𝑀 ∥ 𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 27283). As proven in dvdsval3 14968, 𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 14966 and dvdsval2 14967 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 4645 . . 3 (𝑀𝑁 ↔ ⟨𝑀, 𝑁⟩ ∈ ∥ )
2 df-dvds 14965 . . . 4 ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
32eleq2i 2691 . . 3 (⟨𝑀, 𝑁⟩ ∈ ∥ ↔ ⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)})
41, 3bitri 264 . 2 (𝑀𝑁 ↔ ⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)})
5 oveq2 6643 . . . . 5 (𝑥 = 𝑀 → (𝑛 · 𝑥) = (𝑛 · 𝑀))
65eqeq1d 2622 . . . 4 (𝑥 = 𝑀 → ((𝑛 · 𝑥) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑦))
76rexbidv 3048 . . 3 (𝑥 = 𝑀 → (∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦))
8 eqeq2 2631 . . . 4 (𝑦 = 𝑁 → ((𝑛 · 𝑀) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑁))
98rexbidv 3048 . . 3 (𝑦 = 𝑁 → (∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
107, 9opelopab2 4986 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (⟨𝑀, 𝑁⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
114, 10syl5bb 272 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1481   ∈ wcel 1988  ∃wrex 2910  ⟨cop 4174   class class class wbr 4644  {copab 4703  (class class class)co 6635   · cmul 9926  ℤcz 11362   ∥ cdvds 14964 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-iota 5839  df-fv 5884  df-ov 6638  df-dvds 14965 This theorem is referenced by:  dvdsval2  14967  dvds0lem  14973  dvds1lem  14974  dvds2lem  14975  0dvds  14983  dvdsle  15013  divconjdvds  15018  odd2np1  15046  even2n  15047  oddm1even  15048  opeo  15070  omeo  15071  m1exp1  15074  divalglem4  15100  divalglem9  15105  divalgb  15108  modremain  15113  zeqzmulgcd  15213  bezoutlem4  15240  gcddiv  15249  dvdssqim  15254  coprmdvds2  15349  congr  15359  divgcdcoprm0  15360  cncongr2  15363  dvdsnprmd  15384  prmpwdvds  15589  odmulg  17954  gexdvdsi  17979  lgsquadlem2  25087  dvdspw  31611  dvdsrabdioph  37193  jm2.26a  37386  coskpi2  39840  cosknegpi  39843  fourierswlem  40210  dfeven2  41327
 Copyright terms: Public domain W3C validator