---

Step * 1 1 1 1 1 2 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 ∈ ℤ)
9. k : ℤ
10. p = ((2 * k) + 1) ∈ ℤ
11. |a| ≤ k
12. |b| ≤ k
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)
BY
{ (Assert ¬(|a| = 0 ∈ ℤ) BY
         (ParallelOp 7
          THEN (Eliminate ⌜|a|⌝⋅ THEN EAuto 1)
          THEN (Subst' (0 * 0) + (|b| * |b|) ~ |b| * |b| 6 THENA Auto)
          THEN DVar `p'
          THEN (FLemma `product-eq-0-mod-prime` [7] THENM D -1)
          THEN Auto
          THEN Unhide
          THEN Auto)) }

1
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 ∈ ℤ)
9. k : ℤ
10. p = ((2 * k) + 1) ∈ ℤ
11. |a| ≤ k
12. |b| ≤ k
13. ¬(|a| = 0 ∈ ℤ)
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)

---

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.  \mneg{}(p  =  2)
9.  k  :  \mBbbZ{}
10.  p  =  ((2  *  k)  +  1)
11.  |a|  \mleq{}  k
12.  |b|  \mleq{}  k
\mvdash{}  \mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))


By

---

Latex:
(Assert  \mneg{}(|a|  =  0)  BY
              (ParallelOp  7
                THEN  (Eliminate  \mkleeneopen{}|a|\mkleeneclose{}\mcdot{}  THEN  EAuto  1)
                THEN  (Subst'  (0  *  0)  +  (|b|  *  |b|)  \msim{}  |b|  *  |b|  6  THENA  Auto)
                THEN  DVar  `p'
                THEN  (FLemma  `product-eq-0-mod-prime`  [7]  THENM  D  -1)
                THEN  Auto
                THEN  Unhide
                THEN  Auto))

---

Home Index