---

Step * 2 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 * a) + (b * b)) ∈ ℤ
⊢ (p = 2 ∈ ℤ) ∨ (∃k:ℤ. (p = (1 + (4 * k)) ∈ ℤ))
BY
{ ((Subst' (a * a) + (b * b) ~ (|a| * |a|) + (|b| * |b|) -1 THENA (EqCD THEN Auto))
   THEN ((InstLemma `div_rem_sum` [⌜|a|⌝;⌜2⌝]⋅ THENA Auto) THEN HypSubst' (-1) (-2) THEN Thin (-1))
   THEN (InstLemma `div_rem_sum` [⌜|b|⌝;⌜2⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) (-2)
   THEN Thin (-1)) }

1
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)) ∈ ℤ))

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst'  (a  *  a)  +  (b  *  b)  \msim{}  (|a|  *  |a|)  +  (|b|  *  |b|)  -1  THENA  (EqCD  THEN  Auto))
  THEN  ((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}|a|\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  HypSubst'  (-1)  (-2)  THEN  Thin  (-1))
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}|b|\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  (-2)
  THEN  Thin  (-1))

---

Home Index