---

Step * 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)) ∧ (0 ≤ (b * b))
8. ¬(a = 0 ∈ ℤ)
9. ¬(b = 0 ∈ ℤ)
10. 0 ≤ k
⊢ k = 3 ∈ ℤ
BY
{ ((Assert (((a * a) + (((k * a) - b) * ((k * a) - b))) + 1) = (k * a * ((k * a) - b)) ∈ ℤ BY
          Auto)
   THEN (Assert (b * ((k * a) - b)) = ((a * a) + 1) ∈ ℤ BY
               Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerm ⌜(k * a) - b⌝⋅
   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) ∈ ℤ
⊢ 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))  \mwedge{}  (0  \mleq{}  (b  *  b))
8.  \mneg{}(a  =  0)
9.  \mneg{}(b  =  0)
10.  0  \mleq{}  k
\mvdash{}  k  =  3


By

---

Latex:
((Assert  (((a  *  a)  +  (((k  *  a)  -  b)  *  ((k  *  a)  -  b)))  +  1)  =  (k  *  a  *  ((k  *  a)  -  b))  BY
                Auto)
  THEN  (Assert  (b  *  ((k  *  a)  -  b))  =  ((a  *  a)  +  1)  BY
                          Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerm  \mkleeneopen{}(k  *  a)  -  b\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index