Nuprl Lemma : qle-qabs

[q:ℚ]. (q ≤ |q|)


Proof




Definitions occuring in Statement :  qabs: |r| qle: r ≤ s rationals: uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q true: True subtype_rel: A ⊆B or: P ∨ Q uimplies: supposing a prop: squash: T guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q all: x:A. B[x]
Lemmas referenced :  qmax_ub iff_weakening_equal qabs-as-qmax true_wf squash_wf qle_wf qle_weakening_eq_qorder int-subtype-rationals qmul_wf rationals_wf qabs_wf qle_witness
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination because_Cache natural_numberEquality minusEquality applyEquality sqequalRule inlFormation independent_isectElimination lambdaEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed universeEquality productElimination dependent_functionElimination

Latex:
\mforall{}[q:\mBbbQ{}].  (q  \mleq{}  |q|)



Date html generated: 2016_05_15-PM-11_03_08
Last ObjectModification: 2016_01_16-PM-09_29_10

Theory : rationals


Home Index