---

Step * of Lemma gcd-exp

∀x,y:ℤ. ∀n:ℕ.  (gcd(x^n;y^n) ~ gcd(x;y)^n)
BY
{ (Auto
   THEN (InstLemma `gcd_unique` [⌜x^n⌝; ⌜y^n⌝; ⌜gcd(x^n;y^n)⌝; ⌜gcd(x;y)^n⌝])⋅
   THEN Auto
   THEN Try ((BLemma `gcd_sat_pred` THEN Auto))
   THEN D 0
   THEN Auto
   THEN Try ((BLemma `exp-divides`
              THEN Auto
              THEN ((BLemma `gcd_is_divisor_1` THENA Auto) ORELSE (BLemma `gcd_is_divisor_2` THENA Auto))))) }

1
1. x : ℤ@i
2. y : ℤ@i
3. n : ℕ@i
4. gcd(x;y)^n | y^n
5. z : ℤ@i
6. z | x^n@i
7. z | y^n@i
⊢ z | gcd(x;y)^n

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.  \mforall{}n:\mBbbN{}.    (gcd(x\^{}n;y\^{}n)  \msim{}  gcd(x;y)\^{}n)


By

---

Latex:
(Auto
  THEN  (InstLemma  `gcd\_unique`  [\mkleeneopen{}x\^{}n\mkleeneclose{};  \mkleeneopen{}y\^{}n\mkleeneclose{};  \mkleeneopen{}gcd(x\^{}n;y\^{}n)\mkleeneclose{};  \mkleeneopen{}gcd(x;y)\^{}n\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  Try  ((BLemma  `gcd\_sat\_pred`  THEN  Auto))
  THEN  D  0
  THEN  Auto
  THEN  Try  ((BLemma  `exp-divides`
                        THEN  Auto
                        THEN  ((BLemma  `gcd\_is\_divisor\_1`  THENA  Auto)
                        ORELSE  (BLemma  `gcd\_is\_divisor\_2`  THENA  Auto)
                        ))))

---

Home Index