Step
*
1
1
1
1
2
1
2
2
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. l \/ l1
21. l2 \/ n ⇐ (l2 # n) ∧ (∃x:Point. (x I l2 ∧ x I n))
22. (l2 # n)
23. x : Point
24. x I l2
25. x I n
26. x # l
27. l || n
⊢ False
BY
{ (((InstLemma `common-P_point-parallel-P_lines` [⌜e⌝;⌜<p2, l, n, P4, P5>⌝;⌜<l2, p1, l4>⌝]⋅ THENA Auto) THEN Reduce -1)
THEN EAuto 2
) }
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. l \mbackslash{}/ l1
21. l2 \mbackslash{}/ n \mLeftarrow{}{} (l2 \# n) \mwedge{} (\mexists{}x:Point. (x I l2 \mwedge{} x I n))
22. (l2 \# n)
23. x : Point
24. x I l2
25. x I n
26. x \# l
27. l || n
\mvdash{} False
By
Latex:
(((InstLemma `common-P\_point-parallel-P\_lines` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}<p2, l, n, P4, P5>\mkleeneclose{};\mkleeneopen{}<l2, p1, l4>\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN Reduce -1
)
THEN EAuto 2
)
Home
Index