Nuprl Lemma : converges-to-sine-ext
∀x:ℝ. lim n→∞.if n=0 then r0 else (sine((x within 1/n)) within 1/n) = sine(x)
Proof
Definitions occuring in Statement :
sine: sine(x),
converges-to: lim n→∞.x[n] = y,
rational-approx: (x within 1/n),
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
int_eq: if a=b then c else d,
natural_number: $n
Definitions unfolded in proof :
member: t ∈ T,
converges-to-sine
Lemmas referenced :
converges-to-sine
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}x:\mBbbR{}. lim n\mrightarrow{}\minfty{}.if n=0 then r0 else (sine((x within 1/n)) within 1/n) = sine(x)
Date html generated:
2016_10_26-PM-00_13_45
Last ObjectModification:
2016_09_12-PM-05_39_52
Theory : reals_2
Home
Index