### Nuprl Lemma : multiply_functionality_wrt_eqmod

`∀m,a,a',b,b':ℤ.  ((a ≡ a' mod m) `` (b ≡ b' mod m) `` ((a * b) ≡ (a' * b') mod m))`

Proof

Definitions occuring in Statement :  eqmod: `a ≡ b mod m` all: `∀x:A. B[x]` implies: `P `` Q` multiply: `n * m` int: `ℤ`
Definitions unfolded in proof :  prop: `ℙ` uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` eqmod: `a ≡ b mod m` top: `Top` subtract: `n - m`
Rules used in proof :  Error :inhabitedIsType,  hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut Error :universeIsType,  Error :lambdaFormation_alt,  computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution because_Cache independent_functionElimination dependent_functionElimination multiplyEquality Error :isect_memberEquality_alt,  voidElimination minusEquality natural_numberEquality

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

Date html generated: 2019_06_20-PM-02_24_30
Last ObjectModification: 2019_01_15-PM-03_27_14

Theory : num_thy_1

Home Index