Nuprl Lemma : int_mod_2_isect_int_mod_3
ℤ_2 ⋂ ℤ_3 ≡ ℤ_6
Proof
Definitions occuring in Statement :
int_mod: ℤ_n,
isect2: T1 ⋂ T2,
ext-eq: A ≡ B,
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
nat_plus: ℕ+,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True,
and: P ∧ Q,
prop: ℙ,
lcm: lcm(a;b),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
bfalse: ff,
gcd: gcd(a;b),
btrue: tt
Lemmas referenced :
less_than_wf,
int_mod_isect_int_mod
Rules used in proof :
cut,
lemma_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
dependent_set_memberEquality,
natural_numberEquality,
sqequalRule,
independent_pairFormation,
introduction,
imageMemberEquality,
hypothesisEquality,
baseClosed,
hypothesis,
because_Cache
Latex:
\mBbbZ{}\_2 \mcap{} \mBbbZ{}\_3 \mequiv{} \mBbbZ{}\_6
Date html generated:
2016_05_14-PM-09_27_44
Last ObjectModification:
2016_01_14-PM-11_31_17
Theory : num_thy_1
Home
Index