---

Step * 1 1 1 1 1 of Lemma twosquareinv-fixpoint

.....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 ∈ ℤ} 
BY
{ (Subst' p - 1 ~ 4 * z 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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{}  z  =  ((p  -  1)  \mdiv{}  4)


By

---

Latex:
(Subst'  p  -  1  \msim{}  4  *  z  0  THEN  Auto)

---

Home Index