Nuprl Lemma : qavg-qless-iff-1

[a,b:ℚ].  uiff(qavg(a;b) < b;a < b)


Proof




Definitions occuring in Statement :  qavg: qavg(a;b) qless: r < s rationals: uiff: uiff(P;Q) uall: [x:A]. B[x]
Definitions unfolded in proof :  qavg: qavg(a;b) uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a implies:  Q subtype_rel: A ⊆B not: ¬A qeq: qeq(r;s) callbyvalueall: callbyvalueall evalall: evalall(t) ifthenelse: if then else fi  btrue: tt eq_int: (i =z j) bfalse: ff assert: b false: False prop: qless: r < s grp_lt: a < b set_lt: a <b set_blt: a <b b band: p ∧b q infix_ap: y set_le: b pi2: snd(t) oset_of_ocmon: g↓oset dset_of_mon: g↓set grp_le: b pi1: fst(t) qadd_grp: <ℚ+> q_le: q_le(r;s) bor: p ∨bq qpositive: qpositive(r) qsub: s qadd: s qmul: s lt_int: i <j bnot: ¬bb true: True squash: T guard: {T} iff: ⇐⇒ Q rev_uimplies: rev_uimplies(P;Q) rev_implies:  Q
Lemmas referenced :  qless_witness qless_wf qdiv_wf qadd_wf assert-qeq rationals_wf qmul_preserves_qless qmul_wf squash_wf true_wf qmul-qdiv-cancel int-subtype-rationals subtype_rel_self iff_weakening_equal uiff_transitivity2 qadd_preserves_qless qadd_ac_1_q qadd_comm_q qinverse_q mon_ident_q q_distrib qmul_one_qrng
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt introduction cut independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis universeIsType natural_numberEquality applyEquality because_Cache independent_isectElimination lambdaFormation_alt equalityTransitivity equalitySymmetry productElimination voidElimination equalityIstype inhabitedIsType baseClosed sqequalBase independent_pairEquality isect_memberEquality_alt isectIsTypeImplies lambdaEquality_alt imageElimination imageMemberEquality instantiate universeEquality minusEquality

Latex:
\mforall{}[a,b:\mBbbQ{}].    uiff(qavg(a;b)  <  b;a  <  b)



Date html generated: 2020_05_20-AM-09_17_15
Last ObjectModification: 2019_11_01-PM-01_57_51

Theory : rationals


Home Index