---

Step * 1 of Lemma twosquareinv-fixpoint


1. p : {p:{2...}| prime(p)} 
2. x : ℕ
3. y : ℕ
4. z : ℕ
5. ¬x < y - z
6. ((x * x) + (4 * y * z)) = p ∈ ℤ
7. ¬(x = 0 ∈ ℤ)
8. ¬(z = 0 ∈ ℤ)
9. x < y + y
10. ((y + y) - x) = x ∈ ℕ
11. y = y ∈ ℕ
12. ((x - y) + z) = z ∈ ℕ
⊢ <x, y, z> = <1, 1, (p - 1) ÷ 4> ∈ (x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} )
BY
{ ((Assert x = y ∈ ℤ BY Auto) THEN (Assert p = (y * (y + (4 * z))) ∈ ℤ BY Auto)) }

1
1. p : {p:{2...}| prime(p)} 
2. x : ℕ
3. y : ℕ
4. z : ℕ
5. ¬x < y - z
6. ((x * x) + (4 * y * z)) = p ∈ ℤ
7. ¬(x = 0 ∈ ℤ)
8. ¬(z = 0 ∈ ℤ)
9. x < y + y
10. ((y + y) - x) = x ∈ ℕ
11. y = y ∈ ℕ
12. ((x - y) + z) = z ∈ ℕ
13. x = y ∈ ℤ
14. p = (y * (y + (4 * z))) ∈ ℤ
⊢ <x, y, z> = <1, 1, (p - 1) ÷ 4> ∈ (x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} )

---

Latex:

---

Latex:

1.  p  :  \{p:\{2...\}|  prime(p)\} 
2.  x  :  \mBbbN{}
3.  y  :  \mBbbN{}
4.  z  :  \mBbbN{}
5.  \mneg{}x  <  y  -  z
6.  ((x  *  x)  +  (4  *  y  *  z))  =  p
7.  \mneg{}(x  =  0)
8.  \mneg{}(z  =  0)
9.  x  <  y  +  y
10.  ((y  +  y)  -  x)  =  x
11.  y  =  y
12.  ((x  -  y)  +  z)  =  z
\mvdash{}  <x,  y,  z>  =  ə,  1,  (p  -  1)  \mdiv{}  4>


By

---

Latex:
((Assert  x  =  y  BY  Auto)  THEN  (Assert  p  =  (y  *  (y  +  (4  *  z)))  BY  Auto))

---

Home Index