Step
*
1
2
2
1
of Lemma
polynom-equal-iff
1. n : ℤ
2. 0 < n
3. ∀p,q:polynom(n - 1).
((↑poly-zero(n - 1;add-polynom(n - 1;tt;p;minus-polynom(n - 1;q))))
⇒ (p = q ∈ polynom(n - 1)))
4. p : polynom(n - 1) List
5. polyform-lead-nonzero(n;p)
6. q : polynom(n - 1) List
7. polyform-lead-nonzero(n;q)
8. ↑poly-zero(n;add-polynom(n;tt;p;minus-polynom(n;q)))
9. p ∈ polynom(n)
10. q ∈ polynom(n)
⊢ p = q ∈ (polynom(n - 1) List)
BY
{ ((D 5 THENA Auto) THEN (D 6 THENA Auto) THEN Assert ⌜∀q:polynom(n). (||minus-polynom(n;q)|| = ||q|| ∈ ℤ)⌝⋅) }
1
.....assertion.....
1. n : ℤ
2. 0 < n
3. ∀p,q:polynom(n - 1).
((↑poly-zero(n - 1;add-polynom(n - 1;tt;p;minus-polynom(n - 1;q))))
⇒ (p = q ∈ polynom(n - 1)))
4. p : polynom(n - 1) List
5. q : polynom(n - 1) List
6. ↑poly-zero(n;add-polynom(n;tt;p;minus-polynom(n;q)))
7. p ∈ polynom(n)
8. q ∈ polynom(n)
9. 0 < ||p||
⇒ (¬↑poly-zero(n - 1;hd(p)))
10. 0 < ||q||
⇒ (¬↑poly-zero(n - 1;hd(q)))
⊢ ∀q:polynom(n). (||minus-polynom(n;q)|| = ||q|| ∈ ℤ)
2
1. n : ℤ
2. 0 < n
3. ∀p,q:polynom(n - 1).
((↑poly-zero(n - 1;add-polynom(n - 1;tt;p;minus-polynom(n - 1;q))))
⇒ (p = q ∈ polynom(n - 1)))
4. p : polynom(n - 1) List
5. q : polynom(n - 1) List
6. ↑poly-zero(n;add-polynom(n;tt;p;minus-polynom(n;q)))
7. p ∈ polynom(n)
8. q ∈ polynom(n)
9. 0 < ||p||
⇒ (¬↑poly-zero(n - 1;hd(p)))
10. 0 < ||q||
⇒ (¬↑poly-zero(n - 1;hd(q)))
11. ∀q:polynom(n). (||minus-polynom(n;q)|| = ||q|| ∈ ℤ)
⊢ p = q ∈ (polynom(n - 1) List)
Latex:
Latex:
1. n : \mBbbZ{}
2. 0 < n
3. \mforall{}p,q:polynom(n - 1).
((\muparrow{}poly-zero(n - 1;add-polynom(n - 1;tt;p;minus-polynom(n - 1;q)))) {}\mRightarrow{} (p = q))
4. p : polynom(n - 1) List
5. polyform-lead-nonzero(n;p)
6. q : polynom(n - 1) List
7. polyform-lead-nonzero(n;q)
8. \muparrow{}poly-zero(n;add-polynom(n;tt;p;minus-polynom(n;q)))
9. p \mmember{} polynom(n)
10. q \mmember{} polynom(n)
\mvdash{} p = q
By
Latex:
((D 5 THENA Auto)
THEN (D 6 THENA Auto)
THEN Assert \mkleeneopen{}\mforall{}q:polynom(n). (||minus-polynom(n;q)|| = ||q||)\mkleeneclose{}\mcdot{})
Home
Index