### Nuprl Lemma : near-root-rational

k:{2...}. ∀p:{p:ℤ(0 ≤ p) ∨ (↑isOdd(k))} . ∀q,n:ℕ+.
(∃r:ℤ × ℕ+ [let a,b
in (0 ≤ ⇐⇒ 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: 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: ⇐⇒ 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 :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T prop: or: P ∨ Q int_upper: {i...} implies:  Q sq_stable: SqStable(P) squash: T nat_plus: + uimplies: supposing a sq_type: SQType(T) guard: {T} uiff: uiff(P;Q) and: P ∧ Q bfalse: ff band: p ∧b q ifthenelse: if then else fi  so_lambda: λ2x.t[x] so_apply: x[s] bool: 𝔹 decidable: Dec(P) not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False nat: unit: Unit it: btrue: tt bnot: ¬bb assert: b eq_int: (i =z j) nequal: a ≠ b ∈  top: Top subtype_rel: A ⊆B subtract: m ge: i ≥  le: A ≤ B less_than': less_than'(a;b) exp: i^n primrec: primrec(n;b;c) iff: ⇐⇒ Q rev_implies:  Q true: True sq_exists: x:A [B[x]] rneq: x ≠ y cand: c∧ B less_than: a < b rless: x < y isOdd: isOdd(n) rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y req_int_terms: t1 ≡ t2 rdiv: (x/y)

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: 2020_05_20-PM-00_29_17
Last ObjectModification: 2020_01_06-PM-00_55_43

Theory : reals

Home Index