---

Step * of Lemma twosquareinv-fixpoint

No Annotations
∀p:{p:{2...}| prime(p)} . ∀t:x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} .
  ((twosquareinv(t) = t ∈ (ℕ × ℕ × ℕ)) ⇒ (t ~ <1, 1, (p - 1) ÷ 4>))
BY
{ ((Auto THEN Try ((DoSubsume THEN Auto)))
   THEN DProds
   THEN RenameVar `z' (-2)
   THEN D -2
   THEN (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))
   THEN (Assert ¬(z = 0 ∈ ℤ) BY
               ((D 0 THENA Auto)
                THEN D 1
                THEN Unhide
                THEN (InstLemma `not-prime-square` [⌜x⌝]⋅ THENA Auto)
                THEN D -1
                THEN NthHypSq 2
                THEN Auto))
   THEN MoveToConcl (-3)
   THEN RepUR ``twosquareinv`` 0
   THEN Repeat (AutoSplit)
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 ((EqHD (-1) THEN All Reduce THEN Auto))) }

1
1. p : {p:{2...}| prime(p)} 
2. x : ℕ
3. y : ℕ
4. z : ℕ
5. ¬x < y - z
6. ((x * x) + (4 * y * z)) = p ∈ ℤ
7. ¬(x = 0 ∈ ℤ)
8. ¬(z = 0 ∈ ℤ)
9. x < y + y
10. ((y + y) - x) = x ∈ ℕ
11. y = y ∈ ℕ
12. ((x - y) + z) = z ∈ ℕ
⊢ <x, y, z> = <1, 1, (p - 1) ÷ 4> ∈ (x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} )

---

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(t)  =  t)  {}\mRightarrow{}  (t  \msim{}  ə,  1,  (p  -  1)  \mdiv{}  4>))


By

---

Latex:
((Auto  THEN  Try  ((DoSubsume  THEN  Auto)))
  THEN  DProds
  THEN  RenameVar  `z'  (-2)
  THEN  D  -2
  THEN  (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))
  THEN  (Assert  \mneg{}(z  =  0)  BY
                          ((D  0  THENA  Auto)
                            THEN  D  1
                            THEN  Unhide
                            THEN  (InstLemma  `not-prime-square`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  D  -1
                            THEN  NthHypSq  2
                            THEN  Auto))
  THEN  MoveToConcl  (-3)
  THEN  RepUR  ``twosquareinv``  0
  THEN  Repeat  (AutoSplit)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  ((EqHD  (-1)  THEN  All  Reduce  THEN  Auto)))

---

Home Index