Nuprl Lemma : less-trichotomy

a,b:ℤ.  (a < b ∨ b < a ∨ (a b ∈ ℤ))


Proof




Definitions occuring in Statement :  less_than: a < b all: x:A. B[x] or: P ∨ Q int: equal: t ∈ T
Definitions unfolded in proof :  member: t ∈ T all: x:A. B[x] subtype_rel: A ⊆B prop: squash: T true: True cand: c∧ B and: P ∧ Q less_than: a < b or: P ∨ Q less_than': less_than'(a;b) uall: [x:A]. B[x] guard: {T}
Lemmas referenced :  int_subtype_base equal-wf-base less_than_wf or_wf
Rules used in proof :  intEquality hypothesisEquality lessCases lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution applyEquality extract_by_obid imageMemberEquality sqequalRule introduction independent_pairFormation natural_numberEquality inlFormation baseClosed thin isectElimination sqequalHypSubstitution hypothesis cut inrFormation because_Cache lessTrichotomy

Latex:
\mforall{}a,b:\mBbbZ{}.    (a  <  b  \mvee{}  b  <  a  \mvee{}  (a  =  b))



Date html generated: 2019_06_20-AM-11_19_46
Last ObjectModification: 2019_01_27-PM-05_50_26

Theory : sqequal_1


Home Index