Step * 8 1 1 of Lemma eu-eq_dist-axiomsA


1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. a' Point
11. b' Point
12. c' Point
13. {u:Point| c' u} 
14. B(a'b'c')
15. B(a'uc')
16. ab ≅ a'b'
17. cd ≅ b'c'
18. ef ≅ a'u
19. ¬D(a;b;b;b;x;y)
20. ¬ab > xy
21. xy ≥ ab
22. a' c'
23. Point
24. c'-a'-A
25. a'A ≅ c'a'
26. Point
27. B(Aa'B)
28. a'B ≅ xy
29. Point
30. B(Aa'U)
31. a'U ≅ ef
⊢ ∃a',b',c':Point. ∃u:{u:Point| c' u} (B(a'b'c') ∧ B(a'uc') ∧ xy ≅ a'b' ∧ cd ≅ b'c' ∧ ef ≅ a'u)
BY
((gProperProlong ⌜a'⌝⌜c'⌝`P1'⌜a'⌝⌜c'⌝⋅ THENA Auto)
   THEN (gProlong ⌜a'⌝⌜c'⌝`E1'⌜x⌝⌜y⌝⋅ THENA Auto)
   THEN (gProlong ⌜P1⌝⌜c'⌝`E2'⌜c⌝⌜d⌝⋅ THENA Auto)
   THEN (gProlong ⌜A⌝⌜a'⌝`C'⌜E1⌝⌜E2⌝⋅ THENA Auto)
   THEN ExRepD) }

1
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. a' Point
11. b' Point
12. c' Point
13. {u:Point| c' u} 
14. B(a'b'c')
15. B(a'uc')
16. ab ≅ a'b'
17. cd ≅ b'c'
18. ef ≅ a'u
19. ¬D(a;b;b;b;x;y)
20. ¬ab > xy
21. xy ≥ ab
22. a' c'
23. Point
24. c'-a'-A
25. a'A ≅ c'a'
26. Point
27. B(Aa'B)
28. a'B ≅ xy
29. Point
30. B(Aa'U)
31. a'U ≅ ef
32. P1 Point
33. a'-c'-P1
34. c'P1 ≅ a'c'
35. E1 Point
36. B(a'c'E1)
37. c'E1 ≅ xy
38. E2 Point
39. B(P1c'E2)
40. c'E2 ≅ cd
41. Point
42. B(Aa'C)
43. a'C ≅ E1E2
⊢ ∃a',b',c':Point. ∃u:{u:Point| c' u} (B(a'b'c') ∧ B(a'uc') ∧ xy ≅ a'b' ∧ cd ≅ b'c' ∧ ef ≅ a'u)


Latex:


Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  x  :  Point
9.  y  :  Point
10.  a'  :  Point
11.  b'  :  Point
12.  c'  :  Point
13.  u  :  \{u:Point|  c'  \#  u\} 
14.  B(a'b'c')
15.  B(a'uc')
16.  ab  \mcong{}  a'b'
17.  cd  \mcong{}  b'c'
18.  ef  \mcong{}  a'u
19.  \mneg{}D(a;b;b;b;x;y)
20.  \mneg{}ab  >  xy
21.  xy  \mgeq{}  ab
22.  a'  \#  c'
23.  A  :  Point
24.  c'-a'-A
25.  a'A  \mcong{}  c'a'
26.  B  :  Point
27.  B(Aa'B)
28.  a'B  \mcong{}  xy
29.  U  :  Point
30.  B(Aa'U)
31.  a'U  \mcong{}  ef
\mvdash{}  \mexists{}a',b',c':Point.  \mexists{}u:\{u:Point|  c'  \#  u\}  .  (B(a'b'c')  \mwedge{}  B(a'uc')  \mwedge{}  xy  \mcong{}  a'b'  \mwedge{}  cd  \mcong{}  b'c'  \mwedge{}  ef  \mcong{}  a'u)


By


Latex:
((gProperProlong  \mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}`P1'\mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProlong  \mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}`E1'\mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProlong  \mkleeneopen{}P1\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}`E2'\mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProlong  \mkleeneopen{}A\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}`C'\mkleeneopen{}E1\mkleeneclose{}\mkleeneopen{}E2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ExRepD)




Home Index