---

Step * of Lemma Vieta-jumping-example2

∀k:ℤ. ∀a,b:ℕ.  (((((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ) ⇒ (k = 3 ∈ ℤ))
BY
{ ((D 0 THENA Auto)
   THEN CompleteInductionOnNat
   THEN Auto
   THEN ((Decide ⌜b < a⌝⋅ THENA Auto)
         THENL [(InstHyp [⌜b⌝;⌜a⌝] 3⋅ THEN Auto); ((Assert a ≤ b BY Auto) THEN Thin (-2))]
   )) }

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
⊢ k = 3 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}k:\mBbbZ{}.  \mforall{}a,b:\mBbbN{}.    (((((a  *  a)  +  (b  *  b))  +  1)  =  (k  *  a  *  b))  {}\mRightarrow{}  (k  =  3))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  CompleteInductionOnNat
  THEN  Auto
  THEN  ((Decide  \mkleeneopen{}b  <  a\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [(InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  3\mcdot{}  THEN  Auto);  ((Assert  a  \mleq{}  b  BY  Auto)  THEN  Thin  (-2))]
  ))

---

Home Index