---

Step * of Lemma rat-int-part_wf2

∀q:ℚ. (rat-int-part(q) ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ} )
BY
{ ((D 0 THENA Auto) THEN D 1 THEN Auto) }

1
1. q : Base
2. q1 : Base
3. q = q1 ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) = tt))
4. q ∈ ℤ ⋃ (ℤ × ℤ-o)
5. q1 ∈ ℤ ⋃ (ℤ × ℤ-o)
6. qeq(q;q1) = tt
⊢ rat-int-part(q) = rat-int-part(q1) ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ} 

---

Latex:

---

Latex:
\mforall{}q:\mBbbQ{}.  (rat-int-part(q)  \mmember{}  \{p:\mBbbZ{}  \mtimes{}  \{r:\mBbbQ{}|  (0  \mleq{}  r)  \mwedge{}  r  <  1\}  |  let  x,r  =  p  in  q  =  (x  +  r)\}  )


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  1  THEN  Auto)

---

Home Index