---

Step * 2 2 1 1 3 1 1 1 of Lemma four-squares


1. p : Prime
2. ¬(p = 2 ∈ ℤ)
3. ↑isOdd(p)
4. k : ℤ
5. p = ((2 * k) + 1) ∈ ℤ
6. i : ℕk + 1
7. j : ℕk + 1
8. ((i * i) mod p) = ((-((j * j) + 1)) mod p) ∈ ℤ
9. ((i * i) mod p) ≡ (i * i) mod p
10. ((-((j * j) + 1)) mod p) ≡ (-((j * j) + 1)) mod p
11. (i * i) ≡ (-((j * j) + 1)) mod p
12. c : ℤ
13. (((i * i) + (j * j) + 1) - 0) = (p * c) ∈ ℤ
⊢ ∃n:ℕ+p. ∃a,b:ℤ. (((a * a) + (b * b) + 1) = (n * p) ∈ ℤ)
BY
{ ((Assert (i * i) ≤ (k * k) BY
          ((Assert i ≤ k BY Auto) THEN Mul ⌜i⌝ (-1)⋅ THEN Mul ⌜k⌝ (-2)⋅ THEN Auto))
   THEN (Assert (j * j) ≤ (k * k) BY
               ((Assert j ≤ k BY Auto) THEN Mul ⌜j⌝ (-1)⋅ THEN Mul ⌜k⌝ (-2)⋅ THEN Auto))
   ) }

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

---

Latex:

---

Latex:

1.  p  :  Prime
2.  \mneg{}(p  =  2)
3.  \muparrow{}isOdd(p)
4.  k  :  \mBbbZ{}
5.  p  =  ((2  *  k)  +  1)
6.  i  :  \mBbbN{}k  +  1
7.  j  :  \mBbbN{}k  +  1
8.  ((i  *  i)  mod  p)  =  ((-((j  *  j)  +  1))  mod  p)
9.  ((i  *  i)  mod  p)  \mequiv{}  (i  *  i)  mod  p
10.  ((-((j  *  j)  +  1))  mod  p)  \mequiv{}  (-((j  *  j)  +  1))  mod  p
11.  (i  *  i)  \mequiv{}  (-((j  *  j)  +  1))  mod  p
12.  c  :  \mBbbZ{}
13.  (((i  *  i)  +  (j  *  j)  +  1)  -  0)  =  (p  *  c)
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}p.  \mexists{}a,b:\mBbbZ{}.  (((a  *  a)  +  (b  *  b)  +  1)  =  (n  *  p))


By

---

Latex:
((Assert  (i  *  i)  \mleq{}  (k  *  k)  BY
                ((Assert  i  \mleq{}  k  BY  Auto)  THEN  Mul  \mkleeneopen{}i\mkleeneclose{}  (-1)\mcdot{}  THEN  Mul  \mkleeneopen{}k\mkleeneclose{}  (-2)\mcdot{}  THEN  Auto))
  THEN  (Assert  (j  *  j)  \mleq{}  (k  *  k)  BY
                          ((Assert  j  \mleq{}  k  BY  Auto)  THEN  Mul  \mkleeneopen{}j\mkleeneclose{}  (-1)\mcdot{}  THEN  Mul  \mkleeneopen{}k\mkleeneclose{}  (-2)\mcdot{}  THEN  Auto))
  )

---

Home Index