---

Step * 1 1 of Lemma rat-int-part_wf


1. a1 : ℤ
⊢ <a1, 0> ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x@0,r = p in a1 = (x@0 + r) ∈ ℚ} 
BY
{ (MemTypeCD THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a1  :  \mBbbZ{}
\mvdash{}  <a1,  0>  \mmember{}  \{p:\mBbbZ{}  \mtimes{}  \{r:\mBbbQ{}|  (0  \mleq{}  r)  \mwedge{}  r  <  1\}  |  let  x@0,r  =  p  in  a1  =  (x@0  +  r)\} 


By

---

Latex:
(MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index