ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  divides GIF version

Theorem divides 11798
Description: Define the divides relation. ๐‘€ โˆฅ ๐‘ means ๐‘€ divides into ๐‘ with no remainder. For example, 3 โˆฅ 6 (ex-dvds 14567). As proven in dvdsval3 11800, ๐‘€ โˆฅ ๐‘ โ†” (๐‘ mod ๐‘€) = 0. See divides 11798 and dvdsval2 11799 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 4006 . . 3 (๐‘€ โˆฅ ๐‘ โ†” โŸจ๐‘€, ๐‘โŸฉ โˆˆ โˆฅ )
2 df-dvds 11797 . . . 4 โˆฅ = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ)}
32eleq2i 2244 . . 3 (โŸจ๐‘€, ๐‘โŸฉ โˆˆ โˆฅ โ†” โŸจ๐‘€, ๐‘โŸฉ โˆˆ {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ)})
41, 3bitri 184 . 2 (๐‘€ โˆฅ ๐‘ โ†” โŸจ๐‘€, ๐‘โŸฉ โˆˆ {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ)})
5 oveq2 5885 . . . . 5 (๐‘ฅ = ๐‘€ โ†’ (๐‘› ยท ๐‘ฅ) = (๐‘› ยท ๐‘€))
65eqeq1d 2186 . . . 4 (๐‘ฅ = ๐‘€ โ†’ ((๐‘› ยท ๐‘ฅ) = ๐‘ฆ โ†” (๐‘› ยท ๐‘€) = ๐‘ฆ))
76rexbidv 2478 . . 3 (๐‘ฅ = ๐‘€ โ†’ (โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ โ†” โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘ฆ))
8 eqeq2 2187 . . . 4 (๐‘ฆ = ๐‘ โ†’ ((๐‘› ยท ๐‘€) = ๐‘ฆ โ†” (๐‘› ยท ๐‘€) = ๐‘))
98rexbidv 2478 . . 3 (๐‘ฆ = ๐‘ โ†’ (โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘ฆ โ†” โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘))
107, 9opelopab2 4272 . 2 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (โŸจ๐‘€, ๐‘โŸฉ โˆˆ {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ)} โ†” โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘))
114, 10bitrid 192 1 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ ๐‘ โ†” โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   = wceq 1353   โˆˆ wcel 2148  โˆƒwrex 2456  โŸจcop 3597   class class class wbr 4005  {copab 4065  (class class class)co 5877   ยท cmul 7818  โ„คcz 9255   โˆฅ cdvds 11796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-iota 5180  df-fv 5226  df-ov 5880  df-dvds 11797
This theorem is referenced by:  dvdsval2  11799  dvds0lem  11810  dvds1lem  11811  dvds2lem  11812  0dvds  11820  dvdsle  11852  divconjdvds  11857  odd2np1  11880  even2n  11881  oddm1even  11882  opeo  11904  omeo  11905  m1exp1  11908  divalgb  11932  modremain  11936  zeqzmulgcd  11973  gcddiv  12022  dvdssqim  12027  coprmdvds2  12095  congr  12102  divgcdcoprm0  12103  cncongr2  12106  dvdsnprmd  12127  prmpwdvds  12355
  Copyright terms: Public domain W3C validator