Nuprl Lemma : int_mod_2_union_int_mod_3

_2 ⋃ ℤ_3 ≡ ⇃(ℤ)


Proof




Definitions occuring in Statement :  int_mod: _n quotient: x,y:A//B[x; y] b-union: A ⋃ B ext-eq: A ≡ B true: True natural_number: $n int:
Definitions unfolded in proof :  equiv_rel: EquivRel(T;x,y.E[x; y]) and: P ∧ Q refl: Refl(T;x,y.E[x; y]) all: x:A. B[x] true: True member: t ∈ T cand: c∧ B sym: Sym(T;x,y.E[x; y]) implies:  Q prop: trans: Trans(T;x,y.E[x; y]) uall: [x:A]. B[x] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) gcd: gcd(a;b) ifthenelse: if then else fi  eq_int: (i =z j) bfalse: ff btrue: tt ext-eq: A ≡ B subtype_rel: A ⊆B int_mod: _n quotient: x,y:A//B[x; y] eqmod: a ≡ mod m
Lemmas referenced :  subtract_wf one_divs_any eqmod_equiv_rel eqmod_wf equal-wf-base quotient-member-eq less_than_wf int_mod_union_int_mod quotient_wf int_mod_wf b-union_wf ext-eq_transitivity true_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation lambdaFormation natural_numberEquality intEquality lemma_by_obid hypothesis because_Cache sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality independent_isectElimination dependent_set_memberEquality introduction imageMemberEquality hypothesisEquality baseClosed pointwiseFunctionalityForEquality pertypeElimination productElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination productEquality

Latex:
\mBbbZ{}\_2  \mcup{}  \mBbbZ{}\_3  \mequiv{}  \00D9(\mBbbZ{})



Date html generated: 2016_05_14-PM-09_27_40
Last ObjectModification: 2016_01_14-PM-11_33_03

Theory : num_thy_1


Home Index