Nuprl Lemma : qmul_functionality_wrt_qless2

[a,b,c,d:ℚ].  (a c < d) supposing ((c ≤ d) and a < and (0 ≤ b) and 0 < c)


Proof




Definitions occuring in Statement :  qle: r ≤ s qless: r < s qmul: s rationals: uimplies: supposing a uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a implies:  Q prop: uiff: uiff(P;Q) and: P ∧ Q subtype_rel: A ⊆B true: True guard: {T} squash: T iff: ⇐⇒ Q
Lemmas referenced :  iff_weakening_equal qmul_comm_qrng true_wf squash_wf qless_transitivity_2_qorder rationals_wf int-subtype-rationals qle_wf qless_wf qless_witness qmul_preserves_qless qmul_wf qle_witness qmul_preserves_qle2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis independent_functionElimination because_Cache productElimination independent_pairFormation sqequalRule isect_memberEquality equalityTransitivity equalitySymmetry natural_numberEquality applyEquality lambdaEquality imageElimination imageMemberEquality baseClosed universeEquality

Latex:
\mforall{}[a,b,c,d:\mBbbQ{}].    (a  *  c  <  b  *  d)  supposing  ((c  \mleq{}  d)  and  a  <  b  and  (0  \mleq{}  b)  and  0  <  c)



Date html generated: 2016_05_15-PM-11_00_46
Last ObjectModification: 2016_01_16-PM-09_30_37

Theory : rationals


Home Index