### Nuprl Lemma : qpositive-elim

`∀[r:ℚ]. (qpositive(r) ~ if isint(r) then 0 <z r else let p,q = r in (0 <z p ∧b 0 <z q) ∨b(p <z 0 ∧b q <z 0) fi )`

Proof

Definitions occuring in Statement :  qpositive: `qpositive(r)` rationals: `ℚ` bor: `p ∨bq` band: `p ∧b q` ifthenelse: `if b then t else f fi ` lt_int: `i <z j` bfalse: `ff` btrue: `tt` uall: `∀[x:A]. B[x]` isint: isint def spread: spread def natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` qpositive: `qpositive(r)` uimplies: `b supposing a` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)`
Lemmas referenced :  valueall-type-has-valueall rationals_wf rationals-valueall-type evalall-reduce
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination hypothesisEquality callbyvalueReduce sqequalAxiom

Latex:
\mforall{}[r:\mBbbQ{}]
(qpositive(r)  \msim{}  if  isint(r)
then  0  <z  r
else  let  p,q  =  r
in  (0  <z  p  \mwedge{}\msubb{}  0  <z  q)  \mvee{}\msubb{}(p  <z  0  \mwedge{}\msubb{}  q  <z  0)
fi  )

Date html generated: 2016_05_15-PM-10_39_37
Last ObjectModification: 2015_12_27-PM-07_58_58

Theory : rationals

Home Index