Nuprl Lemma : bnot_of_lt_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 : 
le_int_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
Error :isect_memberFormation_alt, 
introduction, 
cut, 
sqequalRule, 
hypothesis, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
Error :inhabitedIsType, 
isect_memberEquality, 
axiomEquality, 
intEquality, 
Error :universeIsType
Latex:
\mforall{}[i,j:\mBbbZ{}].    \mneg{}\msubb{}i  <z  j  =  j  \mleq{}z  i
Date html generated:
2019_06_20-AM-11_31_08
Last ObjectModification:
2018_09_26-AM-11_29_28
Theory : bool_1
Home
Index