Nuprl Lemma : cosine-approx-for-small-ext

a:{2...}. ∀N:ℕ+. ∀x:{x:ℝ|x| ≤ (r1/r(a))} .  (∃z:ℤ [(|cosine(x) (r(z)/r(2 N))| ≤ (r(2)/r(N)))])


Proof




Definitions occuring in Statement :  cosine: cosine(x) rdiv: (x/y) rleq: x ≤ y rabs: |x| rsub: y int-to-real: r(n) real: int_upper: {i...} nat_plus: + all: x:A. B[x] sq_exists: x:A [B[x]] set: {x:A| B[x]}  multiply: m natural_number: $n int:
Definitions unfolded in proof :  member: t ∈ T cosine-approx-for-small cosine-approx-lemma-ext
Lemmas referenced :  cosine-approx-for-small cosine-approx-lemma-ext
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}a:\{2...\}.  \mforall{}N:\mBbbN{}\msupplus{}.  \mforall{}x:\{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(a))\}  .    (\mexists{}z:\mBbbZ{}  [(|cosine(x)  -  (r(z)/r(2  *  N))|  \mleq{}  (r(2)/r(N)))]\000C)



Date html generated: 2019_10_29-AM-10_37_49
Last ObjectModification: 2019_02_08-PM-01_56_56

Theory : reals


Home Index