Theorem gcdcomd 16533

Description: The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)

Hypotheses

Ref	Expression
gcdcomd.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
gcdcomd.n	⊢ (𝜑 → 𝑁 ∈ ℤ)

Assertion

Ref	Expression
gcdcomd	⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))

Proof of Theorem gcdcomd

Step	Hyp	Ref	Expression
1		gcdcomd.m	. 2 ⊢ (𝜑 → 𝑀 ∈ ℤ)
2		gcdcomd.n	. 2 ⊢ (𝜑 → 𝑁 ∈ ℤ)
3		gcdcom 16532	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7413  ℤcz 12596   gcd cgcd 16513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-mulcl 11199  ax-i2m1 11205  ax-pre-lttri 11211  ax-pre-lttrn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-po 5572  df-so 5573  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-sup 9464  df-pnf 11279  df-mnf 11280  df-ltxr 11282  df-gcd 16514

This theorem is referenced by:  modgcd  16551  rplpwr  16577  rprpwr  16578  coprmprod  16680  rpexp12i  16743  phiprmpw  16795  eulerthlem1  16800  eulerthlem2  16801  prmdiv  16804  coprimeprodsq  16828  pythagtriplem3  16838  prmpwdvds  16924  prmgaplem7  17077  gexexlem  19838  ablfacrp2  20055  pgpfac1lem2  20063  mpodvdsmulf1o  27173  dvdsmulf1o  27175  perfect1  27208  perfectlem1  27209  lgslem1  27277  lgsqrlem2  27327  lgsqr  27331  gausslemma2dlem0c  27338  lgsquad2lem2  27365  lgsquad2  27366  lgsquad3  27367  2sqlem8  27406  2sqmod  27416  nn0prpwlem  36282  aks4d1p8d2  42045  aks4d1p8d3  42046  hashscontpow1  42081  aks6d1c4  42084  aks5  42164  fltbccoprm  42614  flt4lem3  42621  flt4lem5c  42627  flt4lem5d  42628  flt4lem5e  42629  flt4lem5f  42630  flt4lem7  42632  nna4b4nsq  42633  jm2.19lem2  42965  jm2.20nn  42972  perfectALTVlem1  47666