### Nuprl Lemma : coprime_bezout_id

`∀a,b:ℤ.  (CoPrime(a,b) `⇐⇒` ∃x,y:ℤ. (((a * x) + (b * y)) = 1 ∈ ℤ))`

This theorem is one of freek's list of 100 theorems

Proof

Definitions occuring in Statement :  coprime: `CoPrime(a,b)` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` multiply: `n * m` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` rev_implies: `P `` Q` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B`
Lemmas referenced :  coprime_bezout_id1 coprime_wf coprime_bezout_id2 int_subtype_base istype-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis Error :universeIsType,  isectElimination sqequalRule Error :productIsType,  Error :inhabitedIsType,  Error :equalityIsType4,  addEquality multiplyEquality applyEquality natural_numberEquality

Latex:
\mforall{}a,b:\mBbbZ{}.    (CoPrime(a,b)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x,y:\mBbbZ{}.  (((a  *  x)  +  (b  *  y))  =  1))

Date html generated: 2019_06_20-PM-02_23_40
Last ObjectModification: 2018_10_03-AM-00_12_35

Theory : num_thy_1

Home Index