### Nuprl Lemma : rabs-abs

`∀[a:ℤ]. (|r(a)| = r(|a|))`

Proof

Definitions occuring in Statement :  rabs: `|x|` req: `x = y` int-to-real: `r(n)` absval: `|i|` uall: `∀[x:A]. B[x]` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` true: `True` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` nat: `ℕ`
Lemmas referenced :  nat_wf rabs_wf req_witness req_weakening iff_weakening_equal absval_wf int-to-real_wf rabs-int real_wf true_wf squash_wf req_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination lemma_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache sqequalRule natural_numberEquality imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination setElimination rename intEquality

Latex:
\mforall{}[a:\mBbbZ{}].  (|r(a)|  =  r(|a|))

Date html generated: 2016_05_18-AM-07_14_02
Last ObjectModification: 2016_01_17-AM-01_53_33

Theory : reals

Home Index