Nuprl Lemma : better-gcd-properties
∀a,b:ℤ.
((∃c:ℤ. ((c * better-gcd(a;b)) = a ∈ ℤ))
∧ (∃d:ℤ. ((d * better-gcd(a;b)) = b ∈ ℤ))
∧ (∃s,t:ℤ. (better-gcd(a;b) = ((s * a) + (t * b)) ∈ ℤ)))
Proof
Definitions occuring in Statement :
better-gcd: better-gcd(a;b),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
multiply: n * m,
add: n + m,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
gcd-properties,
better-gcd-gcd
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
sqequalRule,
isectElimination,
because_Cache,
intEquality
Latex:
\mforall{}a,b:\mBbbZ{}.
((\mexists{}c:\mBbbZ{}. ((c * better-gcd(a;b)) = a))
\mwedge{} (\mexists{}d:\mBbbZ{}. ((d * better-gcd(a;b)) = b))
\mwedge{} (\mexists{}s,t:\mBbbZ{}. (better-gcd(a;b) = ((s * a) + (t * b)))))
Date html generated:
2016_05_13-PM-04_04_16
Last ObjectModification:
2015_12_26-AM-10_55_36
Theory : int_1
Home
Index