Nuprl Lemma : rv-five-segment-lemma
∀n:ℕ. ∀A,B,C,D:ℝ^n. ∀t:ℝ.
((t ∈ (r0, r1))
⇒ req-vec(n;B;t*A + r1 - t*C)
⇒ let a = d(D;B) in
let b = d(A;D) in
let c = d(B;C) in
let d = d(A;B) in
let x = d(D;C) in
let s = (t/t - r1) in
x^2 = (c^2 + a^2 + (s * (b^2 - d^2 + a^2))))
Proof
Definitions occuring in Statement :
real-vec-dist: d(x;y),
real-vec-mul: a*X,
real-vec-add: X + Y,
req-vec: req-vec(n;x;y),
real-vec: ℝ^n,
rooint: (l, u),
i-member: r ∈ I,
rdiv: (x/y),
rnexp: x^k1,
rsub: x - y,
req: x = y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
real: ℝ,
nat: ℕ,
let: let,
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
Definitions unfolded in proof :
not: ¬A,
false: False,
req_int_terms: t1 ≡ t2,
uiff: uiff(P;Q),
uimplies: b supposing a,
prop: ℙ,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
uall: ∀[x:A]. B[x],
let: let,
top: Top,
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x],
real-vec-dist: d(x;y),
real-vec-norm: ||x||,
nat: ℕ,
le: A ≤ B,
less_than': less_than'(a;b),
subtype_rel: A ⊆r B,
rneq: x ≠ y,
or: P ∨ Q,
rev_uimplies: rev_uimplies(P;Q),
real-vec-sub: X - Y,
real-vec-add: X + Y,
req-vec: req-vec(n;x;y),
real-vec: ℝ^n,
int_seg: {i..j-},
lelt: i ≤ j < k,
true: True,
real-vec-mul: a*X,
squash: ↓T,
guard: {T},
rat_term_to_real: rat_term_to_real(f;t),
rtermMultiply: left "*" right,
rat_term_ind: rat_term_ind,
rtermDivide: num "/" denom,
rtermVar: rtermVar(var),
rtermSubtract: left "-" right,
rtermConstant: "const",
rtermAdd: left "+" right,
pi1: fst(t),
pi2: snd(t)
Latex:
\mforall{}n:\mBbbN{}. \mforall{}A,B,C,D:\mBbbR{}\^{}n. \mforall{}t:\mBbbR{}.
((t \mmember{} (r0, r1))
{}\mRightarrow{} req-vec(n;B;t*A + r1 - t*C)
{}\mRightarrow{} let a = d(D;B) in
let b = d(A;D) in
let c = d(B;C) in
let d = d(A;B) in
let x = d(D;C) in
let s = (t/t - r1) in
x\^{}2 = (c\^{}2 + a\^{}2 + (s * (b\^{}2 - d\^{}2 + a\^{}2))))
Date html generated:
2020_05_20-PM-00_51_24
Last ObjectModification:
2020_03_17-PM-02_22_21
Theory : reals
Home
Index