Nuprl Lemma : better-r2-straightedge-compass

∀c,d,a:ℝ^2. ∀b:{b:ℝ^2| b ≠ a ∧ c_b_d} .
  ∃u:{u:ℝ^2| cu=cd ∧ a_b_u} 
   (∃v:ℝ^2 [(cv=cd
           ∧ v_b_u
           ∧ (¬((¬a_b_v) ∧ (¬b_v_a) ∧ (¬v_a_b)))
           ∧ (b ≠ d ⇒ v ≠ u)
           ∧ ((¬d ≠ b)
             ⇒ ((v ≠ u ⇒ ((¬u ≠ b) ∨ (¬v ≠ b)))
                ∧ ((¬v ≠ u) ⇒ ((∀a':ℝ^2. ((d(a';b) = d(a;b)) ⇒ a'_b_a ⇒ (d(c;a) = d(c;a')))) ∧ (¬u ≠ b))))))])


Proof



Definitions occuring in Statement :  rv-be: a_b_c,  real-vec-sep: a ≠ b,  rv-congruent: ab=cd,  real-vec-dist: d(x;y),  real-vec: ℝ^n,  req: x = y,  all: ∀x:A. B[x],  sq_exists: ∃x:A [B[x]],  exists: ∃x:A. B[x],  not: ¬A,  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  set: {x:A| B[x]} ,  natural_number: $n
Definitions unfolded in proof :  all: ∀x:A. B[x],  member: t ∈ T,  and: P ∧ Q,  uall: ∀[x:A]. B[x],  nat: ℕ,  le: A ≤ B,  less_than': less_than'(a;b),  not: ¬A,  implies: P ⇒ Q,  false: False,  prop: ℙ,  sq_stable: SqStable(P),  squash: ↓T,  exists: ∃x:A. B[x],  real-vec: ℝ^n,  int_seg: {i..j-},  lelt: i ≤ j < k,  subtype_rel: A ⊆r B,  real-vec-dist: d(x;y),  real-vec-norm: ||x||,  real-vec-sub: X - Y,  nat_plus: ℕ+,  real-vec-sep: a ≠ b,  rless: x < y,  sq_exists: ∃x:A [B[x]],  decidable: Dec(P),  or: P ∨ Q,  uimplies: b supposing a,  satisfiable_int_formula: satisfiable_int_formula(fmla),  real: ℝ,  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  btrue: tt,  bfalse: ff,  uiff: uiff(P;Q),  rev_uimplies: rev_uimplies(P;Q),  req_int_terms: t1 ≡ t2,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  cand: A c∧ B,  less_than: a < b,  true: True,  rge: x ≥ y,  guard: {T},  rv-congruent: ab=cd,  rv-be: a_b_c,  rv-between: a-b-c,  stable: Stable{P},  real-vec-between: a-b-c,  rneq: x ≠ y,  i-member: r ∈ I,  rooint: (l, u),  rdiv: (x/y),  req-vec: req-vec(n;x;y),  real-vec-mul: a*X,  real-vec-add: X + Y,  real-vec-be: real-vec-be(n;a;b;c),  rccint: [l, u]
Latex:
\mforall{}c,d,a:\mBbbR{}\^{}2.  \mforall{}b:\{b:\mBbbR{}\^{}2|  b  \mneq{}  a  \mwedge{}  c\_b\_d\}  .
    \mexists{}u:\{u:\mBbbR{}\^{}2|  cu=cd  \mwedge{}  a\_b\_u\} 
      (\mexists{}v:\mBbbR{}\^{}2  [(cv=cd
                      \mwedge{}  v\_b\_u
                      \mwedge{}  (\mneg{}((\mneg{}a\_b\_v)  \mwedge{}  (\mneg{}b\_v\_a)  \mwedge{}  (\mneg{}v\_a\_b)))
                      \mwedge{}  (b  \mneq{}  d  {}\mRightarrow{}  v  \mneq{}  u)
                      \mwedge{}  ((\mneg{}d  \mneq{}  b)
                          {}\mRightarrow{}  ((v  \mneq{}  u  {}\mRightarrow{}  ((\mneg{}u  \mneq{}  b)  \mvee{}  (\mneg{}v  \mneq{}  b)))
                                \mwedge{}  ((\mneg{}v  \mneq{}  u)
                                    {}\mRightarrow{}  ((\mforall{}a':\mBbbR{}\^{}2.  ((d(a';b)  =  d(a;b))  {}\mRightarrow{}  a'\_b\_a  {}\mRightarrow{}  (d(c;a)  =  d(c;a'))))
                                          \mwedge{}  (\mneg{}u  \mneq{}  b))))))])


Date html generated: 2020_05_20-PM-00_57_43
Last ObjectModification: 2019_12_14-PM-02_59_07

Theory : reals


Home Index