### Nuprl Lemma : eqmod_functionality_wrt_eqmod

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

Proof

Definitions occuring in Statement :  eqmod: `a ≡ b mod m` uimplies: `b supposing a` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` prop: `ℙ` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` subtype_rel: `A ⊆r B`
Lemmas referenced :  eqmod_wf equal-wf-base int_subtype_base eqmod_inversion eqmod_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation Error :isect_memberFormation_alt,  cut introduction axiomEquality hypothesis thin rename independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality Error :universeIsType,  intEquality applyEquality sqequalRule equalitySymmetry hyp_replacement applyLambdaEquality dependent_functionElimination independent_functionElimination because_Cache

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

Date html generated: 2019_06_20-PM-02_24_18
Last ObjectModification: 2018_09_26-PM-05_58_20

Theory : num_thy_1

Home Index