Nuprl Lemma : gcd-reduce-ext

p,q:ℤ.  ∃g:ℕ. ∃a,b,x,y:ℤ((p (a g) ∈ ℤ) ∧ (q (b g) ∈ ℤ) ∧ (((x a) (y b)) 1 ∈ ℤ))


Proof




Definitions occuring in Statement :  nat: all: x:A. B[x] exists: x:A. B[x] and: P ∧ Q multiply: m add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  member: t ∈ T remainder: rem m divide: n ÷ m subtract: m so_apply: x[s1;s2] natrec: natrec genrec: genrec genrec-ap: genrec-ap spreadn: spread7 gcd-reduce decidable__equal_int decidable__int_equal uall: [x:A]. B[x] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2x.t[x] top: Top so_apply: x[s] uimplies: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: or: P ∨ Q squash: T so_lambda: λ2y.t[x; y]
Lemmas referenced :  gcd-reduce lifting-strict-int_eq istype-void strict4-decide lifting-strict-spread has-value_wf_base istype-base is-exception_wf decidable__equal_int decidable__int_equal
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed Error :isect_memberEquality_alt,  voidElimination independent_isectElimination independent_pairFormation Error :lambdaFormation_alt,  callbyvalueCallbyvalue callbyvalueReduce Error :universeIsType,  baseApply closedConclusion hypothesisEquality callbyvalueExceptionCases Error :inrFormation_alt,  imageMemberEquality imageElimination exceptionSqequal Error :inlFormation_alt,  Error :inhabitedIsType,  sqequalSqle divergentSqle callbyvalueSpread productElimination sqleReflexivity Error :equalityIstype,  dependent_functionElimination independent_functionElimination spreadExceptionCases axiomSqleEquality

Latex:
\mforall{}p,q:\mBbbZ{}.    \mexists{}g:\mBbbN{}.  \mexists{}a,b,x,y:\mBbbZ{}.  ((p  =  (a  *  g))  \mwedge{}  (q  =  (b  *  g))  \mwedge{}  (((x  *  a)  +  (y  *  b))  =  1))



Date html generated: 2019_06_20-PM-02_27_15
Last ObjectModification: 2019_03_10-PM-02_40_50

Theory : num_thy_1


Home Index