Nuprl Lemma : chrem_exists
∀r,s:ℕ+. (CoPrime(r,s) ⇒ (∀a,b:ℤ. ∃x:ℤ. ((x ≡ a mod r) ∧ (x ≡ b mod s))))
Proof
Definitions occuring in Statement :
eqmod: a ≡ b mod m,
coprime: CoPrime(a,b),
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
int: ℤ
Definitions unfolded in proof :
prop: ℙ,
nat_plus: ℕ+,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x],
coprime: CoPrime(a,b),
exists: ∃x:A. B[x],
and: P ∧ Q,
top: Top,
uimplies: b supposing a,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
nat_plus_wf,
coprime_wf,
istype-int,
chrem_exists_aux,
gcd_p_sym,
eqmod_wf,
istype-void,
mul-commutes,
one-mul,
zero-mul,
add-zero,
eqmod_functionality_wrt_eqmod,
add_functionality_wrt_eqmod,
multiply_functionality_wrt_eqmod,
eqmod_weakening,
zero-add
Rules used in proof :
rename,
setElimination,
thin,
isectElimination,
sqequalHypSubstitution,
Error :universeIsType,
hypothesis,
extract_by_obid,
introduction,
cut,
hypothesisEquality,
Error :inhabitedIsType,
Error :lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
because_Cache,
independent_functionElimination,
dependent_functionElimination,
natural_numberEquality,
productElimination,
Error :dependent_pairFormation_alt,
addEquality,
multiplyEquality,
independent_pairFormation,
sqequalRule,
Error :productIsType,
Error :isect_memberEquality_alt,
voidElimination,
independent_isectElimination
Latex:
\mforall{}r,s:\mBbbN{}\msupplus{}. (CoPrime(r,s) {}\mRightarrow{} (\mforall{}a,b:\mBbbZ{}. \mexists{}x:\mBbbZ{}. ((x \mequiv{} a mod r) \mwedge{} (x \mequiv{} b mod s))))
Date html generated:
2019_06_20-PM-02_25_01
Last ObjectModification:
2019_01_17-AM-09_14_04
Theory : num_thy_1
Home
Index