Nuprl Lemma : rabs-rdiv

`∀x,y:ℝ.  (y ≠ r0 `` (|(x/y)| = (|x|/|y|)))`

Proof

Definitions occuring in Statement :  rdiv: `(x/y)` rneq: `x ≠ y` rabs: `|x|` req: `x = y` int-to-real: `r(n)` real: `ℝ` all: `∀x:A. B[x]` implies: `P `` Q` natural_number: `\$n`
Definitions unfolded in proof :  rdiv: `(x/y)` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` rneq: `x ≠ y` guard: `{T}` or: `P ∨ Q` uimplies: `b supposing a` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  rabs-neq-zero rneq_wf int-to-real_wf real_wf rabs_wf rmul_wf rinv_wf2 rless_wf req_weakening req_functionality req_transitivity rabs-rmul rmul_functionality rabs-rinv
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis isectElimination natural_numberEquality inrFormation because_Cache independent_isectElimination productElimination

Latex:
\mforall{}x,y:\mBbbR{}.    (y  \mneq{}  r0  {}\mRightarrow{}  (|(x/y)|  =  (|x|/|y|)))

Date html generated: 2016_05_18-AM-07_26_56
Last ObjectModification: 2015_12_28-AM-00_50_22

Theory : reals

Home Index