---

Step * 1 1 1 of Lemma Vieta-jumping-example2


1. k : ℤ
2. a : ℕ
3. ∀a:ℕa. ∀b:ℕ.  (((((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ) ⇒ (k = 3 ∈ ℤ))
4. b : ℕ
5. (((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ
6. a ≤ b
7. 0 ≤ (a * a)
8. 0 ≤ (b * b)
9. ¬(a = 0 ∈ ℤ)
10. ¬(b = 0 ∈ ℤ)
11. 0 ≤ k
12. v : ℤ
13. ((k * a) - b) = v ∈ ℤ
14. (((a * a) + (v * v)) + 1) = (k * a * v) ∈ ℤ
15. (b * v) = ((a * a) + 1) ∈ ℤ
⊢ k = 3 ∈ ℤ
BY
{ (Assert 0 ≤ v BY
         (Mul ⌜b⌝ 0⋅ THEN Auto)) }

1
1. k : ℤ
2. a : ℕ
3. ∀a:ℕa. ∀b:ℕ.  (((((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ) ⇒ (k = 3 ∈ ℤ))
4. b : ℕ
5. (((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ
6. a ≤ b
7. 0 ≤ (a * a)
8. 0 ≤ (b * b)
9. ¬(a = 0 ∈ ℤ)
10. ¬(b = 0 ∈ ℤ)
11. 0 ≤ k
12. v : ℤ
13. ((k * a) - b) = v ∈ ℤ
14. (((a * a) + (v * v)) + 1) = (k * a * v) ∈ ℤ
15. (b * v) = ((a * a) + 1) ∈ ℤ
16. 0 ≤ v
⊢ k = 3 ∈ ℤ

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  a  :  \mBbbN{}
3.  \mforall{}a:\mBbbN{}a.  \mforall{}b:\mBbbN{}.    (((((a  *  a)  +  (b  *  b))  +  1)  =  (k  *  a  *  b))  {}\mRightarrow{}  (k  =  3))
4.  b  :  \mBbbN{}
5.  (((a  *  a)  +  (b  *  b))  +  1)  =  (k  *  a  *  b)
6.  a  \mleq{}  b
7.  0  \mleq{}  (a  *  a)
8.  0  \mleq{}  (b  *  b)
9.  \mneg{}(a  =  0)
10.  \mneg{}(b  =  0)
11.  0  \mleq{}  k
12.  v  :  \mBbbZ{}
13.  ((k  *  a)  -  b)  =  v
14.  (((a  *  a)  +  (v  *  v))  +  1)  =  (k  *  a  *  v)
15.  (b  *  v)  =  ((a  *  a)  +  1)
\mvdash{}  k  =  3


By

---

Latex:
(Assert  0  \mleq{}  v  BY
              (Mul  \mkleeneopen{}b\mkleeneclose{}  0\mcdot{}  THEN  Auto))

---

Home Index