Nuprl Lemma : gcd_is_divisor_1

a,b:ℤ.  (gcd(a;b) a)


Proof




Definitions occuring in Statement :  divides: a gcd: gcd(a;b) all: x:A. B[x] int:
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T implies:  Q prop: uall: [x:A]. B[x] gcd_p: GCD(a;b;y) and: P ∧ Q
Lemmas referenced :  istype-int gcd_wf gcd_sat_pred gcd_p_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  Error :inhabitedIsType,  hypothesisEquality cut introduction extract_by_obid hypothesis sqequalHypSubstitution dependent_functionElimination thin equalitySymmetry hyp_replacement applyLambdaEquality isectElimination Error :equalityIsType1,  equalityTransitivity independent_functionElimination productElimination

Latex:
\mforall{}a,b:\mBbbZ{}.    (gcd(a;b)  |  a)



Date html generated: 2019_06_20-PM-02_22_04
Last ObjectModification: 2018_10_03-AM-00_12_14

Theory : num_thy_1


Home Index