---

Step * 1 1 1 of Lemma twosquareinv-involution


1. p : {p:{2...}| prime(p)} 
2. x : ℕ
3. y : ℕ
4. z : ℕ
5. [%1] : ((x * x) + (4 * y * z)) = p ∈ ℤ
6. ¬(x = 0 ∈ ℤ)
7. ¬(z = 0 ∈ ℤ)
⊢ twosquareinv(twosquareinv(<x, y, z>)) ~ <x, y, z>
BY
{ (RepUR ``twosquareinv`` 0 THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:

1.  p  :  \{p:\{2...\}|  prime(p)\} 
2.  x  :  \mBbbN{}
3.  y  :  \mBbbN{}
4.  z  :  \mBbbN{}
5.  [\%1]  :  ((x  *  x)  +  (4  *  y  *  z))  =  p
6.  \mneg{}(x  =  0)
7.  \mneg{}(z  =  0)
\mvdash{}  twosquareinv(twosquareinv(<x,  y,  z>))  \msim{}  <x,  y,  z>


By

---

Latex:
(RepUR  ``twosquareinv``  0  THEN  Repeat  (AutoSplit))

---

Home Index