Nuprl Lemma : eqmod-eqmod-div

`∀m,m',a,a',b,b':ℤ.  ((m' | m) `` (a ≡ a' mod m) `` (b ≡ b' mod m) `` (a ≡ b mod m' `⇐⇒` a' ≡ b' mod m'))`

Proof

Definitions occuring in Statement :  eqmod: `a ≡ b mod m` divides: `b | a` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` eqmod: `a ≡ b mod m` divides: `b | a` exists: `∃x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` sq_type: `SQType(T)` guard: `{T}` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` top: `Top`
Lemmas referenced :  subtype_base_sq int_subtype_base equal_wf squash_wf true_wf mul_assoc iff_weakening_equal eqmod_wf divides_wf subtract_wf decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermSubtract_wf itermVar_wf itermMultiply_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_term_value_mul_lemma int_term_value_add_lemma int_formula_prop_wf equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation sqequalHypSubstitution productElimination thin promote_hyp cut instantiate introduction extract_by_obid isectElimination cumulativity intEquality independent_isectElimination hypothesis dependent_functionElimination hypothesisEquality equalityTransitivity equalitySymmetry independent_functionElimination applyEquality lambdaEquality imageElimination universeEquality because_Cache natural_numberEquality sqequalRule imageMemberEquality baseClosed dependent_pairFormation addEquality multiplyEquality unionElimination int_eqEquality isect_memberEquality voidElimination voidEquality computeAll baseApply closedConclusion

Latex:
\mforall{}m,m',a,a',b,b':\mBbbZ{}.
((m'  |  m)  {}\mRightarrow{}  (a  \mequiv{}  a'  mod  m)  {}\mRightarrow{}  (b  \mequiv{}  b'  mod  m)  {}\mRightarrow{}  (a  \mequiv{}  b  mod  m'  \mLeftarrow{}{}\mRightarrow{}  a'  \mequiv{}  b'  mod  m'))

Date html generated: 2017_04_17-AM-09_42_49
Last ObjectModification: 2017_02_27-PM-05_37_40

Theory : num_thy_1

Home Index