---

Step * 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
⊢ k = 3 ∈ ℤ
BY
{ ((Assert (0 ≤ (a * a)) ∧ (0 ≤ (b * b)) BY
          Auto)
   THEN (CaseNat 0 `a'
         THENL [(Eliminate ⌜a⌝⋅ THEN Auto)
               ; (CaseNat 0 `b' THENL [(Eliminate ⌜b⌝⋅ THEN Auto); (Assert 0 ≤ k BY (Mul ⌜a * b⌝ 0⋅ 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)) ∧ (0 ≤ (b * b))
8. ¬(a = 0 ∈ ℤ)
9. ¬(b = 0 ∈ ℤ)
10. 0 ≤ k
⊢ 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
\mvdash{}  k  =  3


By

---

Latex:
((Assert  (0  \mleq{}  (a  *  a))  \mwedge{}  (0  \mleq{}  (b  *  b))  BY
                Auto)
  THEN  (CaseNat  0  `a'
              THENL  [(Eliminate  \mkleeneopen{}a\mkleeneclose{}\mcdot{}  THEN  Auto)
                          ;  (CaseNat  0  `b'
                                THENL  [(Eliminate  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto);  (Assert  0  \mleq{}  k  BY  (Mul  \mkleeneopen{}a  *  b\mkleeneclose{}  0\mcdot{}  THEN  Auto))]
                          )]
            )
  )

---

Home Index