---

Step * 2 2 1 1 of Lemma four-squares


1. p : Prime
2. ¬(p = 2 ∈ ℤ)
3. ↑isOdd(p)
4. k : ℤ
5. p = ((2 * k) + 1) ∈ ℤ
⊢ ∃n:ℕ+p. ∃a,b:ℤ. (((a * a) + (b * b) + 1) = (n * p) ∈ ℤ)
BY
{ (InstLemma `pigeon-hole-implies2` [⌜k + 1⌝;⌜p⌝;⌜λx.((x * x) mod p)⌝;⌜λx.((-((x * x) + 1)) mod p)⌝]⋅ THENA Auto) }

1
.....antecedent..... 
1. p : Prime
2. ¬(p = 2 ∈ ℤ)
3. ↑isOdd(p)
4. k : ℤ
5. p = ((2 * k) + 1) ∈ ℤ
⊢ Inj(ℕk + 1;ℕp;λx.((x * x) mod p))

2
.....antecedent..... 
1. p : Prime
2. ¬(p = 2 ∈ ℤ)
3. ↑isOdd(p)
4. k : ℤ
5. p = ((2 * k) + 1) ∈ ℤ
⊢ Inj(ℕk + 1;ℕp;λx.((-((x * x) + 1)) mod p))

3
1. p : Prime
2. ¬(p = 2 ∈ ℤ)
3. ↑isOdd(p)
4. k : ℤ
5. p = ((2 * k) + 1) ∈ ℤ
6. ∃i:ℕk + 1. (∃j:ℕk + 1 [(((λx.((x * x) mod p)) i) = ((λx.((-((x * x) + 1)) mod p)) j) ∈ ℤ)])
⊢ ∃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)
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}p.  \mexists{}a,b:\mBbbZ{}.  (((a  *  a)  +  (b  *  b)  +  1)  =  (n  *  p))


By

---

Latex:
(InstLemma  `pigeon-hole-implies2`  [\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}\mlambda{}x.((x  *  x)  mod  p)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.((-((x  *  x)  +  1))  mod  p)\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index