---

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)))))

Definition: r2-perp
r2-perp(x) ==  λi.if (i =z 0) then (-(x 1)/||x||) else (x 0/||x||) fi 

Lemma: r2-perp_wf
∀[x:ℝ^2]. ((r0 < ||x||) ⇒ (r2-perp(x) ∈ {y:ℝ^2| (x⋅y = r0) ∧ (||y|| = r1)} ))

Lemma: r2-dot-product-eq-0-iff-perp
∀x:ℝ^2. ((r0 < ||x||) ⇒ (∀y:ℝ^2. (y⋅x = r0 ⇐⇒ ∃t:ℝ. req-vec(2;y;t*r2-perp(x)))))

Definition: vec-midpoint
vec-midpoint(a;b) ==  (r1/r(2))*a + b

Lemma: vec-midpoint_wf
∀[n:ℕ]. ∀[a,b:ℝ^n].  (vec-midpoint(a;b) ∈ ℝ^n)

Lemma: vec-midpoint-dist
∀[n:ℕ]. ∀[a,b:ℝ^n].  (d(a;vec-midpoint(a;b)) = ((r1/r(2)) * d(a;b)))

Lemma: vec-midpoint-symmetry
∀[n:ℕ]. ∀[a,b:ℝ^n].  req-vec(n;vec-midpoint(b;a);vec-midpoint(a;b))

Lemma: r2-equidistant-implies
∀a,b:ℝ^2.  (a ≠ b ⇒ (∀x:ℝ^2. (ax=bx ⇒ (∃t:ℝ. req-vec(2;x;vec-midpoint(a;b) + t*r2-perp(b - a))))))

Lemma: r2-equidistant-implies'
∀a,b:ℝ^2.  (a ≠ b ⇒ (∀x:ℝ^2. (xa=xb ⇒ (∃t:ℝ. req-vec(2;x;vec-midpoint(a;b) + t*r2-perp(b - a))))))

Lemma: r2-upper-dimension
∀[a,b,p,q,r:ℝ^2].
  (¬(p ≠ q ∧ q ≠ r ∧ r ≠ p ∧ (¬p-q-r) ∧ (¬q-r-p) ∧ (¬r-p-q))) supposing (ra=rb and qa=qb and pa=pb and a ≠ b)

Definition: r2-eu-prim
r2-eu-prim() ==  Point=ℝ^2 O=λa,b,c,d. (d(c;d) < d(a;b)) Left=λa,b,c. r2-left(a;b;c)

Lemma: r2-eu-prim_wf
r2-eu-prim() ∈ GeometryPrimitives

Lemma: r2-basic-geo-axioms
BasicGeometryAxioms(r2-eu-prim())

Lemma: r2-gt-or
∀a,b,c:ℝ^2. ∀d:{d:ℝ^2| d(c;d) < d(a;b)} . ∀x,y:ℝ^2.  ((d(c;d) < d(x;y)) ∨ (d(x;y) < d(a;b)))

Definition: r2-eu
EuclideanPlane(ℝ^2) ==
  primitive=r2-eu-prim()
  Ssquashstable=TERMOF{sq_stable-dist-rless:o, 1:l} 2
  Lorsquashstable=TERMOF{sq_stable__r2-left-or:o, 1:l}
  SepOr=TERMOF{r2-sep-or:o, 1:l}
  nontriv=TERMOF{r2-nontrivial:o, 1:l}
  SS=TERMOF{r2-plane-separation:o, 1:l}
  SC=TERMOF{r2-straightedge-compass-simple:o, 1:l}
  CC=TERMOF{r2-compass-compass-simple:o, 1:l}

Lemma: r2-eu_wf
EuclideanPlane(ℝ^2) ∈ EuclideanPlane

Definition: r2-line
r2-line ==  a:ℝ^2 × b:ℝ^2 × a ≠ b

Lemma: r2-line_wf
r2-line ∈ Type

Definition: r2-line-sep
r2-line-sep(l;m) ==  ∃p:ℝ^2. ((|pfst(l)fst(snd(l))| = r0) ∧ |pfst(m)fst(snd(m))| ≠ r0)

Lemma: r2-line-sep_wf
∀l,m:r2-line.  (r2-line-sep(l;m) ∈ ℙ)

Definition: r2-line-eq
r2-line-eq(l;m) ==  ¬r2-line-sep(l;m)

Lemma: r2-line-eq_wf
∀l,m:r2-line.  (r2-line-eq(l;m) ∈ ℙ)

Lemma: r2-line-eq_weakening
∀l,m:r2-line.  ((l = m ∈ r2-line) ⇒ r2-line-eq(l;m))

Definition: line-det
line-det(a;b;c;d) ==
  ((((d 1) * (a 1)) - (d 1) * (a 0) - (d 0) * (a 1)) + ((d 0) * (a 0))) - (((b 1) * (c 1)) - (b 1) * (c 0) - (b 0)
  * (c 1))
  + ((b 0) * (c 0))

Lemma: line-det_wf
∀[a,b,c,d:ℝ^2].  (line-det(a;b;c;d) ∈ ℝ)

Definition: r2-lines-par
r2-lines-par(a;b;c;d) ==  line-det(a;b;c;d) ≠ r0

Lemma: r2-lines-par_wf
∀[a,b,c,d:ℝ^2].  (r2-lines-par(a;b;c;d) ∈ ℙ)



Home Index