Nuprl Lemma : divides-iff-gcd-assoced

x,y:ℤ.  (x ⇐⇒ gcd(x;y) x)


Proof




Definitions occuring in Statement :  assoced: b divides: a gcd: gcd(a;b) all: x:A. B[x] iff: ⇐⇒ Q int:
Definitions unfolded in proof :  all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] rev_implies:  Q uimplies: supposing a guard: {T} assoced: b
Lemmas referenced :  divides_wf assoced_wf gcd_wf divides-iff-gcd assoced_functionality_wrt_assoced gcd_sym assoced_weakening gcd_is_divisor_2 divides_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis dependent_functionElimination intEquality productElimination independent_functionElimination equalityTransitivity equalitySymmetry because_Cache independent_isectElimination

Latex:
\mforall{}x,y:\mBbbZ{}.    (x  |  y  \mLeftarrow{}{}\mRightarrow{}  gcd(x;y)  \msim{}  x)



Date html generated: 2018_05_21-PM-01_10_28
Last ObjectModification: 2018_01_28-PM-02_03_50

Theory : num_thy_1


Home Index