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


Definitions occuring in Statement :  coprime: CoPrime(a,b) all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q multiply: m add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T uall: [x:A]. B[x] prop: rev_implies:  Q exists: x:A. B[x] subtype_rel: A ⊆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

\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