---

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


1. p : Prime
2. a : ℤ
3. b : ℤ
4. ¬((a ≡ 0 mod p) ∧ (b ≡ 0 mod p))
5. ((a * a) + (b * b)) ≡ 0 mod p
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)
BY
{ (((InstLemma `small-eqmod` [⌜p⌝;⌜a⌝]⋅ THENA Auto) THEN D -1 THEN RenameVar `aa' (-2))
   THEN (InstLemma `small-eqmod` [⌜p⌝;⌜b⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `bb' (-2)
   THEN ExRepD
   THEN (RWO "-1< -4<" 5 THENA Auto)
   THEN (RWO "-2< -5<" 4 THENA Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(((InstLemma  `small-eqmod`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  RenameVar  `aa'  (-2))
  THEN  (InstLemma  `small-eqmod`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `bb'  (-2)
  THEN  ExRepD
  THEN  (RWO  "-1<  -4<"  5  THENA  Auto)
  THEN  (RWO  "-2<  -5<"  4  THENA  Auto))

---

Home Index