Nuprl Lemma : int-div-exception
∀[x:ℤ]. ∀[u,v:Top].  (x ÷ exception(u; v) ~ exception(u; v))
Proof
Definitions occuring in Statement : 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
divide: n ÷ m
, 
int: ℤ
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Lemmas referenced : 
top_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
Error :isect_memberFormation_alt, 
introduction, 
cut, 
exceptionDivide, 
hypothesisEquality, 
hypothesis, 
axiomSqEquality, 
Error :inhabitedIsType, 
sqequalRule, 
sqequalHypSubstitution, 
Error :isect_memberEquality_alt, 
isectElimination, 
thin, 
Error :isectIsTypeImplies, 
Error :universeIsType, 
extract_by_obid, 
intEquality
Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[u,v:Top].    (x  \mdiv{}  exception(u;  v)  \msim{}  exception(u;  v))
Date html generated:
2019_06_20-AM-11_21_59
Last ObjectModification:
2018_10_15-PM-03_22_12
Theory : arithmetic
Home
Index