### 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