Nuprl Lemma : qdiv-non-neg
∀a,b:ℚ. (0 < b ∧ (0 ≤ a)) ∨ (b < 0 ∧ (a ≤ 0)) ⇐⇒ 0 ≤ (a/b) supposing ¬(b = 0 ∈ ℚ)
Proof
Definitions occuring in Statement :
qle: r ≤ s,
qless: r < s,
qdiv: (r/s),
rationals: ℚ,
uimplies: b supposing a,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
or: P ∨ Q,
and: P ∧ Q,
natural_number: $n,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
not: ¬A,
implies: P ⇒ Q,
false: False,
uall: ∀[x:A]. B[x],
prop: ℙ,
iff: P ⇐⇒ Q,
and: P ∧ Q,
or: P ∨ Q,
subtype_rel: A ⊆r B,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
true: True,
squash: ↓T,
guard: {T},
decidable: Dec(P),
cand: A c∧ B
Lemmas referenced :
equal-wf-T-base,
rationals_wf,
or_wf,
qless_wf,
int-subtype-rationals,
qle_wf,
qdiv_wf,
not_wf,
qmul_preserves_qle,
qmul_wf,
squash_wf,
true_wf,
qmul_zero_qrng,
qmul-qdiv-cancel,
iff_weakening_equal,
qmul_over_minus_qrng,
qadd_preserves_qless,
qadd_wf,
qadd_comm_q,
qinverse_q,
mon_ident_q,
qadd_preserves_qle,
decidable__qless,
qmul_preserves_qle2,
qle_weakening_lt_qorder,
qle_witness,
qless_trichot_qorder,
qless-int,
qmul_reverses_qle
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
introduction,
sqequalRule,
sqequalHypSubstitution,
lambdaEquality,
dependent_functionElimination,
thin,
hypothesisEquality,
voidElimination,
extract_by_obid,
isectElimination,
hypothesis,
baseClosed,
rename,
independent_pairFormation,
unionElimination,
productEquality,
natural_numberEquality,
applyEquality,
because_Cache,
independent_isectElimination,
productElimination,
imageElimination,
equalityTransitivity,
equalitySymmetry,
imageMemberEquality,
universeEquality,
independent_functionElimination,
minusEquality,
inrFormation,
inlFormation
Latex:
\mforall{}a,b:\mBbbQ{}. (0 < b \mwedge{} (0 \mleq{} a)) \mvee{} (b < 0 \mwedge{} (a \mleq{} 0)) \mLeftarrow{}{}\mRightarrow{} 0 \mleq{} (a/b) supposing \mneg{}(b = 0)
Date html generated:
2018_05_21-PM-11_58_47
Last ObjectModification:
2017_07_26-PM-06_48_20
Theory : rationals
Home
Index