---

Step * 2 of Lemma olympiad-problem-six


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) ∈ ℤ)
BY
{ ((Assert 0 ≤ (a * a) BY
          Auto)
   THEN (Assert 0 ≤ (b * b) BY
               Auto)
   THEN (Assert 0 ≤ k BY
               (Mul ⌜(a * b) + 1⌝ 0⋅ THEN Auto))
   THEN ((Decide ⌜k = 0 ∈ ℤ⌝⋅ THENA Auto)
         THENL [(D 0 With ⌜0⌝  THEN Auto)
               ; ((Assert ((((k * a) - b) * ((k * a) - b)) + (a * a)) = (k * ((((k * a) - b) * a) + 1)) ∈ ℤ BY
                         Auto)
                  THEN (Assert (b * ((k * a) - b)) = ((a * a) - k) ∈ ℤ 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)) = (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 ∈ ℤ)
8. 0 ≤ (a * a)
9. 0 ≤ (b * b)
10. 0 ≤ k
11. ¬(k = 0 ∈ ℤ)
12. v : ℤ
13. ((k * a) - b) = v ∈ ℤ
14. ((v * v) + (a * a)) = (k * ((v * a) + 1)) ∈ ℤ
15. (b * v) = ((a * a) - k) ∈ ℤ
⊢ ∃n:ℤ. (k = (n * n) ∈ ℤ)

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  a  :  \mBbbN{}
3.  \mforall{}a:\mBbbN{}a.  \mforall{}b:\mBbbN{}.    ((((a  *  a)  +  (b  *  b))  =  (k  *  ((a  *  b)  +  1)))  {}\mRightarrow{}  (\mexists{}n:\mBbbZ{}.  (k  =  (n  *  n))))
4.  b  :  \mBbbN{}
5.  ((a  *  a)  +  (b  *  b))  =  (k  *  ((a  *  b)  +  1))
6.  \mneg{}b  <  a
7.  \mneg{}(a  =  0)
\mvdash{}  \mexists{}n:\mBbbZ{}.  (k  =  (n  *  n))


By

---

Latex:
((Assert  0  \mleq{}  (a  *  a)  BY
                Auto)
  THEN  (Assert  0  \mleq{}  (b  *  b)  BY
                          Auto)
  THEN  (Assert  0  \mleq{}  k  BY
                          (Mul  \mkleeneopen{}(a  *  b)  +  1\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  ((Decide  \mkleeneopen{}k  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [(D  0  With  \mkleeneopen{}0\mkleeneclose{}    THEN  Auto)
                          ;  ((Assert  ((((k  *  a)  -  b)  *  ((k  *  a)  -  b))  +  (a  *  a))
                                              =  (k  *  ((((k  *  a)  -  b)  *  a)  +  1))  BY
                                              Auto)
                                THEN  (Assert  (b  *  ((k  *  a)  -  b))  =  ((a  *  a)  -  k)  BY
                                                        Auto)
                                THEN  RepeatFor  2  (MoveToConcl  (-1))
                                THEN  GenConclTerm  \mkleeneopen{}(k  *  a)  -  b\mkleeneclose{}\mcdot{}
                                THEN  Auto)]
  ))

---

Home Index