---

Step * 2 1 of Lemma better-r2-straightedge-compass


1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : {b:ℝ^2| b ≠ a ∧ c_b_d} 
5. q : ℝ^2
6. q_a_b
7. d(c;d) < d(c;q)
8. u : {u:ℝ^2| cd=cu ∧ q_u_b} 
9. v : ℝ^2
10. [%6] : cd=cv
∧ q_b_v
∧ (b ≠ d ⇒ (u ≠ v ∧ u ≠ b ∧ v ≠ b))
∧ (req-vec(2;b;d)
  ⇒ ((u ≠ v ⇒ ((req-vec(2;u;b) ∧ (r0 < b - c⋅q - b)) ∨ (req-vec(2;v;b) ∧ (b - c⋅q - b < r0))))
     ∧ (req-vec(2;u;v) ⇒ ((b - c⋅q - b = r0) ∧ req-vec(2;u;b)))))
11. v_b_a
12. v_b_u
⊢ ∃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))))))])
BY
{ (D 0 With ⌜v⌝ 
   THENA (Auto
          THEN DSetVars
          THEN MemTypeCD
          THEN Auto
          THEN Try ((BLemma `rv-be-symmetry` THEN Auto))
          THEN All (Unfold `rv-congruent`)
          THEN Auto)
   ) }

1
1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : {b:ℝ^2| b ≠ a ∧ c_b_d} 
5. q : ℝ^2
6. q_a_b
7. d(c;d) < d(c;q)
8. u : {u:ℝ^2| cd=cu ∧ q_u_b} 
9. v : ℝ^2
10. [%6] : cd=cv
∧ q_b_v
∧ (b ≠ d ⇒ (u ≠ v ∧ u ≠ b ∧ v ≠ b))
∧ (req-vec(2;b;d)
  ⇒ ((u ≠ v ⇒ ((req-vec(2;u;b) ∧ (r0 < b - c⋅q - b)) ∨ (req-vec(2;v;b) ∧ (b - c⋅q - b < r0))))
     ∧ (req-vec(2;u;v) ⇒ ((b - c⋅q - b = r0) ∧ req-vec(2;u;b)))))
11. v_b_a
12. v_b_u
⊢ ∃v@0:ℝ^2 [(cv@0=cd
           ∧ v@0_b_v
           ∧ (¬((¬a_b_v@0) ∧ (¬b_v@0_a) ∧ (¬v@0_a_b)))
           ∧ (b ≠ d ⇒ v@0 ≠ v)
           ∧ ((¬d ≠ b)
             ⇒ ((v@0 ≠ v ⇒ ((¬v ≠ b) ∨ (¬v@0 ≠ b)))
                ∧ ((¬v@0 ≠ v) ⇒ ((∀a':ℝ^2. ((d(a';b) = d(a;b)) ⇒ a'_b_a ⇒ (d(c;a) = d(c;a')))) ∧ (¬v ≠ b))))))]

---

Latex:

---

Latex:

1.  c  :  \mBbbR{}\^{}2
2.  d  :  \mBbbR{}\^{}2
3.  a  :  \mBbbR{}\^{}2
4.  b  :  \{b:\mBbbR{}\^{}2|  b  \mneq{}  a  \mwedge{}  c\_b\_d\} 
5.  q  :  \mBbbR{}\^{}2
6.  q\_a\_b
7.  d(c;d)  <  d(c;q)
8.  u  :  \{u:\mBbbR{}\^{}2|  cd=cu  \mwedge{}  q\_u\_b\} 
9.  v  :  \mBbbR{}\^{}2
10.  [\%6]  :  cd=cv
\mwedge{}  q\_b\_v
\mwedge{}  (b  \mneq{}  d  {}\mRightarrow{}  (u  \mneq{}  v  \mwedge{}  u  \mneq{}  b  \mwedge{}  v  \mneq{}  b))
\mwedge{}  (req-vec(2;b;d)
    {}\mRightarrow{}  ((u  \mneq{}  v  {}\mRightarrow{}  ((req-vec(2;u;b)  \mwedge{}  (r0  <  b  -  c\mcdot{}q  -  b))  \mvee{}  (req-vec(2;v;b)  \mwedge{}  (b  -  c\mcdot{}q  -  b  <  r0))))
          \mwedge{}  (req-vec(2;u;v)  {}\mRightarrow{}  ((b  -  c\mcdot{}q  -  b  =  r0)  \mwedge{}  req-vec(2;u;b)))))
11.  v\_b\_a
12.  v\_b\_u
\mvdash{}  \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))))))])


By

---

Latex:
(D  0  With  \mkleeneopen{}v\mkleeneclose{} 
  THENA  (Auto
                THEN  DSetVars
                THEN  MemTypeCD
                THEN  Auto
                THEN  Try  ((BLemma  `rv-be-symmetry`  THEN  Auto))
                THEN  All  (Unfold  `rv-congruent`)
                THEN  Auto)
  )

---

Home Index