---

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


1. b : ℕ
2. k : ℤ
3. a : ℕ
4. ∀a:ℕb. ∀b:ℕ.  (((((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ) ⇒ (k = 3 ∈ ℤ))
5. (((b * b) + (b * b)) + 1) = (k * b * b) ∈ ℤ
6. b ≤ b
7. 0 ≤ (b * b)
8. 0 ≤ (b * b)
9. ¬(b = 0 ∈ ℤ)
10. ¬(b = 0 ∈ ℤ)
11. 0 ≤ k
12. v : ℤ
13. ((k * b) - b) = v ∈ ℤ
14. (((b * b) + (v * v)) + 1) = (k * b * v) ∈ ℤ
15. (b * v) = ((b * b) + 1) ∈ ℤ
16. 0 ≤ v
17. ¬v < b
18. ¬((b + 1) ≤ b)
19. a = b ∈ ℤ
20. ((k - 2) * b * b) = 1 ∈ ℤ
⊢ k = 3 ∈ ℤ
BY
{ ((Lemmaize [-1] THEN Auto)
   THEN (CaseNat 0 `b'
         THENL [(Eliminate ⌜b⌝⋅ THEN Auto); (CaseNat 1 `b' THENL [(Eliminate ⌜b⌝⋅ THEN Auto); (Assert 2 ≤ b BY Auto)])]
        )
   ) }

1
1. b : ℕ
2. k : ℤ
3. ((k - 2) * b * b) = 1 ∈ ℤ
4. ¬(b = 0 ∈ ℤ)
5. ¬(b = 1 ∈ ℤ)
6. 2 ≤ b
⊢ k = 3 ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
((Lemmaize  [-1]  THEN  Auto)
  THEN  (CaseNat  0  `b'
              THENL  [(Eliminate  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto)
                          ;  (CaseNat  1  `b'  THENL  [(Eliminate  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto);  (Assert  2  \mleq{}  b  BY  Auto)])]
            )
  )

---

Home Index