Step
*
of Lemma
gcd_functionality_wrt_eqmod
∀a,a',m:ℤ. ((a' ≡ a mod m)
⇒ (gcd(a';m) ~ gcd(a;m)))
BY
{ (Auto
THEN D -1
THEN (InstLemma `gcd_elim` [⌜a'⌝;⌜m⌝]⋅ THENA Auto)
THEN (InstLemma `gcd_elim` [⌜a⌝;⌜m⌝]⋅ THENA Auto)
THEN ExRepD
THEN ((HypSubst (-4) 0 THENA Auto) THEN Thin (-4))
THEN (HypSubst (-1) 0 THENA Auto)
THEN Thin (-1)
THEN D -3
THEN D -1
THEN ExRepD
THEN D 0
THEN BackThruSomeHyp
THEN Auto) }
1
1. a : ℤ
2. a' : ℤ
3. m : ℤ
4. c : ℤ
5. (a' - a) = (m * c) ∈ ℤ
6. y1 : ℤ
7. y1 | a'
8. y1 | m
9. ∀z:ℤ. (((z | a') ∧ (z | m))
⇒ (z | y1))
10. y : ℤ
11. y | a
12. y | m
13. ∀z:ℤ. (((z | a) ∧ (z | m))
⇒ (z | y))
⊢ y1 | a
2
1. a : ℤ
2. a' : ℤ
3. m : ℤ
4. c : ℤ
5. (a' - a) = (m * c) ∈ ℤ
6. y1 : ℤ
7. y1 | a'
8. y1 | m
9. ∀z:ℤ. (((z | a') ∧ (z | m))
⇒ (z | y1))
10. y : ℤ
11. y | a
12. y | m
13. ∀z:ℤ. (((z | a) ∧ (z | m))
⇒ (z | y))
⊢ y | a'
Latex:
Latex:
\mforall{}a,a',m:\mBbbZ{}. ((a' \mequiv{} a mod m) {}\mRightarrow{} (gcd(a';m) \msim{} gcd(a;m)))
By
Latex:
(Auto
THEN D -1
THEN (InstLemma `gcd\_elim` [\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma `gcd\_elim` [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{} THENA Auto)
THEN ExRepD
THEN ((HypSubst (-4) 0 THENA Auto) THEN Thin (-4))
THEN (HypSubst (-1) 0 THENA Auto)
THEN Thin (-1)
THEN D -3
THEN D -1
THEN ExRepD
THEN D 0
THEN BackThruSomeHyp
THEN Auto)
Home
Index