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