Theorem gcdcomd 16446

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 16445	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7361  ℤcz 12493   gcd cgcd 16426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7683  ax-resscn 11088  ax-1cn 11089  ax-icn 11090  ax-addcl 11091  ax-mulcl 11093  ax-i2m1 11099  ax-pre-lttri 11105  ax-pre-lttrn 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3351  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-sup 9350  df-pnf 11173  df-mnf 11174  df-ltxr 11176  df-gcd 16427

This theorem is referenced by:  modgcd  16464  rplpwr  16490  rprpwr  16491  coprmprod  16593  rpexp12i  16656  phiprmpw  16708  eulerthlem1  16713  eulerthlem2  16714  prmdiv  16717  coprimeprodsq  16741  pythagtriplem3  16751  prmpwdvds  16837  prmgaplem7  16990  gexexlem  19786  ablfacrp2  20003  pgpfac1lem2  20011  mpodvdsmulf1o  27165  dvdsmulf1o  27167  perfect1  27200  perfectlem1  27201  lgslem1  27269  lgsqrlem2  27319  lgsqr  27323  gausslemma2dlem0c  27330  lgsquad2lem2  27357  lgsquad2  27358  lgsquad3  27359  2sqlem8  27398  2sqmod  27408  nn0prpwlem  36529  aks4d1p8d2  42418  aks4d1p8d3  42419  hashscontpow1  42454  aks6d1c4  42457  aks5  42537  fltbccoprm  42962  flt4lem3  42969  flt4lem5c  42975  flt4lem5d  42976  flt4lem5e  42977  flt4lem5f  42978  flt4lem7  42980  nna4b4nsq  42981  jm2.19lem2  43310  jm2.20nn  43317  perfectALTVlem1  48044