Step
*
1
1
1
1
1
1
1
1
of Lemma
p5eu
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ab=ac
6. ¬(a = b ∈ Point)
7. ¬(a = c ∈ Point)
8. ¬(b = c ∈ Point)
9. x : Point
10. a_b_x ∧ bx=ac
11. y : Point
12. a_c_y ∧ cy=ab
⊢ (¬(x = b ∈ Point))
∧ (¬(c = b ∈ Point))
∧ (¬(y = c ∈ Point))
∧ (¬(b = c ∈ Point))
∧ (∃a',c',x',z':Point. (b_x_a' ∧ b_c_c' ∧ c_y_x' ∧ c_b_z' ∧ ba'=cx' ∧ bc'=cz' ∧ a'c'=x'z'))
BY
{ Auto }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ab=ac
6. ¬(a = b ∈ Point)
7. ¬(a = c ∈ Point)
8. ¬(b = c ∈ Point)
9. x : Point
10. a_b_x
11. bx=ac
12. y : Point
13. a_c_y
14. cy=ab
15. ¬(x = b ∈ Point)
16. ¬(c = b ∈ Point)
17. ¬(y = c ∈ Point)
18. ¬(b = c ∈ Point)
⊢ ∃a',c',x',z':Point. (b_x_a' ∧ b_c_c' ∧ c_y_x' ∧ c_b_z' ∧ ba'=cx' ∧ bc'=cz' ∧ a'c'=x'z')
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ab=ac
6. \mneg{}(a = b)
7. \mneg{}(a = c)
8. \mneg{}(b = c)
9. x : Point
10. a\_b\_x \mwedge{} bx=ac
11. y : Point
12. a\_c\_y \mwedge{} cy=ab
\mvdash{} (\mneg{}(x = b))
\mwedge{} (\mneg{}(c = b))
\mwedge{} (\mneg{}(y = c))
\mwedge{} (\mneg{}(b = c))
\mwedge{} (\mexists{}a',c',x',z':Point. (b\_x\_a' \mwedge{} b\_c\_c' \mwedge{} c\_y\_x' \mwedge{} c\_b\_z' \mwedge{} ba'=cx' \mwedge{} bc'=cz' \mwedge{} a'c'=x'z'))
By
Latex:
Auto
Home
Index