---

Step * of Lemma olympiad-problem-six

∀k:ℤ. ∀a,b:ℕ.  ((((a * a) + (b * b)) = (k * ((a * b) + 1)) ∈ ℤ) ⇒ (∃n:ℤ. (k = (n * n) ∈ ℤ)))
BY
{ ((D 0 THENA Auto)
   THEN CompleteInductionOnNat
   THEN Auto
   THEN ((Decide ⌜b < a⌝⋅ THENA Auto) THENL [(InstHyp [⌜b⌝;⌜a⌝] 3⋅ THEN Auto); CaseNat 0 `a'])) }

1
1. k : ℤ
2. a : ℕ
3. ∀a:ℕa. ∀b:ℕ.  ((((a * a) + (b * b)) = (k * ((a * b) + 1)) ∈ ℤ) ⇒ (∃n:ℤ. (k = (n * n) ∈ ℤ)))
4. b : ℕ
5. ((a * a) + (b * b)) = (k * ((a * b) + 1)) ∈ ℤ
6. ¬b < a
7. a = 0 ∈ ℤ
⊢ ∃n:ℤ. (k = (n * n) ∈ ℤ)

2
1. k : ℤ
2. a : ℕ
3. ∀a:ℕa. ∀b:ℕ.  ((((a * a) + (b * b)) = (k * ((a * b) + 1)) ∈ ℤ) ⇒ (∃n:ℤ. (k = (n * n) ∈ ℤ)))
4. b : ℕ
5. ((a * a) + (b * b)) = (k * ((a * b) + 1)) ∈ ℤ
6. ¬b < a
7. ¬(a = 0 ∈ ℤ)
⊢ ∃n:ℤ. (k = (n * n) ∈ ℤ)

---

Latex:

---

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


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);  CaseNat  0  `a']))

---

Home Index