---

Step * 1 of Lemma twosquare-type-finite


1. p : {p:{2...}| prime(p)} 
⊢ finite(x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} )
BY
{ (InstLemma `finite-decidable-subset` [⌜ℕp × ℕp × ℕp⌝;⌜λ2t.let x,y,z = t in 
                                                        ((x * x) + (4 * y * z)) = p ∈ ℤ⌝]⋅
   THENA Auto
   ) }

1
.....antecedent..... 
1. p : {p:{2...}| prime(p)} 
⊢ finite(ℕp × ℕp × ℕp)

2
.....decidable?..... 
1. p : {p:{2...}| prime(p)} 
2. x : ℕp × ℕp × ℕp
⊢ Dec(↓let x,y,z = x in 
       ((x * x) + (4 * y * z)) = p ∈ ℤ)

3
1. p : {p:{2...}| prime(p)} 
2. finite({t:ℕp × ℕp × ℕp| let x,y,z = t in ((x * x) + (4 * y * z)) = p ∈ ℤ} )
⊢ finite(x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} )

---

Latex:

---

Latex:

1.  p  :  \{p:\{2...\}|  prime(p)\} 
\mvdash{}  finite(x:\mBbbN{}  \mtimes{}  y:\mBbbN{}  \mtimes{}  \{z:\mBbbN{}|  ((x  *  x)  +  (4  *  y  *  z))  =  p\}  )


By

---

Latex:
(InstLemma  `finite-decidable-subset`  [\mkleeneopen{}\mBbbN{}p  \mtimes{}  \mBbbN{}p  \mtimes{}  \mBbbN{}p\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}t.let  x,y,z  =  t  in 
                                                                                                            ((x  *  x)  +  (4  *  y  *  z))  =  p\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index