---

Step * of Lemma twosquareinv-involution

No Annotations
∀p:{p:{2...}| prime(p)} . ∀t:x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} .  (twosquareinv(twosquareinv(t)) ~ t)
BY
{ (Intros THEN DProds THEN D -1 THEN RenameVar `z' (-2)) }

1
1. p : {p:{2...}| prime(p)} 
2. x : ℕ
3. y : ℕ
4. z : ℕ
5. [%1] : ((x * x) + (4 * y * z)) = p ∈ ℤ
⊢ twosquareinv(twosquareinv(<x, y, z>)) ~ <x, y, z>

---

Latex:

---

Latex:
No  Annotations
\mforall{}p:\{p:\{2...\}|  prime(p)\}  .  \mforall{}t:x:\mBbbN{}  \mtimes{}  y:\mBbbN{}  \mtimes{}  \{z:\mBbbN{}|  ((x  *  x)  +  (4  *  y  *  z))  =  p\}  .
    (twosquareinv(twosquareinv(t))  \msim{}  t)


By

---

Latex:
(Intros  THEN  DProds  THEN  D  -1  THEN  RenameVar  `z'  (-2))

---

Home Index