---

Step * of Lemma gcd-exp

∀x,y:ℤ. ∀n:ℕ.  (gcd(x^n;y^n) ~ gcd(x;y)^n)
BY
{ TACTIC:(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 : ℤ
2. y : ℤ
3. n : ℕ
4. gcd(x;y)^n | y^n
5. z : ℤ
6. z | x^n
7. z | y^n
⊢ 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:
TACTIC:(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