Nuprl Lemma : bnot_of_le_int
∀[i,j:ℤ].  ¬bi ≤z j = j <z i
Proof
Definitions occuring in Statement : 
le_int: i ≤z j
, 
bnot: ¬bb
, 
lt_int: i <z j
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
int: ℤ
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
le_int: i ≤z j
Lemmas referenced : 
bnot_bnot_elim, 
lt_int_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
Error :isect_memberFormation_alt, 
introduction, 
cut, 
hypothesis, 
Error :inhabitedIsType, 
hypothesisEquality, 
sqequalRule, 
sqequalHypSubstitution, 
isect_memberEquality, 
isectElimination, 
thin, 
axiomEquality, 
intEquality, 
Error :universeIsType, 
lemma_by_obid
Latex:
\mforall{}[i,j:\mBbbZ{}].    \mneg{}\msubb{}i  \mleq{}z  j  =  j  <z  i
Date html generated:
2019_06_20-AM-11_31_07
Last ObjectModification:
2018_09_26-AM-11_14_54
Theory : bool_1
Home
Index