---

Step * 1 1 1 1 1 1 of Lemma prime-sum-of-two-squares


1. p : Prime
2. a : ℤ
3. (2 * |a|) ≤ p
4. b : ℤ
5. (2 * |b|) ≤ p
6. ((|a| * |a|) + (|b| * |b|)) ≡ 0 mod p
7. ¬((|a| ≡ 0 mod p) ∧ (|b| ≡ 0 mod p))
8. p = 2 ∈ ℤ
⊢ ∃a,b:ℤ. (2 = ((a * a) + (b * b)) ∈ ℤ)
BY
{ (InstConcl [⌜1⌝;⌜1⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  Prime
2.  a  :  \mBbbZ{}
3.  (2  *  |a|)  \mleq{}  p
4.  b  :  \mBbbZ{}
5.  (2  *  |b|)  \mleq{}  p
6.  ((|a|  *  |a|)  +  (|b|  *  |b|))  \mequiv{}  0  mod  p
7.  \mneg{}((|a|  \mequiv{}  0  mod  p)  \mwedge{}  (|b|  \mequiv{}  0  mod  p))
8.  p  =  2
\mvdash{}  \mexists{}a,b:\mBbbZ{}.  (2  =  ((a  *  a)  +  (b  *  b)))


By

---

Latex:
(InstConcl  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index