Step
*
1
1
1
1
of Lemma
perp-aux-general-construction
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. c # ba
7. Colinear(a;b;x)
8. Colinear(c;x;x)
9. ∀u,v:Point. (Colinear(a;b;u) ⇒ Colinear(c;x;v) ⇒ Ruxv)
10. a ≠ x
11. Raxc
12. Rbxc
13. Point
14. c ≠ x
15. c' : Point
16. c-x-c'
17. xc' ≅ cx
18. ∀c':Point. (c'=x=c ⇒ ac ≅ ac')
19. c'=x=c
20. ac ≅ ac'
21. c1 : Point
22. c-a-c1
23. ac1 ≅ ca
24. c' # c1a
⊢ ∃c1,c',p:Point. (((c=a=c1 ∧ c=x=c') ∧ c'a ≅ ca) ∧ c' # c1a ∧ ((a # cc' ∧ c1=p=c') ∧ ab ⊥a pa) ∧ p # ab)
BY
{ (((Assert c1=a=c BY (D 0 THEN Auto)) THEN InstConcl [⌜c1⌝;⌜c'⌝]⋅ THEN Auto)
THEN ((InstLemma`geo-congruent-mid-exists` [⌜e⌝;⌜c'⌝;⌜c1⌝;⌜a⌝]⋅ THEN Auto) THEN ExRepD THEN RenameVar `p' (26))
THEN InstConcl [⌜p⌝]⋅
THEN Auto) }
1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. c # ba
7. Colinear(a;b;x)
8. Colinear(c;x;x)
9. ∀u,v:Point. (Colinear(a;b;u) ⇒ Colinear(c;x;v) ⇒ Ruxv)
10. a ≠ x
11. Raxc
12. Rbxc
13. Point
14. c ≠ x
15. c' : Point
16. c-x-c'
17. xc' ≅ cx
18. ∀c':Point. (c'=x=c ⇒ ac ≅ ac')
19. c'=x=c
20. ac ≅ ac'
21. c1 : Point
22. c-a-c1
23. ac1 ≅ ca
24. c' # c1a
25. c1=a=c
26. p : Point
27. c'=p=c1
⊢ c=a=c1
2
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. c # ba
7. Colinear(a;b;x)
8. Colinear(c;x;x)
9. ∀u,v:Point. (Colinear(a;b;u) ⇒ Colinear(c;x;v) ⇒ Ruxv)
10. a ≠ x
11. Raxc
12. Rbxc
13. Point
14. c ≠ x
15. c' : Point
16. c-x-c'
17. xc' ≅ cx
18. ∀c':Point. (c'=x=c ⇒ ac ≅ ac')
19. c'=x=c
20. ac ≅ ac'
21. c1 : Point
22. c-a-c1
23. ac1 ≅ ca
24. c' # c1a
25. c1=a=c
26. p : Point
27. c'=p=c1
28. c=a=c1
⊢ c=x=c'
3
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. c # ba
7. Colinear(a;b;x)
8. Colinear(c;x;x)
9. ∀u,v:Point. (Colinear(a;b;u) ⇒ Colinear(c;x;v) ⇒ Ruxv)
10. a ≠ x
11. Raxc
12. Rbxc
13. Point
14. c ≠ x
15. c' : Point
16. c-x-c'
17. xc' ≅ cx
18. ∀c':Point. (c'=x=c ⇒ ac ≅ ac')
19. c'=x=c
20. ac ≅ ac'
21. c1 : Point
22. c-a-c1
23. ac1 ≅ ca
24. c' # c1a
25. c1=a=c
26. p : Point
27. c'=p=c1
28. c=a=c1
29. c=x=c'
30. c'a ≅ ca
31. c' # c1a
32. a # cc'
⊢ c1=p=c'
4
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. c # ba
7. Colinear(a;b;x)
8. Colinear(c;x;x)
9. ∀u,v:Point. (Colinear(a;b;u) ⇒ Colinear(c;x;v) ⇒ Ruxv)
10. a ≠ x
11. Raxc
12. Rbxc
13. Point
14. c ≠ x
15. c' : Point
16. c-x-c'
17. xc' ≅ cx
18. ∀c':Point. (c'=x=c ⇒ ac ≅ ac')
19. c'=x=c
20. ac ≅ ac'
21. c1 : Point
22. c-a-c1
23. ac1 ≅ ca
24. c' # c1a
25. c1=a=c
26. p : Point
27. c'=p=c1
28. c=a=c1
29. c=x=c'
30. c'a ≅ ca
31. c' # c1a
32. a # cc'
33. c1=p=c'
⊢ ab ⊥a pa
5
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. c # ba
7. Colinear(a;b;x)
8. Colinear(c;x;x)
9. ∀u,v:Point. (Colinear(a;b;u) ⇒ Colinear(c;x;v) ⇒ Ruxv)
10. a ≠ x
11. Raxc
12. Rbxc
13. Point
14. c ≠ x
15. c' : Point
16. c-x-c'
17. xc' ≅ cx
18. ∀c':Point. (c'=x=c ⇒ ac ≅ ac')
19. c'=x=c
20. ac ≅ ac'
21. c1 : Point
22. c-a-c1
23. ac1 ≅ ca
24. c' # c1a
25. c1=a=c
26. p : Point
27. c'=p=c1
28. c=a=c1
29. c=x=c'
30. c'a ≅ ca
31. c' # c1a
32. a # cc'
33. c1=p=c'
34. ab ⊥a pa
⊢ p # ab
Latex:
Latex:
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. c \# ba
7. Colinear(a;b;x)
8. Colinear(c;x;x)
9. \mforall{}u,v:Point. (Colinear(a;b;u) {}\mRightarrow{} Colinear(c;x;v) {}\mRightarrow{} Ruxv)
10. a \mneq{} x
11. Raxc
12. Rbxc
13. Point
14. c \mneq{} x
15. c' : Point
16. c-x-c'
17. xc' \00D0 cx
18. \mforall{}c':Point. (c'=x=c {}\mRightarrow{} ac \00D0 ac')
19. c'=x=c
20. ac \00D0 ac'
21. c1 : Point
22. c-a-c1
23. ac1 \00D0 ca
24. c' \# c1a
\mvdash{} \mexists{}c1,c',p:Point
(((c=a=c1 \mwedge{} c=x=c') \mwedge{} c'a \00D0 ca) \mwedge{} c' \# c1a \mwedge{} ((a \# cc' \mwedge{} c1=p=c') \mwedge{} ab \mbot{}a pa) \mwedge{} p \# ab)
By
Latex:
(((Assert c1=a=c BY (D 0 THEN Auto)) THEN InstConcl [\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{} THEN Auto)
THEN ((InstLemma`geo-congruent-mid-exists` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{} THEN Auto)
THEN ExRepD
THEN RenameVar `p' (26))
THEN InstConcl [\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index