Step
*
1
1
of Lemma
r2-straightedge-compass
.....assertion.....
1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : {b:ℝ^2| b ≠ a ∧ c_b_d}
⊢ ∀x:ℝ. ∃q:ℝ^2. (b-a-q ∧ (x < d(b;q)))
BY
{ (D -1 THEN (Assert b ≠ a BY (Unhide THEN Auto)) THEN ThinVar `c' THEN ThinVar `d' THEN Auto) }
1
1. a : ℝ^2
2. b : ℝ^2
3. b ≠ a
4. x : ℝ
⊢ ∃q:ℝ^2. (b-a-q ∧ (x < d(b;q)))
Latex:
Latex:
.....assertion.....
1. c : \mBbbR{}\^{}2
2. d : \mBbbR{}\^{}2
3. a : \mBbbR{}\^{}2
4. b : \{b:\mBbbR{}\^{}2| b \mneq{} a \mwedge{} c\_b\_d\}
\mvdash{} \mforall{}x:\mBbbR{}. \mexists{}q:\mBbbR{}\^{}2. (b-a-q \mwedge{} (x < d(b;q)))
By
Latex:
(D -1 THEN (Assert b \mneq{} a BY (Unhide THEN Auto)) THEN ThinVar `c' THEN ThinVar `d' THEN Auto)
Home
Index