Nuprl Lemma : line-circle-intersection-lemma
∀a,b,c,r:ℝ.
((r0 < (a^2 + b^2))
⇒ (r0 ≤ (((a^2 + b^2) * r^2) - c^2))
⇒ (∀x,y:ℝ.
((((x = ((a * c) + (b * rsqrt(((a^2 + b^2) * r^2) - c^2))/a^2 + b^2))
∧ (y = ((b * c) - a * rsqrt(((a^2 + b^2) * r^2) - c^2)/a^2 + b^2)))
∨ ((x = ((a * c) - b * rsqrt(((a^2 + b^2) * r^2) - c^2)/a^2 + b^2))
∧ (y = ((b * c) + (a * rsqrt(((a^2 + b^2) * r^2) - c^2))/a^2 + b^2))))
⇒ ((((a * x) + (b * y)) = c) ∧ ((x^2 + y^2) = r^2)))))
Proof
Definitions occuring in Statement :
rsqrt: rsqrt(x),
rdiv: (x/y),
rleq: x ≤ y,
rless: x < y,
rnexp: x^k1,
rsub: x - y,
req: x = y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
nat: ℕ,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
not: ¬A,
implies: P ⇒ Q,
false: False,
cand: A c∧ B,
or: P ∨ Q,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
rneq: x ≠ y,
guard: {T},
prop: ℙ,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
true: True,
req_int_terms: t1 ≡ t2,
rdiv: (x/y),
squash: ↓T,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Latex:
\mforall{}a,b,c,r:\mBbbR{}.
((r0 < (a\^{}2 + b\^{}2))
{}\mRightarrow{} (r0 \mleq{} (((a\^{}2 + b\^{}2) * r\^{}2) - c\^{}2))
{}\mRightarrow{} (\mforall{}x,y:\mBbbR{}.
((((x = ((a * c) + (b * rsqrt(((a\^{}2 + b\^{}2) * r\^{}2) - c\^{}2))/a\^{}2 + b\^{}2))
\mwedge{} (y = ((b * c) - a * rsqrt(((a\^{}2 + b\^{}2) * r\^{}2) - c\^{}2)/a\^{}2 + b\^{}2)))
\mvee{} ((x = ((a * c) - b * rsqrt(((a\^{}2 + b\^{}2) * r\^{}2) - c\^{}2)/a\^{}2 + b\^{}2))
\mwedge{} (y = ((b * c) + (a * rsqrt(((a\^{}2 + b\^{}2) * r\^{}2) - c\^{}2))/a\^{}2 + b\^{}2))))
{}\mRightarrow{} ((((a * x) + (b * y)) = c) \mwedge{} ((x\^{}2 + y\^{}2) = r\^{}2)))))
Date html generated:
2020_05_20-PM-01_10_17
Last ObjectModification:
2020_01_14-PM-03_35_31
Theory : reals!model!euclidean!geometry
Home
Index