Step
*
1
1
1
2
1
1
1
of Lemma
rpolynomial-complete-roots-unique
.....assertion.....
1. x : ℝ
2. n : ℤ
3. 0 < n
4. ∀z,y:ℕn - 1 ⟶ ℝ. ∀j:ℕn - 1.
((∀i,j:ℕn - 1. (i < j ⇒ ((z i) < (z j))))
⇒ (∀i,j:ℕn - 1. (i < j ⇒ ((y i) < (y j))))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
⇒ (∀i:ℕn - 1. (((z i) < x) ∧ ((y i) < x)))
⇒ (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
⇒ ((z j) = (y j)))
5. z : ℕn ⟶ ℝ
6. ∀y:ℕn - 1 ⟶ ℝ. ∀j:ℕn - 1.
((∀i,j:ℕn - 1. (i < j ⇒ ((z i) < (z j))))
⇒ (∀i,j:ℕn - 1. (i < j ⇒ ((y i) < (y j))))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
⇒ (∀i:ℕn - 1. (((z i) < x) ∧ ((y i) < x)))
⇒ (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
⇒ ((z j) = (y j)))
7. y : ℕn ⟶ ℝ
8. ∀j:ℕn - 1
((∀i,j:ℕn - 1. (i < j ⇒ ((z i) < (z j))))
⇒ (∀i,j:ℕn - 1. (i < j ⇒ ((y i) < (y j))))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
⇒ (∀i:ℕn - 1. (((z i) < x) ∧ ((y i) < x)))
⇒ (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
⇒ ((z j) = (y j)))
9. j : ℕn
10. ∀i,j:ℕn. (i < j ⇒ ((z i) < (z j)))
11. ∀i,j:ℕn. (i < j ⇒ ((y i) < (y j)))
12. ∀i:ℕn. (rprod(0;n - 1;j.(z i) - y j) = r0)
13. ∀i:ℕn. (rprod(0;n - 1;j.(y i) - z j) = r0)
14. ∀i:ℕn. (((z i) < x) ∧ ((y i) < x))
15. (rprod(0;n - 1 - 1;j.x - y j) * (x - y (n - 1))) = (rprod(0;n - 1 - 1;j.x - z j) * (x - z (n - 1)))
⊢ (z (n - 1)) = (y (n - 1))
BY
{ ((BLemma `req-iff-not-rneq` THENA Auto) THEN (D 0 THENA Auto)) }
1
1. x : ℝ
2. n : ℤ
3. 0 < n
4. ∀z,y:ℕn - 1 ⟶ ℝ. ∀j:ℕn - 1.
((∀i,j:ℕn - 1. (i < j ⇒ ((z i) < (z j))))
⇒ (∀i,j:ℕn - 1. (i < j ⇒ ((y i) < (y j))))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
⇒ (∀i:ℕn - 1. (((z i) < x) ∧ ((y i) < x)))
⇒ (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
⇒ ((z j) = (y j)))
5. z : ℕn ⟶ ℝ
6. ∀y:ℕn - 1 ⟶ ℝ. ∀j:ℕn - 1.
((∀i,j:ℕn - 1. (i < j ⇒ ((z i) < (z j))))
⇒ (∀i,j:ℕn - 1. (i < j ⇒ ((y i) < (y j))))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
⇒ (∀i:ℕn - 1. (((z i) < x) ∧ ((y i) < x)))
⇒ (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
⇒ ((z j) = (y j)))
7. y : ℕn ⟶ ℝ
8. ∀j:ℕn - 1
((∀i,j:ℕn - 1. (i < j ⇒ ((z i) < (z j))))
⇒ (∀i,j:ℕn - 1. (i < j ⇒ ((y i) < (y j))))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
⇒ (∀i:ℕn - 1. (((z i) < x) ∧ ((y i) < x)))
⇒ (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
⇒ ((z j) = (y j)))
9. j : ℕn
10. ∀i,j:ℕn. (i < j ⇒ ((z i) < (z j)))
11. ∀i,j:ℕn. (i < j ⇒ ((y i) < (y j)))
12. ∀i:ℕn. (rprod(0;n - 1;j.(z i) - y j) = r0)
13. ∀i:ℕn. (rprod(0;n - 1;j.(y i) - z j) = r0)
14. ∀i:ℕn. (((z i) < x) ∧ ((y i) < x))
15. (rprod(0;n - 1 - 1;j.x - y j) * (x - y (n - 1))) = (rprod(0;n - 1 - 1;j.x - z j) * (x - z (n - 1)))
16. z (n - 1) ≠ y (n - 1)
⊢ False
Latex:
Latex:
.....assertion.....
1. x : \mBbbR{}
2. n : \mBbbZ{}
3. 0 < n
4. \mforall{}z,y:\mBbbN{}n - 1 {}\mrightarrow{} \mBbbR{}. \mforall{}j:\mBbbN{}n - 1.
((\mforall{}i,j:\mBbbN{}n - 1. (i < j {}\mRightarrow{} ((z i) < (z j))))
{}\mRightarrow{} (\mforall{}i,j:\mBbbN{}n - 1. (i < j {}\mRightarrow{} ((y i) < (y j))))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. (((z i) < x) \mwedge{} ((y i) < x)))
{}\mRightarrow{} (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
{}\mRightarrow{} ((z j) = (y j)))
5. z : \mBbbN{}n {}\mrightarrow{} \mBbbR{}
6. \mforall{}y:\mBbbN{}n - 1 {}\mrightarrow{} \mBbbR{}. \mforall{}j:\mBbbN{}n - 1.
((\mforall{}i,j:\mBbbN{}n - 1. (i < j {}\mRightarrow{} ((z i) < (z j))))
{}\mRightarrow{} (\mforall{}i,j:\mBbbN{}n - 1. (i < j {}\mRightarrow{} ((y i) < (y j))))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. (((z i) < x) \mwedge{} ((y i) < x)))
{}\mRightarrow{} (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
{}\mRightarrow{} ((z j) = (y j)))
7. y : \mBbbN{}n {}\mrightarrow{} \mBbbR{}
8. \mforall{}j:\mBbbN{}n - 1
((\mforall{}i,j:\mBbbN{}n - 1. (i < j {}\mRightarrow{} ((z i) < (z j))))
{}\mRightarrow{} (\mforall{}i,j:\mBbbN{}n - 1. (i < j {}\mRightarrow{} ((y i) < (y j))))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. (((z i) < x) \mwedge{} ((y i) < x)))
{}\mRightarrow{} (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
{}\mRightarrow{} ((z j) = (y j)))
9. j : \mBbbN{}n
10. \mforall{}i,j:\mBbbN{}n. (i < j {}\mRightarrow{} ((z i) < (z j)))
11. \mforall{}i,j:\mBbbN{}n. (i < j {}\mRightarrow{} ((y i) < (y j)))
12. \mforall{}i:\mBbbN{}n. (rprod(0;n - 1;j.(z i) - y j) = r0)
13. \mforall{}i:\mBbbN{}n. (rprod(0;n - 1;j.(y i) - z j) = r0)
14. \mforall{}i:\mBbbN{}n. (((z i) < x) \mwedge{} ((y i) < x))
15. (rprod(0;n - 1 - 1;j.x - y j) * (x - y (n - 1)))
= (rprod(0;n - 1 - 1;j.x - z j) * (x - z (n - 1)))
\mvdash{} (z (n - 1)) = (y (n - 1))
By
Latex:
((BLemma `req-iff-not-rneq` THENA Auto) THEN (D 0 THENA Auto))
Home
Index