Nuprl Lemma : eqmod-test
∀m:ℤ. (((m - 1) * (m - 1)) ≡ 1 mod m)
Proof
Definitions occuring in Statement :
eqmod: a ≡ b mod m,
all: ∀x:A. B[x],
multiply: n * m,
subtract: n - m,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
subtract: n - m
Lemmas referenced :
subtract_wf,
eqmod-zero,
eqmod_functionality_wrt_eqmod,
multiply_functionality_wrt_eqmod,
subtract_functionality_wrt_eqmod,
eqmod_weakening
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
intEquality,
hypothesisEquality,
because_Cache,
multiplyEquality,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
natural_numberEquality,
hypothesis,
dependent_functionElimination,
independent_isectElimination,
independent_functionElimination,
productElimination,
sqequalRule
Latex:
\mforall{}m:\mBbbZ{}. (((m - 1) * (m - 1)) \mequiv{} 1 mod m)
Date html generated:
2016_05_15-PM-06_02_36
Last ObjectModification:
2015_12_27-PM-00_18_16
Theory : general
Home
Index