Theorem gcdcomd 16442

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℤcz 12489   gcd cgcd 16422

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 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-mulcl 11089  ax-i2m1 11095  ax-pre-lttri 11101  ax-pre-lttrn 11102

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 3063  df-rmo 3343  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-sup 9346  df-pnf 11169  df-mnf 11170  df-ltxr 11172  df-gcd 16423

This theorem is referenced by:  modgcd  16460  rplpwr  16486  rprpwr  16487  coprmprod  16589  rpexp12i  16652  phiprmpw  16704  eulerthlem1  16709  eulerthlem2  16710  prmdiv  16713  coprimeprodsq  16737  pythagtriplem3  16747  prmpwdvds  16833  prmgaplem7  16986  gexexlem  19785  ablfacrp2  20002  pgpfac1lem2  20010  mpodvdsmulf1o  27144  dvdsmulf1o  27146  perfect1  27179  perfectlem1  27180  lgslem1  27248  lgsqrlem2  27298  lgsqr  27302  gausslemma2dlem0c  27309  lgsquad2lem2  27336  lgsquad2  27337  lgsquad3  27338  2sqlem8  27377  2sqmod  27387  nn0prpwlem  36510  aks4d1p8d2  42516  aks4d1p8d3  42517  hashscontpow1  42552  aks6d1c4  42555  aks5  42635  fltbccoprm  43073  flt4lem3  43080  flt4lem5c  43086  flt4lem5d  43087  flt4lem5e  43088  flt4lem5f  43089  flt4lem7  43091  nna4b4nsq  43092  jm2.19lem2  43421  jm2.20nn  43428  perfectALTVlem1  48155