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

Theorem dvdsval2 16140
Description: One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.)
Assertion
Ref Expression
dvdsval2 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ ๐‘ โ†” (๐‘ / ๐‘€) โˆˆ โ„ค))

Proof of Theorem dvdsval2
Dummy variable ๐‘˜ is distinct from all other variables.
StepHypRef Expression
1 divides 16139 . . 3 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ ๐‘ โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘€) = ๐‘))
213adant2 1132 . 2 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ ๐‘ โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘€) = ๐‘))
3 zcn 12505 . . . . . . . . . . 11 (๐‘ โˆˆ โ„ค โ†’ ๐‘ โˆˆ โ„‚)
433ad2ant3 1136 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ ๐‘ โˆˆ โ„‚)
54adantr 482 . . . . . . . . 9 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ๐‘ โˆˆ โ„‚)
6 zcn 12505 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„ค โ†’ ๐‘˜ โˆˆ โ„‚)
76adantl 483 . . . . . . . . 9 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ๐‘˜ โˆˆ โ„‚)
8 zcn 12505 . . . . . . . . . . 11 (๐‘€ โˆˆ โ„ค โ†’ ๐‘€ โˆˆ โ„‚)
983ad2ant1 1134 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ ๐‘€ โˆˆ โ„‚)
109adantr 482 . . . . . . . . 9 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ๐‘€ โˆˆ โ„‚)
11 simpl2 1193 . . . . . . . . 9 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ๐‘€ โ‰  0)
125, 7, 10, 11divmul3d 11966 . . . . . . . 8 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘ / ๐‘€) = ๐‘˜ โ†” ๐‘ = (๐‘˜ ยท ๐‘€)))
13 eqcom 2744 . . . . . . . 8 (๐‘ = (๐‘˜ ยท ๐‘€) โ†” (๐‘˜ ยท ๐‘€) = ๐‘)
1412, 13bitrdi 287 . . . . . . 7 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘ / ๐‘€) = ๐‘˜ โ†” (๐‘˜ ยท ๐‘€) = ๐‘))
1514biimprd 248 . . . . . 6 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘˜ ยท ๐‘€) = ๐‘ โ†’ (๐‘ / ๐‘€) = ๐‘˜))
1615impr 456 . . . . 5 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท ๐‘€) = ๐‘)) โ†’ (๐‘ / ๐‘€) = ๐‘˜)
17 simprl 770 . . . . 5 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท ๐‘€) = ๐‘)) โ†’ ๐‘˜ โˆˆ โ„ค)
1816, 17eqeltrd 2838 . . . 4 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท ๐‘€) = ๐‘)) โ†’ (๐‘ / ๐‘€) โˆˆ โ„ค)
1918rexlimdvaa 3154 . . 3 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘€) = ๐‘ โ†’ (๐‘ / ๐‘€) โˆˆ โ„ค))
20 simpr 486 . . . . 5 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง (๐‘ / ๐‘€) โˆˆ โ„ค) โ†’ (๐‘ / ๐‘€) โˆˆ โ„ค)
21 simp2 1138 . . . . . . 7 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ ๐‘€ โ‰  0)
224, 9, 21divcan1d 11933 . . . . . 6 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘ / ๐‘€) ยท ๐‘€) = ๐‘)
2322adantr 482 . . . . 5 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง (๐‘ / ๐‘€) โˆˆ โ„ค) โ†’ ((๐‘ / ๐‘€) ยท ๐‘€) = ๐‘)
24 oveq1 7365 . . . . . . 7 (๐‘˜ = (๐‘ / ๐‘€) โ†’ (๐‘˜ ยท ๐‘€) = ((๐‘ / ๐‘€) ยท ๐‘€))
2524eqeq1d 2739 . . . . . 6 (๐‘˜ = (๐‘ / ๐‘€) โ†’ ((๐‘˜ ยท ๐‘€) = ๐‘ โ†” ((๐‘ / ๐‘€) ยท ๐‘€) = ๐‘))
2625rspcev 3582 . . . . 5 (((๐‘ / ๐‘€) โˆˆ โ„ค โˆง ((๐‘ / ๐‘€) ยท ๐‘€) = ๐‘) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘€) = ๐‘)
2720, 23, 26syl2anc 585 . . . 4 (((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โˆง (๐‘ / ๐‘€) โˆˆ โ„ค) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘€) = ๐‘)
2827ex 414 . . 3 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘ / ๐‘€) โˆˆ โ„ค โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘€) = ๐‘))
2919, 28impbid 211 . 2 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘€) = ๐‘ โ†” (๐‘ / ๐‘€) โˆˆ โ„ค))
302, 29bitrd 279 1 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ ๐‘ โ†” (๐‘ / ๐‘€) โˆˆ โ„ค))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆƒwrex 3074   class class class wbr 5106  (class class class)co 7358  โ„‚cc 11050  0cc0 11052   ยท cmul 11057   / cdiv 11813  โ„คcz 12500   โˆฅ cdvds 16137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-z 12501  df-dvds 16138
This theorem is referenced by:  dvdsval3  16141  nndivdvds  16146  fsumdvds  16191  divconjdvds  16198  3dvds  16214  evend2  16240  oddp1d2  16241  fldivndvdslt  16297  bitsmod  16317  sadaddlem  16347  bitsuz  16355  divgcdz  16392  dvdsgcdidd  16419  mulgcd  16430  sqgcd  16442  lcmgcdlem  16483  mulgcddvds  16532  qredeu  16535  prmind2  16562  isprm5  16584  divgcdodd  16587  divnumden  16624  hashdvds  16648  hashgcdlem  16661  pythagtriplem19  16706  pcprendvds2  16714  pcpremul  16716  pc2dvds  16752  pcz  16754  dvdsprmpweqle  16759  pcadd  16762  pcmptdvds  16767  fldivp1  16770  pockthlem  16778  prmreclem1  16789  prmreclem3  16791  4sqlem8  16818  4sqlem9  16819  4sqlem12  16829  4sqlem14  16831  sylow1lem1  19381  sylow3lem4  19413  odadd1  19627  odadd2  19628  pgpfac1lem3  19857  prmirredlem  20896  znidomb  20971  root1eq1  26111  atantayl2  26291  efchtdvds  26511  muinv  26545  bposlem6  26640  lgseisenlem1  26726  lgsquad2lem1  26735  lgsquad3  26738  m1lgs  26739  2sqlem3  26771  2sqlem8  26777  qqhval2lem  32565  nn0prpwlem  34797  knoppndvlem8  34985  aks4d1p8d3  40546  aks4d1p8  40547  congrep  41300  jm2.22  41322  jm2.23  41323  proot1ex  41531  nzss  42604  etransclem9  44491  etransclem38  44520  etransclem44  44526  etransclem45  44527  divgcdoddALTV  45881  0dig2nn0o  46706
  Copyright terms: Public domain W3C validator