---

Step * 2 1 1 1 1 1 1 of Lemma prime-sum-of-two-squares-iff-one-mod-four


1. p : {2...}
2. prime(p)
3. x : ℤ
4. y : ℤ
5. z : ℕ
6. w : ℕ
7. x = 0 ∈ ℤ
8. y = 0 ∈ ℤ
9. p = ((4 * w * w) + (4 * z * z)) ∈ ℤ
⊢ False
BY
{ ((InstLemma `not-prime-mult` [⌜2⌝;⌜2⌝;⌜(w * w) + (z * z)⌝]⋅ THENA Auto) THEN D -1) }

1
1. p : {2...}
2. prime(p)
3. x : ℤ
4. y : ℤ
5. z : ℕ
6. w : ℕ
7. x = 0 ∈ ℤ
8. y = 0 ∈ ℤ
9. p = ((4 * w * w) + (4 * z * z)) ∈ ℤ
⊢ prime((2 * 2) * ((w * w) + (z * z)))

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  prime(p)
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  z  :  \mBbbN{}
6.  w  :  \mBbbN{}
7.  x  =  0
8.  y  =  0
9.  p  =  ((4  *  w  *  w)  +  (4  *  z  *  z))
\mvdash{}  False


By

---

Latex:
((InstLemma  `not-prime-mult`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}(w  *  w)  +  (z  *  z)\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index