---

Step * 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 ∈ ℤ
⊢ twosquareinv(twosquareinv(<x, y, z>)) ~ <x, y, z>
BY
{ (Assert ¬(x = 0 ∈ ℤ) BY
         ((D 0 THENA Auto)
          THEN D 1
          THEN Unhide
          THEN (InstLemma `not-prime-mult` [⌜2⌝;⌜2⌝;⌜y * z⌝]⋅ THENA Auto)
          THEN D -1
          THEN NthHypSq 2
          THEN Auto)) }

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

---

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
\mvdash{}  twosquareinv(twosquareinv(<x,  y,  z>))  \msim{}  <x,  y,  z>


By

---

Latex:
(Assert  \mneg{}(x  =  0)  BY
              ((D  0  THENA  Auto)
                THEN  D  1
                THEN  Unhide
                THEN  (InstLemma  `not-prime-mult`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}y  *  z\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  NthHypSq  2
                THEN  Auto))

---

Home Index