Nuprl Lemma : arctangent1
arctangent(r1) = (π/r(4))
Proof
Definitions occuring in Statement :
arctangent: arctangent(x),
pi: π,
rdiv: (x/y),
req: x = y,
int-to-real: r(n),
natural_number: $n
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
rneq: x ≠ y,
guard: {T},
or: P ∨ Q,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True,
prop: ℙ,
cand: A c∧ B,
rminus: -(x),
halfpi: π/2,
cubic_converge: cubic_converge(b;m),
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
bnot: ¬bb,
lt_int: i <z j,
bfalse: ff,
btrue: tt,
fastpi: fastpi(n),
primrec: primrec(n;b;c),
rdiv: (x/y),
rmul: a * b,
pi: π,
int-rmul: k1 * a,
rinv: rinv(x),
mu-ge: mu-ge(f;n),
int-to-real: r(n),
absval: |i|,
eq_int: (i =z j),
accelerate: accelerate(k;f),
imax: imax(a;b),
canonical-bound: canonical-bound(r),
reg-seq-inv: reg-seq-inv(x),
reg-seq-mul: reg-seq-mul(x;y),
subtype_rel: A ⊆r B,
real: ℝ,
nat_plus: ℕ+,
rless: x < y,
sq_exists: ∃x:A [B[x]],
top: Top,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
rdiv_wf,
pi_wf,
int-to-real_wf,
rless-int,
rless_wf,
rminus_wf,
halfpi_wf,
real_wf,
less_than_wf,
arctangent_wf,
rtan_wf,
member_rooint_lemma,
arctangent-rtan,
req_functionality,
arctangent_functionality,
req_inversion,
rtan-pi-over-4,
req_weakening
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
dependent_set_memberEquality,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
natural_numberEquality,
independent_isectElimination,
sqequalRule,
inrFormation,
dependent_functionElimination,
because_Cache,
productElimination,
independent_functionElimination,
independent_pairFormation,
imageMemberEquality,
hypothesisEquality,
baseClosed,
addEquality,
applyEquality,
lambdaEquality,
setElimination,
rename,
productEquality,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
arctangent(r1) = (\mpi{}/r(4))
Date html generated:
2018_05_22-PM-03_03_56
Last ObjectModification:
2017_10_22-PM-08_10_28
Theory : reals_2
Home
Index