### Nuprl Lemma : near-root-rational-ext

`∀k:{2...}. ∀p:{p:ℤ| (0 ≤ p) ∨ (↑isOdd(k))} . ∀q,n:ℕ+.`
`  (∃r:ℤ × ℕ+ [let a,b = r `
`              in (0 ≤ p `⇐⇒` 0 ≤ a) ∧ (|(r(a))/b^k - (r(p)/r(q))| < (r1/r(n)))])`

Proof

Definitions occuring in Statement :  rdiv: `(x/y)` rless: `x < y` rabs: `|x|` rnexp: `x^k1` int-rdiv: `(a)/k1` rsub: `x - y` int-to-real: `r(n)` isOdd: `isOdd(n)` int_upper: `{i...}` nat_plus: `ℕ+` assert: `↑b` le: `A ≤ B` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` iff: `P `⇐⇒` Q` or: `P ∨ Q` and: `P ∧ Q` set: `{x:A| B[x]} ` spread: spread def product: `x:A × B[x]` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  member: `t ∈ T` eq_int: `(i =z j)` btrue: `tt` it: `⋅` bfalse: `ff` band: `p ∧b q` ifthenelse: `if b then t else f fi ` subtract: `n - m` lt_int: `i <z j` near-root: `near-root(k;p;q;n)` near-root-rational iroot-lemma2 uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x.t[x]` top: `Top` so_apply: `x[s]` uimplies: `b supposing a` strict4: `strict4(F)` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ` or: `P ∨ Q` squash: `↓T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  near-root-rational lifting-strict-decide istype-void has-value_wf_base istype-base is-exception_wf istype-universe lifting-strict-int_eq strict4-decide lifting-strict-callbyvalue strict4-spread lifting-strict-less iroot-lemma2
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed isect_memberEquality_alt voidElimination independent_isectElimination independent_pairFormation lambdaFormation_alt callbyvalueCallbyvalue callbyvalueReduce universeIsType baseApply closedConclusion hypothesisEquality callbyvalueExceptionCases inrFormation_alt imageMemberEquality imageElimination exceptionSqequal inlFormation_alt because_Cache

Latex:
\mforall{}k:\{2...\}.  \mforall{}p:\{p:\mBbbZ{}|  (0  \mleq{}  p)  \mvee{}  (\muparrow{}isOdd(k))\}  .  \mforall{}q,n:\mBbbN{}\msupplus{}.
(\mexists{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  [let  a,b  =  r
in  (0  \mleq{}  p  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  a)  \mwedge{}  (|(r(a))/b\^{}k  -  (r(p)/r(q))|  <  (r1/r(n)))])

Date html generated: 2019_10_30-AM-07_53_39
Last ObjectModification: 2019_04_02-AM-10_58_22

Theory : reals

Home Index