Step
*
1
1
2
2
1
1
1
1
of Lemma
rv-be-inner-trans
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. a_b_d
6. a ≠ b
7. b ≠ c
8. ¬a-b-c
9. ¬a-b-d
10. req-vec(2;b;d)
11. c ≠ d
12. d ≠ c
13. c ≠ d
⊢ ¬d-c-d
BY
{ ((D 0 THENA Auto) THEN D -1) }
1
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. a_b_d
6. a ≠ b
7. b ≠ c
8. ¬a-b-c
9. ¬a-b-d
10. req-vec(2;b;d)
11. c ≠ d
12. d ≠ c
13. c ≠ d
14. d-c-d
15. d ≠ d
⊢ False
Latex:
Latex:
1. a : \mBbbR{}\^{}2
2. b : \mBbbR{}\^{}2
3. c : \mBbbR{}\^{}2
4. d : \mBbbR{}\^{}2
5. a\_b\_d
6. a \mneq{} b
7. b \mneq{} c
8. \mneg{}a-b-c
9. \mneg{}a-b-d
10. req-vec(2;b;d)
11. c \mneq{} d
12. d \mneq{} c
13. c \mneq{} d
\mvdash{} \mneg{}d-c-d
By
Latex:
((D 0 THENA Auto) THEN D -1)
Home
Index