Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > gcdcomd | Structured version Visualization version GIF version |
Description: The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.) |
Ref | Expression |
---|---|
gcdcomd.m | ⊢ (𝜑 → 𝑀 ∈ ℤ) |
gcdcomd.n | ⊢ (𝜑 → 𝑁 ∈ ℤ) |
Ref | Expression |
---|---|
gcdcomd | ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gcdcomd.m | . 2 ⊢ (𝜑 → 𝑀 ∈ ℤ) | |
2 | gcdcomd.n | . 2 ⊢ (𝜑 → 𝑁 ∈ ℤ) | |
3 | gcdcom 15917 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) | |
4 | 1, 2, 3 | syl2anc 587 | 1 ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 (class class class)co 7155 ℤcz 12025 gcd cgcd 15898 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-sep 5172 ax-nul 5179 ax-pow 5237 ax-pr 5301 ax-un 7464 ax-resscn 10637 ax-1cn 10638 ax-icn 10639 ax-addcl 10640 ax-mulcl 10642 ax-i2m1 10648 ax-pre-lttri 10654 ax-pre-lttrn 10655 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4802 df-br 5036 df-opab 5098 df-mpt 5116 df-id 5433 df-po 5446 df-so 5447 df-xp 5533 df-rel 5534 df-cnv 5535 df-co 5536 df-dm 5537 df-rn 5538 df-res 5539 df-ima 5540 df-iota 6298 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-ov 7158 df-oprab 7159 df-mpo 7160 df-er 8304 df-en 8533 df-dom 8534 df-sdom 8535 df-sup 8944 df-pnf 10720 df-mnf 10721 df-ltxr 10723 df-gcd 15899 |
This theorem is referenced by: modgcd 15936 rplpwr 15963 rprpwr 15964 coprmprod 16062 rpexp12i 16125 phiprmpw 16173 eulerthlem1 16178 eulerthlem2 16179 prmdiv 16182 coprimeprodsq 16205 pythagtriplem3 16215 prmpwdvds 16300 prmgaplem7 16453 gexexlem 19045 ablfacrp2 19262 pgpfac1lem2 19270 dvdsmulf1o 25883 perfect1 25916 perfectlem1 25917 lgslem1 25985 lgsqrlem2 26035 lgsqr 26039 gausslemma2dlem0c 26046 lgsquad2lem2 26073 lgsquad2 26074 lgsquad3 26075 2sqlem8 26114 2sqmod 26124 nn0prpwlem 34086 fltbccoprm 39998 flt4lem3 40005 flt4lem5c 40011 flt4lem5d 40012 flt4lem5e 40013 flt4lem5f 40014 flt4lem7 40016 nna4b4nsq 40017 jm2.19lem2 40332 jm2.20nn 40339 perfectALTVlem1 44634 |
Copyright terms: Public domain | W3C validator |