### Nuprl Lemma : chinese-remainder2-extract

`∀r,s,a,b:ℤ.  Dec(∃x:ℤ [((x ≡ a mod r) ∧ (x ≡ b mod s))])`

Proof

Definitions occuring in Statement :  eqmod: `a ≡ b mod m` decidable: `Dec(P)` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` and: `P ∧ Q` int: `ℤ`
Definitions unfolded in proof :  member: `t ∈ T` remainder: `n rem m` divide: `n ÷ m` subtract: `n - m` so_apply: `x[s1;s2]` natrec: natrec genrec: genrec sign: `sign(x)` ifthenelse: `if b then t else f fi ` le_int: `i ≤z j` bnot: `¬bb` lt_int: `i <z j` btrue: `tt` it: `⋅` bfalse: `ff` eq_int: `(i =z j)` genrec-ap: genrec-ap spreadn: spread7 chinese-remainder2 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 y.t[x; y]` top: `Top` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]` strict4: `strict4(F)` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ` or: `P ∨ Q` squash: `↓T`
Lemmas referenced :  chinese-remainder2 lifting-strict-spread istype-void strict4-spread lifting-strict-int_eq strict4-decide has-value_wf_base istype-base is-exception_wf istype-universe value-type-has-value int-value-type lifting-strict-decide lifting-strict-less gcd-reduce 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 isect_memberEquality_alt voidElimination independent_isectElimination independent_pairFormation lambdaFormation_alt callbyvalueCallbyvalue callbyvalueReduce universeIsType baseApply closedConclusion hypothesisEquality callbyvalueExceptionCases inrFormation_alt imageMemberEquality imageElimination exceptionSqequal inlFormation_alt inhabitedIsType sqequalSqle divergentSqle callbyvalueSpread productElimination sqleReflexivity equalityIstype dependent_functionElimination independent_functionElimination spreadExceptionCases axiomSqleEquality callbyvalueIntEq intEquality int_eqExceptionCases callbyvalueMultiply multiplyExceptionCases because_Cache

Latex:
\mforall{}r,s,a,b:\mBbbZ{}.    Dec(\mexists{}x:\mBbbZ{}  [((x  \mequiv{}  a  mod  r)  \mwedge{}  (x  \mequiv{}  b  mod  s))])

Date html generated: 2019_10_15-AM-11_16_52
Last ObjectModification: 2019_06_26-PM-03_39_28

Theory : general

Home Index