---

Step * 1 1 1 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 ∈ ℕ
13. x = y ∈ ℤ
14. p = (1 * (1 + (4 * z))) ∈ ℤ
15. y = 1 ∈ ℤ
⊢ <1, 1, z> = <1, 1, (p - 1) ÷ 4> ∈ (x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} )
BY
{ RepeatFor 2 (EqCDA) }

1
.....subterm..... T:t
2:n
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 = (1 * (1 + (4 * z))) ∈ ℤ
15. y = 1 ∈ ℤ
⊢ z = ((p - 1) ÷ 4) ∈ {z:ℕ| ((1 * 1) + (4 * 1 * 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
13.  x  =  y
14.  p  =  (1  *  (1  +  (4  *  z)))
15.  y  =  1
\mvdash{}  ə,  1,  z>  =  ə,  1,  (p  -  1)  \mdiv{}  4>


By

---

Latex:
RepeatFor  2  (EqCDA)

---

Home Index