Nuprl Lemma : not-gt-2
∀x,y:ℤ. uiff(¬(y > x);y ≤ x)
Proof
Definitions occuring in Statement :
uiff: uiff(P;Q),
gt: i > j,
le: A ≤ B,
all: ∀x:A. B[x],
not: ¬A,
int: ℤ
Definitions unfolded in proof :
gt: i > j
Lemmas referenced :
not-lt-2
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}x,y:\mBbbZ{}. uiff(\mneg{}(y > x);y \mleq{} x)
Date html generated:
2016_05_13-PM-03_31_06
Last ObjectModification:
2015_12_26-AM-09_46_09
Theory : arithmetic
Home
Index