---

Step * 2 1 1 of Lemma prime-sum-of-two-squares-iff-one-mod-four


1. p : {p:{2...}| prime(p)} 
2. a : ℤ
3. b : ℤ
4. p
= (((((|a| ÷ 2) * 2) + (|a| rem 2)) * (((|a| ÷ 2) * 2) + (|a| rem 2)))
  + ((((|b| ÷ 2) * 2) + (|b| rem 2)) * (((|b| ÷ 2) * 2) + (|b| rem 2))))
∈ ℤ
⊢ (p = 2 ∈ ℤ) ∨ (∃k:ℤ. (p = (1 + (4 * k)) ∈ ℤ))
BY
{ (MoveToConcl (-1)
   THEN ((GenConcl ⌜(|a| rem 2) = x ∈ ℕ2⌝⋅ THENA Auto) THEN (GenConcl ⌜(|b| rem 2) = y ∈ ℕ2⌝⋅ THENA Auto))
   THEN (GenConcl ⌜(|a| ÷ 2) = z ∈ ℕ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(|b| ÷ 2) = w ∈ ℕ⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. p : {p:{2...}| prime(p)} 
2. x : ℕ2
3. y : ℕ2
4. z : ℕ
5. w : ℕ
⊢ (p = ((((z * 2) + x) * ((z * 2) + x)) + (((w * 2) + y) * ((w * 2) + y))) ∈ ℤ)
⇒ ((p = 2 ∈ ℤ) ∨ (∃k:ℤ. (p = (1 + (4 * k)) ∈ ℤ)))

---

Latex:

---

Latex:

1.  p  :  \{p:\{2...\}|  prime(p)\} 
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  p
=  (((((|a|  \mdiv{}  2)  *  2)  +  (|a|  rem  2))  *  (((|a|  \mdiv{}  2)  *  2)  +  (|a|  rem  2)))
    +  ((((|b|  \mdiv{}  2)  *  2)  +  (|b|  rem  2))  *  (((|b|  \mdiv{}  2)  *  2)  +  (|b|  rem  2))))
\mvdash{}  (p  =  2)  \mvee{}  (\mexists{}k:\mBbbZ{}.  (p  =  (1  +  (4  *  k))))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  ((GenConcl  \mkleeneopen{}(|a|  rem  2)  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (GenConcl  \mkleeneopen{}(|b|  rem  2)  =  y\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}(|a|  \mdiv{}  2)  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(|b|  \mdiv{}  2)  =  w\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index