---

Step * of Lemma prime-sum-of-two-squares-if-one-mod-four

∀p:{p:{2...}| prime(p)} . ((∃k:ℤ. (p = (1 + (4 * k)) ∈ ℤ)) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
BY
{ (Auto
   THEN ExRepD
   THEN (InstLemma `twosquare-type-finite` [⌜p⌝]⋅ THENA Auto)
   THEN D -1
   THEN (InstLemma `involution-with-unique-fixpoint` [⌜n⌝;⌜x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} ⌝;
         ⌜λ2t.twosquareinv(t)⌝]⋅
         THENA (Auto
                THEN RepeatFor 2 (((FLemma `twosquareinv-fixpoint` [-2] THENA Auto) THEN RWO "-1" 0))
                THEN RevHypSubst (-2) 0
                THEN Auto)
         )) }

1
1. p : {p:{2...}| prime(p)} 
2. k : ℤ
3. p = (1 + (4 * k)) ∈ ℤ
4. n : ℕ
5. x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ}  ~ ℕn
6. (n rem 2) = 1 ∈ ℤ
⇐⇒ ∃x:x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} 
     (twosquareinv(x) = x ∈ (x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} ))
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}p:\{p:\{2...\}|  prime(p)\}  .  ((\mexists{}k:\mBbbZ{}.  (p  =  (1  +  (4  *  k))))  {}\mRightarrow{}  (\mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  (InstLemma  `twosquare-type-finite`  [\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (InstLemma  `involution-with-unique-fixpoint`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x:\mBbbN{}
                                                                                                                  \mtimes{}  y:\mBbbN{}
                                                                                                                  \mtimes{}  \{z:\mBbbN{}|  ((x  *  x)  +  (4  *  y  *  z))  =  p\}  \mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}t.twosquareinv(t)\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  RepeatFor  2  (((FLemma  `twosquareinv-fixpoint`  [-2]  THENA  Auto)  THEN  RWO  "-1"  0))
                            THEN  RevHypSubst  (-2)  0
                            THEN  Auto)
              ))

---

Home Index