Nuprl Lemma : rmul-nonzero-on
∀I:Interval. ∀f,g:I ⟶ℝ. (f[x]≠r0 for x ∈ I ⇒ g[x]≠r0 for x ∈ I ⇒ f[x] * g[x]≠r0 for x ∈ I)
Proof
Definitions occuring in Statement :
nonzero-on: f[x]≠r0 for x ∈ I,
rfun: I ⟶ℝ,
interval: Interval,
rmul: a * b,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
nonzero-on: f[x]≠r0 for x ∈ I,
member: t ∈ T,
sq_exists: ∃x:{A| B[x]},
uall: ∀[x:A]. B[x],
and: P ∧ Q,
cand: A c∧ B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
or: P ∨ Q,
prop: ℙ,
nat_plus: ℕ+,
so_lambda: λ2x.t[x],
so_apply: x[s],
label: ...$L... t,
rfun: I ⟶ℝ,
guard: {T},
uimplies: b supposing a,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
rge: x ≥ y
Lemmas referenced :
rmul_wf,
rmul-is-positive,
rless_wf,
int-to-real_wf,
i-member-approx,
less_than_wf,
i-member_wf,
i-approx_wf,
real_wf,
set_wf,
nat_plus_wf,
icompact_wf,
nonzero-on_wf,
rfun_wf,
interval_wf,
all_wf,
rleq_wf,
rabs_wf,
equal_wf,
rleq_weakening_rless,
rless_transitivity1,
rleq_weakening_equal,
rleq_functionality,
req_weakening,
rabs-rmul,
rleq_functionality_wrt_implies,
rmul_functionality_wrt_rleq2
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
setElimination,
rename,
dependent_set_memberFormation,
cut,
introduction,
extract_by_obid,
isectElimination,
hypothesis,
productElimination,
independent_functionElimination,
inlFormation,
independent_pairFormation,
productEquality,
natural_numberEquality,
dependent_set_memberEquality,
because_Cache,
sqequalRule,
lambdaEquality,
applyEquality,
setEquality,
functionEquality,
equalityTransitivity,
equalitySymmetry,
independent_isectElimination
Latex:
\mforall{}I:Interval. \mforall{}f,g:I {}\mrightarrow{}\mBbbR{}. (f[x]\mneq{}r0 for x \mmember{} I {}\mRightarrow{} g[x]\mneq{}r0 for x \mmember{} I {}\mRightarrow{} f[x] * g[x]\mneq{}r0 for x \mmember{} I)
Date html generated:
2017_10_03-AM-10_26_58
Last ObjectModification:
2017_07_28-AM-08_10_56
Theory : reals
Home
Index