---

Step * 1 1 1 1 2 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) ∈ ℤ
16. 0 ≤ v
17. ¬v < a
18. (a + 1) ≤ b
19. (a * (a + 1)) ≤ (a * b)
20. a ≤ v
21. (b * a) ≤ (b * v)
⊢ k = 3 ∈ ℤ
BY
{ ((Assert a = 1 ∈ ℤ BY Auto) THEN Eliminate ⌜a⌝⋅) }

1
1. k : ℤ
2. a : ℕ
3. ∀a:ℕ1. ∀b:ℕ.  (((((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ) ⇒ (k = 3 ∈ ℤ))
4. b : ℕ
5. (((1 * 1) + (b * b)) + 1) = (k * 1 * b) ∈ ℤ
6. 1 ≤ b
7. 0 ≤ (1 * 1)
8. 0 ≤ (b * b)
9. ¬(1 = 0 ∈ ℤ)
10. ¬(b = 0 ∈ ℤ)
11. 0 ≤ k
12. v : ℤ
13. ((k * 1) - b) = v ∈ ℤ
14. (((1 * 1) + (v * v)) + 1) = (k * 1 * v) ∈ ℤ
15. (b * v) = ((1 * 1) + 1) ∈ ℤ
16. 0 ≤ v
17. ¬v < 1
18. (1 + 1) ≤ b
19. (1 * (1 + 1)) ≤ (1 * b)
20. 1 ≤ v
21. (b * 1) ≤ (b * v)
22. a = 1 ∈ ℤ
⊢ 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)
16.  0  \mleq{}  v
17.  \mneg{}v  <  a
18.  (a  +  1)  \mleq{}  b
19.  (a  *  (a  +  1))  \mleq{}  (a  *  b)
20.  a  \mleq{}  v
21.  (b  *  a)  \mleq{}  (b  *  v)
\mvdash{}  k  =  3


By

---

Latex:
((Assert  a  =  1  BY  Auto)  THEN  Eliminate  \mkleeneopen{}a\mkleeneclose{}\mcdot{})

---

Home Index