### Nuprl Lemma : gcd-properties

`∀a,b:ℤ.`
`  ((∃c:ℤ. ((c * gcd(a;b)) = a ∈ ℤ)) ∧ (∃d:ℤ. ((d * gcd(a;b)) = b ∈ ℤ)) ∧ (∃s,t:ℤ. (gcd(a;b) = ((s * a) + (t * b)) ∈ ℤ)))`

Proof

Definitions occuring in Statement :  gcd: `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]` int_seg: `{i..j-}` false: `False` lelt: `i ≤ j < k` and: `P ∧ Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` guard: `{T}` uimplies: `b supposing a` implies: `P `` Q` decidable: `Dec(P)` or: `P ∨ Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` less_than: `a < b` squash: `↓T` cand: `A c∧ B` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` sq_type: `SQType(T)` nat: `ℕ` prop: `ℙ` exists: `∃x:A. B[x]` sq_stable: `SqStable(P)` gcd: `gcd(a;b)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` ge: `i ≥ j ` nat_plus: `ℕ+`
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt thin sqequalHypSubstitution setElimination rename productElimination hypothesis introduction extract_by_obid isectElimination hypothesisEquality natural_numberEquality independent_isectElimination independent_functionElimination voidElimination universeIsType dependent_functionElimination unionElimination applyEquality sqequalRule instantiate because_Cache dependent_set_memberEquality_alt independent_pairFormation imageElimination equalityTransitivity equalitySymmetry addEquality minusEquality Error :memTop,  productIsType promote_hyp hypothesis_subsumption lambdaEquality_alt functionIsType functionEquality intEquality productEquality baseApply closedConclusion baseClosed setIsType inhabitedIsType imageMemberEquality multiplyEquality equalityElimination dependent_pairFormation_alt equalityIstype cumulativity sqequalBase universeEquality

Latex:
\mforall{}a,b:\mBbbZ{}.
((\mexists{}c:\mBbbZ{}.  ((c  *  gcd(a;b))  =  a))
\mwedge{}  (\mexists{}d:\mBbbZ{}.  ((d  *  gcd(a;b))  =  b))
\mwedge{}  (\mexists{}s,t:\mBbbZ{}.  (gcd(a;b)  =  ((s  *  a)  +  (t  *  b)))))

Date html generated: 2020_05_19-PM-09_36_09
Last ObjectModification: 2020_01_08-PM-04_39_18

Theory : int_1

Home Index