### 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