Step
*
1
1
1
1
2
1
1
of Lemma
AX3
1. e : EuclideanParPlane@i'
2. l2 : Line@i
3. p1 : Point@i
4. l4 : n:{n:Line| p1 I n} × p1 # l2@i
5. l1 : Line@i
6. p : Point@i
7. m2 : n:{n:Line| p I n} × p # l1@i
8. p2 : Point@i
9. l : Line@i
10. n : Line@i
11. P4 : p2 I n@i
12. P5 : p2 # l@i
13. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
14. l \/ l1
15. ∀x:{x:Point| x I l ∧ x I n} . x # l1
16. ∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n))
17. l \/ l2
18. l2 \/ n
19. l2 \/ l
20. l2 \/ l1
⊢ ∃P:P_point(e). ((¬P_point-line-sep(e;P;<l2, p1, l4>)) ∧ (¬P_point-line-sep(e;P;<l1, p, m2>)))
BY
{ ((((InstLemma `geo-intersect-lines-iff` [⌜e⌝;⌜l1⌝;⌜l2⌝]⋅ THEN EAuto 1) THEN ExRepD) THEN D -2 THEN EAuto 1)
THEN (Unfold `geo-line-sep` -2 THEN ExRepD)
THEN (((Assert p3 I l1 BY EAuto 1) THEN (Assert p3 # l2 BY Auto)) THEN RenameVar `S1' (-2) THEN RenameVar `S2' (-1))
THEN (D 0 With ⌜<p3, l2, l1, S1, S2>⌝ THEN Auto)
THEN Unfold `P_point-line-sep` 0
THEN Reduce 0
THEN (D 0 THENA Auto)
THEN D -1
THEN D -2) }
1
1. e : EuclideanParPlane@i'
2. l2 : Line@i
3. p1 : Point@i
4. l4 : n:{n:Line| p1 I n} × p1 # l2@i
5. l1 : Line@i
6. p : Point@i
7. m2 : n:{n:Line| p I n} × p # l1@i
8. p2 : Point@i
9. l : Line@i
10. n : Line@i
11. P4 : p2 I n@i
12. P5 : p2 # l@i
13. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
14. l \/ l1
15. ∀x:{x:Point| x I l ∧ x I n} . x # l1
16. ∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n))
17. l \/ l2
18. l2 \/ n
19. l2 \/ l
20. l2 \/ l1
21. l1 \/ l2 ⇐ (l1 # l2) ∧ (∃x:Point. (x I l1 ∧ x I l2))
22. p3 : Point
23. Colinear(p3;fst(l1);fst(snd(l1)))
24. p3 # fst(l2)fst(snd(l2))
25. x : Point
26. x I l1
27. x I l2
28. S1 : p3 I l1
29. S2 : p3 # l2
30. l2 \/ l2
31. ∀x:{x:Point| x I l2 ∧ x I l1} . x # l2
⊢ False
2
1. e : EuclideanParPlane@i'
2. l2 : Line@i
3. p1 : Point@i
4. l4 : n:{n:Line| p1 I n} × p1 # l2@i
5. l1 : Line@i
6. p : Point@i
7. m2 : n:{n:Line| p I n} × p # l1@i
8. p2 : Point@i
9. l : Line@i
10. n : Line@i
11. P4 : p2 I n@i
12. P5 : p2 # l@i
13. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
14. l \/ l1
15. ∀x:{x:Point| x I l ∧ x I n} . x # l1
16. ∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n))
17. l \/ l2
18. l2 \/ n
19. l2 \/ l
20. l2 \/ l1
21. l1 \/ l2 ⇐ (l1 # l2) ∧ (∃x:Point. (x I l1 ∧ x I l2))
22. p3 : Point
23. Colinear(p3;fst(l1);fst(snd(l1)))
24. p3 # fst(l2)fst(snd(l2))
25. x : Point
26. x I l1
27. x I l2
28. S1 : p3 I l1
29. S2 : p3 # l2
30. l1 \/ l2
31. ∀x:{x:Point| x I l2 ∧ x I l1} . x # l2
⊢ False
3
1. e : EuclideanParPlane@i'
2. l2 : Line@i
3. p1 : Point@i
4. l4 : n:{n:Line| p1 I n} × p1 # l2@i
5. l1 : Line@i
6. p : Point@i
7. m2 : n:{n:Line| p I n} × p # l1@i
8. p2 : Point@i
9. l : Line@i
10. n : Line@i
11. P4 : p2 I n@i
12. P5 : p2 # l@i
13. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
14. l \/ l1
15. ∀x:{x:Point| x I l ∧ x I n} . x # l1
16. ∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n))
17. l \/ l2
18. l2 \/ n
19. l2 \/ l
20. l2 \/ l1
21. l1 \/ l2 ⇐ (l1 # l2) ∧ (∃x:Point. (x I l1 ∧ x I l2))
22. p3 : Point
23. Colinear(p3;fst(l1);fst(snd(l1)))
24. p3 # fst(l2)fst(snd(l2))
25. x : Point
26. x I l1
27. x I l2
28. S1 : p3 I l1
29. S2 : p3 # l2
30. ¬P_point-line-sep(e;<p3, l2, l1, S1, S2>;<l2, p1, l4>)
31. l2 \/ l1
32. ∀x:{x:Point| x I l2 ∧ x I l1} . x # l1
⊢ False
4
1. e : EuclideanParPlane@i'
2. l2 : Line@i
3. p1 : Point@i
4. l4 : n:{n:Line| p1 I n} × p1 # l2@i
5. l1 : Line@i
6. p : Point@i
7. m2 : n:{n:Line| p I n} × p # l1@i
8. p2 : Point@i
9. l : Line@i
10. n : Line@i
11. P4 : p2 I n@i
12. P5 : p2 # l@i
13. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
14. l \/ l1
15. ∀x:{x:Point| x I l ∧ x I n} . x # l1
16. ∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n))
17. l \/ l2
18. l2 \/ n
19. l2 \/ l
20. l2 \/ l1
21. l1 \/ l2 ⇐ (l1 # l2) ∧ (∃x:Point. (x I l1 ∧ x I l2))
22. p3 : Point
23. Colinear(p3;fst(l1);fst(snd(l1)))
24. p3 # fst(l2)fst(snd(l2))
25. x : Point
26. x I l1
27. x I l2
28. S1 : p3 I l1
29. S2 : p3 # l2
30. ¬P_point-line-sep(e;<p3, l2, l1, S1, S2>;<l2, p1, l4>)
31. l1 \/ l1
32. ∀x:{x:Point| x I l2 ∧ x I l1} . x # l1
⊢ False
Latex:
Latex:
1. e : EuclideanParPlane@i'
2. l2 : Line@i
3. p1 : Point@i
4. l4 : n:\{n:Line| p1 I n\} \mtimes{} p1 \# l2@i
5. l1 : Line@i
6. p : Point@i
7. m2 : n:\{n:Line| p I n\} \mtimes{} p \# l1@i
8. p2 : Point@i
9. l : Line@i
10. n : Line@i
11. P4 : p2 I n@i
12. P5 : p2 \# l@i
13. \mneg{}((l \mbackslash{}/ l2 \mvee{} n \mbackslash{}/ l2) \mwedge{} (\mforall{}x:\{x:Point| x I l \mwedge{} x I n\} . x \# l2))
14. l \mbackslash{}/ l1
15. \mforall{}x:\{x:Point| x I l \mwedge{} x I n\} . x \# l1
16. \mforall{}l,m,n:Line. (l \mbackslash{}/ m {}\mRightarrow{} (l \mbackslash{}/ n \mvee{} m \mbackslash{}/ n))
17. l \mbackslash{}/ l2
18. l2 \mbackslash{}/ n
19. l2 \mbackslash{}/ l
20. l2 \mbackslash{}/ l1
\mvdash{} \mexists{}P:P\_point(e). ((\mneg{}P\_point-line-sep(e;P;<l2, p1, l4>)) \mwedge{} (\mneg{}P\_point-line-sep(e;P;<l1, p, m2>)))
By
Latex:
((((InstLemma `geo-intersect-lines-iff` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}l2\mkleeneclose{}]\mcdot{} THEN EAuto 1) THEN ExRepD)
THEN D -2
THEN EAuto 1)
THEN (Unfold `geo-line-sep` -2 THEN ExRepD)
THEN (((Assert p3 I l1 BY EAuto 1) THEN (Assert p3 \# l2 BY Auto))
THEN RenameVar `S1' (-2)
THEN RenameVar `S2' (-1))
THEN (D 0 With \mkleeneopen{}<p3, l2, l1, S1, S2>\mkleeneclose{} THEN Auto)
THEN Unfold `P\_point-line-sep` 0
THEN Reduce 0
THEN (D 0 THENA Auto)
THEN D -1
THEN D -2)
Home
Index