---

Step * of Lemma twosquareinv_wf

∀[p:{2...}]. ∀[t:x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} ].
  (twosquareinv(t) ∈ x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} )
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[t:x:\mBbbN{}  \mtimes{}  y:\mBbbN{}  \mtimes{}  \{z:\mBbbN{}|  ((x  *  x)  +  (4  *  y  *  z))  =  p\}  ].
    (twosquareinv(t)  \mmember{}  x:\mBbbN{}  \mtimes{}  y:\mBbbN{}  \mtimes{}  \{z:\mBbbN{}|  ((x  *  x)  +  (4  *  y  *  z))  =  p\}  )


By

---

Latex:
ProveWfLemma

---

Home Index