---

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


1. p : Prime
2. a : ℤ
3. (2 * |a|) ≤ p
4. b : ℤ
5. ¬((a ≡ 0 mod p) ∧ (b ≡ 0 mod p))
6. (2 * |b|) ≤ p
7. ((a * a) + (b * b)) ≡ 0 mod p
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)
BY
{ (Assert ¬((|a| ≡ 0 mod p) ∧ (|b| ≡ 0 mod p)) BY
         (ParallelOp -3
          THEN ParallelLast
          THEN MoveToConcl (-1)
          THEN (RWO "absval_unfold" 0 THENA Auto)
          THEN (AutoSplit THEN Auto)
          THEN D -1
          THEN D 0 With ⌜-c⌝ 
          THEN Auto)) }

1
1. p : Prime
2. a : ℤ
3. (2 * |a|) ≤ p
4. b : ℤ
5. ¬((a ≡ 0 mod p) ∧ (b ≡ 0 mod p))
6. (2 * |b|) ≤ p
7. ((a * a) + (b * b)) ≡ 0 mod p
8. ¬((|a| ≡ 0 mod p) ∧ (|b| ≡ 0 mod p))
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mneg{}((|a|  \mequiv{}  0  mod  p)  \mwedge{}  (|b|  \mequiv{}  0  mod  p))  BY
              (ParallelOp  -3
                THEN  ParallelLast
                THEN  MoveToConcl  (-1)
                THEN  (RWO  "absval\_unfold"  0  THENA  Auto)
                THEN  (AutoSplit  THEN  Auto)
                THEN  D  -1
                THEN  D  0  With  \mkleeneopen{}-c\mkleeneclose{} 
                THEN  Auto))

---

Home Index