Step
*
1
1
1
2
1
1
2
3
of Lemma
rpolynomial-complete-roots-unique
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))
17. ¬(j = (n - 1) ∈ ℤ)
⊢ rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j)
BY
{ (RWO "-2" (-3) 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 - y (n - 1)))
16. (z (n - 1)) = (y (n - 1))
17. ¬(j = (n - 1) ∈ ℤ)
⊢ rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j)
Latex:
Latex:
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)))
16. (z (n - 1)) = (y (n - 1))
17. \mneg{}(j = (n - 1))
\mvdash{} rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j)
By
Latex:
(RWO "-2" (-3) THENA Auto)
Home
Index