---

Step * 1 of Lemma p2J_functionality


1. a1 : ℙ^2
2. b1 : ℙ^2
3. a2 : ℙ^2
4. b2 : ℙ^2
5. a2 ≠ b2
6. m1 : ℝ
7. m1 ≠ r0
8. req-vec(2 + 1;a1;m1*a2)
9. m : ℝ
10. m ≠ r0
11. req-vec(2 + 1;b1;m*b2)
12. a1 ≠ b1
⊢ ↓∃m:{m:ℝ| m ≠ r0} . req-vec(2 + 1;p2J(a1;b1);m*p2J(a2;b2))
BY
{ ((Assert m1 * m ≠ r0 BY Auto) THEN (D 0 THEN D 0 With ⌜m1 * m⌝ ) THEN Auto THEN All Reduce) }

1
1. a1 : ℙ^2
2. b1 : ℙ^2
3. a2 : ℙ^2
4. b2 : ℙ^2
5. a2 ≠ b2
6. m1 : ℝ
7. m1 ≠ r0
8. req-vec(3;a1;m1*a2)
9. m : ℝ
10. m ≠ r0
11. req-vec(3;b1;m*b2)
12. a1 ≠ b1
13. m1 * m ≠ r0
⊢ req-vec(3;p2J(a1;b1);m1 * m*p2J(a2;b2))

---

Latex:

---

Latex:

1.  a1  :  \mBbbP{}\^{}2
2.  b1  :  \mBbbP{}\^{}2
3.  a2  :  \mBbbP{}\^{}2
4.  b2  :  \mBbbP{}\^{}2
5.  a2  \mneq{}  b2
6.  m1  :  \mBbbR{}
7.  m1  \mneq{}  r0
8.  req-vec(2  +  1;a1;m1*a2)
9.  m  :  \mBbbR{}
10.  m  \mneq{}  r0
11.  req-vec(2  +  1;b1;m*b2)
12.  a1  \mneq{}  b1
\mvdash{}  \mdownarrow{}\mexists{}m:\{m:\mBbbR{}|  m  \mneq{}  r0\}  .  req-vec(2  +  1;p2J(a1;b1);m*p2J(a2;b2))


By

---

Latex:
((Assert  m1  *  m  \mneq{}  r0  BY  Auto)  THEN  (D  0  THEN  D  0  With  \mkleeneopen{}m1  *  m\mkleeneclose{}  )  THEN  Auto  THEN  All  Reduce)

---

Home Index