Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > divides | Structured version Visualization version GIF version |
Description: Define the divides relation. 𝑀 ∥ 𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 28563). As proven in dvdsval3 15843, 𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 15841 and dvdsval2 15842 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
Ref | Expression |
---|---|
divides | ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br 5068 | . . 3 ⊢ (𝑀 ∥ 𝑁 ↔ 〈𝑀, 𝑁〉 ∈ ∥ ) | |
2 | df-dvds 15840 | . . . 4 ⊢ ∥ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} | |
3 | 2 | eleq2i 2830 | . . 3 ⊢ (〈𝑀, 𝑁〉 ∈ ∥ ↔ 〈𝑀, 𝑁〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}) |
4 | 1, 3 | bitri 278 | . 2 ⊢ (𝑀 ∥ 𝑁 ↔ 〈𝑀, 𝑁〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}) |
5 | oveq2 7239 | . . . . 5 ⊢ (𝑥 = 𝑀 → (𝑛 · 𝑥) = (𝑛 · 𝑀)) | |
6 | 5 | eqeq1d 2740 | . . . 4 ⊢ (𝑥 = 𝑀 → ((𝑛 · 𝑥) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑦)) |
7 | 6 | rexbidv 3224 | . . 3 ⊢ (𝑥 = 𝑀 → (∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦)) |
8 | eqeq2 2750 | . . . 4 ⊢ (𝑦 = 𝑁 → ((𝑛 · 𝑀) = 𝑦 ↔ (𝑛 · 𝑀) = 𝑁)) | |
9 | 8 | rexbidv 3224 | . . 3 ⊢ (𝑦 = 𝑁 → (∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑦 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁)) |
10 | 7, 9 | opelopab2 5436 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (〈𝑀, 𝑁〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁)) |
11 | 4, 10 | syl5bb 286 | 1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2111 ∃wrex 3063 〈cop 4561 class class class wbr 5067 {copab 5129 (class class class)co 7231 · cmul 10758 ℤcz 12200 ∥ cdvds 15839 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-ext 2709 ax-sep 5206 ax-nul 5213 ax-pr 5336 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-rex 3068 df-rab 3071 df-v 3422 df-dif 3883 df-un 3885 df-in 3887 df-ss 3897 df-nul 4252 df-if 4454 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4834 df-br 5068 df-opab 5130 df-iota 6355 df-fv 6405 df-ov 7234 df-dvds 15840 |
This theorem is referenced by: dvdsval2 15842 dvds0lem 15852 dvds1lem 15853 dvds2lem 15854 0dvds 15862 dvdsle 15895 divconjdvds 15900 dvdsexp2im 15912 odd2np1 15926 even2n 15927 oddm1even 15928 opeo 15950 omeo 15951 m1exp1 15961 divalglem4 15981 divalglem9 15986 divalgb 15989 modremain 15993 zeqzmulgcd 16093 bezoutlem4 16126 gcddiv 16135 dvdssqim 16140 coprmdvds2 16235 congr 16245 divgcdcoprm0 16246 cncongr2 16249 dvdsnprmd 16271 prmpwdvds 16481 odmulg 18971 gexdvdsi 18996 lgsquadlem2 26286 dvdsexpim 40064 dvdsrabdioph 40363 jm2.26a 40553 coskpi2 43110 cosknegpi 43113 fourierswlem 43474 dfeven2 44802 |
Copyright terms: Public domain | W3C validator |