---

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


1. p : Prime
2. k : ℤ
3. p = ((2 * k) + 1) ∈ ℤ
4. n : ℕ+k + 1
5. m : ℕ+k + 1
6. ((n * n) + (m * m)) ≡ 0 mod p
7. 1 ≤ n
8. (n * 1) ≤ (n * n)
9. 1 ≤ m
10. (m * 1) ≤ (m * m)
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)
BY
{ (D 6 THEN (Decide ⌜c ≤ 0⌝⋅ THENA Auto) THEN Try ((Mul ⌜p⌝ (-1)⋅ THEN Auto)) THEN (Decide ⌜p ≤ c⌝⋅ THENA Auto)) }

1
1. p : Prime
2. k : ℤ
3. p = ((2 * k) + 1) ∈ ℤ
4. n : ℕ+k + 1
5. m : ℕ+k + 1
6. c : ℤ
7. (((n * n) + (m * m)) - 0) = (p * c) ∈ ℤ
8. 1 ≤ n
9. (n * 1) ≤ (n * n)
10. 1 ≤ m
11. (m * 1) ≤ (m * m)
12. ¬(c ≤ 0)
13. p ≤ c
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)

2
1. p : Prime
2. k : ℤ
3. p = ((2 * k) + 1) ∈ ℤ
4. n : ℕ+k + 1
5. m : ℕ+k + 1
6. c : ℤ
7. (((n * n) + (m * m)) - 0) = (p * c) ∈ ℤ
8. 1 ≤ n
9. (n * 1) ≤ (n * n)
10. 1 ≤ m
11. (m * 1) ≤ (m * m)
12. ¬(c ≤ 0)
13. ¬(p ≤ c)
⊢ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)

---

Latex:

---

Latex:

1.  p  :  Prime
2.  k  :  \mBbbZ{}
3.  p  =  ((2  *  k)  +  1)
4.  n  :  \mBbbN{}\msupplus{}k  +  1
5.  m  :  \mBbbN{}\msupplus{}k  +  1
6.  ((n  *  n)  +  (m  *  m))  \mequiv{}  0  mod  p
7.  1  \mleq{}  n
8.  (n  *  1)  \mleq{}  (n  *  n)
9.  1  \mleq{}  m
10.  (m  *  1)  \mleq{}  (m  *  m)
\mvdash{}  \mexists{}a,b:\mBbbZ{}.  (p  =  ((a  *  a)  +  (b  *  b)))


By

---

Latex:
(D  6
  THEN  (Decide  \mkleeneopen{}c  \mleq{}  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((Mul  \mkleeneopen{}p\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  (Decide  \mkleeneopen{}p  \mleq{}  c\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index