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

Theorem gcdcom 15073
 Description: The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
Assertion
Ref Expression
gcdcom ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))

Proof of Theorem gcdcom
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 ancom 465 . . 3 ((𝑀 = 0 ∧ 𝑁 = 0) ↔ (𝑁 = 0 ∧ 𝑀 = 0))
2 ancom 465 . . . . . 6 ((𝑛𝑀𝑛𝑁) ↔ (𝑛𝑁𝑛𝑀))
32a1i 11 . . . . 5 (𝑛 ∈ ℤ → ((𝑛𝑀𝑛𝑁) ↔ (𝑛𝑁𝑛𝑀)))
43rabbiia 3161 . . . 4 {𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)} = {𝑛 ∈ ℤ ∣ (𝑛𝑁𝑛𝑀)}
54supeq1i 8236 . . 3 sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < ) = sup({𝑛 ∈ ℤ ∣ (𝑛𝑁𝑛𝑀)}, ℝ, < )
61, 5ifbieq2i 4060 . 2 if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )) = if((𝑁 = 0 ∧ 𝑀 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑁𝑛𝑀)}, ℝ, < ))
7 gcdval 15056 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )))
8 gcdval 15056 . . 3 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd 𝑀) = if((𝑁 = 0 ∧ 𝑀 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑁𝑛𝑀)}, ℝ, < )))
98ancoms 468 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 gcd 𝑀) = if((𝑁 = 0 ∧ 𝑀 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑁𝑛𝑀)}, ℝ, < )))
106, 7, 93eqtr4a 2670 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {crab 2900  ifcif 4036   class class class wbr 4583  (class class class)co 6549  supcsup 8229  ℝcr 9814  0cc0 9815   < clt 9953  ℤcz 11254   ∥ cdvds 14821   gcd cgcd 15054 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-i2m1 9883  ax-pre-lttri 9889  ax-pre-lttrn 9890 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-pnf 9955  df-mnf 9956  df-ltxr 9958  df-gcd 15055 This theorem is referenced by:  divgcdnnr  15075  gcdid0  15079  neggcd  15082  gcdabs2  15090  modgcd  15091  1gcd  15092  6gcd4e2  15093  rplpwr  15114  rppwr  15115  eucalginv  15135  3lcm2e6woprm  15166  coprmdvds  15204  qredeq  15209  coprmprod  15213  divgcdcoprmex  15218  cncongr1  15219  rpexp12i  15272  cncongrprm  15275  phiprmpw  15319  eulerthlem1  15324  eulerthlem2  15325  fermltl  15327  prmdiv  15328  vfermltl  15344  coprimeprodsq  15351  coprimeprodsq2  15352  pythagtriplem3  15361  pythagtrip  15377  pcgcd  15420  prmpwdvds  15446  pockthlem  15447  prmgaplem7  15599  gcdi  15615  gcdmodi  15616  1259lem5  15680  2503lem3  15684  4001lem4  15689  odinv  17801  gexexlem  18078  ablfacrp2  18289  pgpfac1lem2  18297  dvdsmulf1o  24720  perfect1  24753  perfectlem1  24754  lgslem1  24822  lgsprme0  24864  lgsdirnn0  24869  lgsqrlem2  24872  lgsqr  24876  gausslemma2dlem0c  24883  lgsquad2lem2  24910  lgsquad2  24911  lgsquad3  24912  2sqlem8  24951  ex-gcd  26706  2sqmod  28979  gcd32  30890  nn0prpwlem  31487  jm2.19lem2  36575  jm2.20nn  36582  goldbachthlem2  39996  goldbachth  39997  perfectALTVlem1  40164
 Copyright terms: Public domain W3C validator