---

Step * 1 of Lemma p2J_wf


1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. p2J(a;b) ∈ ℝ^3
5. i : ℕ3
6. j : ℕ3
7. (a i) * (b j) ≠ (a j) * (b i)
⊢ ∃k:ℕ3. p2J(a;b) k ≠ r0
BY
{ (RepUR ``p2J`` 0
   THEN RepeatFor 2 (IntSegCases (-3))
   THEN Eliminate ⌜i⌝⋅
   THEN Eliminate ⌜j⌝⋅
   THEN Try ((Assert ⌜False⌝⋅ THEN Auto THEN D -3 THEN Complete (Auto)))) }

1
1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. p2J(a;b) ∈ ℝ^3
5. i : ℤ
6. j : ℤ
7. (a 0) * (b 1) ≠ (a 1) * (b 0)
8. i = 0 ∈ ℤ
9. j = 1 ∈ ℤ
⊢ ∃k:ℕ3
   if (k =z 0) then ((a 1) * (b 2)) - (b 1) * (a 2)
   if (k =z 1) then ((a 2) * (b 0)) - (b 2) * (a 0)
   else ((a 1) * (b 0)) - (b 1) * (a 0)
   fi  ≠ r0

2
1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. p2J(a;b) ∈ ℝ^3
5. i : ℤ
6. j : ℤ
7. (a 0) * (b 2) ≠ (a 2) * (b 0)
8. i = 0 ∈ ℤ
9. j = 2 ∈ ℤ
⊢ ∃k:ℕ3
   if (k =z 0) then ((a 1) * (b 2)) - (b 1) * (a 2)
   if (k =z 1) then ((a 2) * (b 0)) - (b 2) * (a 0)
   else ((a 1) * (b 0)) - (b 1) * (a 0)
   fi  ≠ r0

3
1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. p2J(a;b) ∈ ℝ^3
5. i : ℤ
6. j : ℤ
7. (a 1) * (b 0) ≠ (a 0) * (b 1)
8. i = 1 ∈ ℤ
9. j = 0 ∈ ℤ
⊢ ∃k:ℕ3
   if (k =z 0) then ((a 1) * (b 2)) - (b 1) * (a 2)
   if (k =z 1) then ((a 2) * (b 0)) - (b 2) * (a 0)
   else ((a 1) * (b 0)) - (b 1) * (a 0)
   fi  ≠ r0

4
1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. p2J(a;b) ∈ ℝ^3
5. i : ℤ
6. j : ℤ
7. (a 1) * (b 2) ≠ (a 2) * (b 1)
8. i = 1 ∈ ℤ
9. j = 2 ∈ ℤ
⊢ ∃k:ℕ3
   if (k =z 0) then ((a 1) * (b 2)) - (b 1) * (a 2)
   if (k =z 1) then ((a 2) * (b 0)) - (b 2) * (a 0)
   else ((a 1) * (b 0)) - (b 1) * (a 0)
   fi  ≠ r0

5
1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. p2J(a;b) ∈ ℝ^3
5. i : ℤ
6. j : ℤ
7. (a 2) * (b 0) ≠ (a 0) * (b 2)
8. i = 2 ∈ ℤ
9. j = 0 ∈ ℤ
⊢ ∃k:ℕ3
   if (k =z 0) then ((a 1) * (b 2)) - (b 1) * (a 2)
   if (k =z 1) then ((a 2) * (b 0)) - (b 2) * (a 0)
   else ((a 1) * (b 0)) - (b 1) * (a 0)
   fi  ≠ r0

6
1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. p2J(a;b) ∈ ℝ^3
5. i : ℤ
6. j : ℤ
7. (a 2) * (b 1) ≠ (a 1) * (b 2)
8. i = 2 ∈ ℤ
9. j = 1 ∈ ℤ
⊢ ∃k:ℕ3
   if (k =z 0) then ((a 1) * (b 2)) - (b 1) * (a 2)
   if (k =z 1) then ((a 2) * (b 0)) - (b 2) * (a 0)
   else ((a 1) * (b 0)) - (b 1) * (a 0)
   fi  ≠ r0

---

Latex:

---

Latex:

1.  a  :  \mBbbP{}\^{}2
2.  b  :  \mBbbP{}\^{}2
3.  a  \mneq{}  b
4.  p2J(a;b)  \mmember{}  \mBbbR{}\^{}3
5.  i  :  \mBbbN{}3
6.  j  :  \mBbbN{}3
7.  (a  i)  *  (b  j)  \mneq{}  (a  j)  *  (b  i)
\mvdash{}  \mexists{}k:\mBbbN{}3.  p2J(a;b)  k  \mneq{}  r0


By

---

Latex:
(RepUR  ``p2J``  0
  THEN  RepeatFor  2  (IntSegCases  (-3))
  THEN  Eliminate  \mkleeneopen{}i\mkleeneclose{}\mcdot{}
  THEN  Eliminate  \mkleeneopen{}j\mkleeneclose{}\mcdot{}
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  D  -3  THEN  Complete  (Auto))))

---

Home Index