Nuprl Lemma : sine-approx-for-small-ext
∀a:{2...}. ∀N:ℕ+. ∀x:{x:ℝ| |x| ≤ (r1/r(a))} . (∃z:ℤ [(|sine(x) - (r(z)/r(2 * N))| ≤ (r(2)/r(N)))])
Proof
Definitions occuring in Statement :
sine: sine(x)
,
rdiv: (x/y)
,
rleq: x ≤ y
,
rabs: |x|
,
rsub: x - 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: n * m
,
natural_number: $n
,
int: ℤ
Definitions unfolded in proof :
member: t ∈ T
,
sine-approx-for-small,
sine-approx-lemma-ext
Lemmas referenced :
sine-approx-for-small,
sine-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{} [(|sine(x) - (r(z)/r(2 * N))| \mleq{} (r(2)/r(N)))])
Date html generated:
2019_10_29-AM-10_34_38
Last ObjectModification:
2019_02_08-PM-01_42_07
Theory : reals
Home
Index