Nuprl Lemma : sq_stable__eqmod

m,a,b:ℤ.  SqStable(a ≡ mod m)


Proof




Definitions occuring in Statement :  eqmod: a ≡ mod m sq_stable: SqStable(P) all: x:A. B[x] int:
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T implies:  Q
Lemmas referenced :  sq_stable_from_decidable eqmod_wf decidable__eqmod
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination dependent_functionElimination intEquality

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



Date html generated: 2016_05_14-PM-04_21_35
Last ObjectModification: 2015_12_26-PM-08_17_43

Theory : num_thy_1


Home Index