---

Step * of Lemma rless_ibs_property

∀x,y:ℝ.
  ((x < y ⇐⇒ ∃n:ℕ. ((rless_ibs(x;y) n) = 1 ∈ ℤ))
  ∧ (∀n:ℕ
       (((rless_ibs(x;y) n) = 0 ∈ ℤ)
       ⇒ (((y < x) ∧ (∀m:ℕ. ((rless_ibs(x;y) m) = 0 ∈ ℤ))) ∨ (|x - y| ≤ (r(4)/r(n + 1)))))))
BY
{ (InstLemma `rless_ibs_wf` [] THEN RepeatFor 2 (ParallelLast') THEN All (RepUR ``rless_ibs``) THEN D 0) }

1
1. x : ℝ
2. y : ℝ
3. λn.if (∃m∈upto(n + 1).(x (m + 1)) + 4 <z y (m + 1))_b then 1 else 0 fi  ∈ IBS
⊢ x < y ⇐⇒ ∃n:ℕ. (if (∃m∈upto(n + 1).(x (m + 1)) + 4 <z y (m + 1))_b then 1 else 0 fi  = 1 ∈ ℤ)

2
1. x : ℝ
2. y : ℝ
3. λn.if (∃m∈upto(n + 1).(x (m + 1)) + 4 <z y (m + 1))_b then 1 else 0 fi  ∈ IBS
⊢ ∀n:ℕ
    ((if (∃m∈upto(n + 1).(x (m + 1)) + 4 <z y (m + 1))_b then 1 else 0 fi  = 0 ∈ ℤ)
    ⇒ (((y < x) ∧ (∀m:ℕ. (if (∃m∈upto(m + 1).(x (m + 1)) + 4 <z y (m + 1))_b then 1 else 0 fi  = 0 ∈ ℤ)))
       ∨ (|x - y| ≤ (r(4)/r(n + 1)))))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.
    ((x  <  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((rless\_ibs(x;y)  n)  =  1))
    \mwedge{}  (\mforall{}n:\mBbbN{}
              (((rless\_ibs(x;y)  n)  =  0)
              {}\mRightarrow{}  (((y  <  x)  \mwedge{}  (\mforall{}m:\mBbbN{}.  ((rless\_ibs(x;y)  m)  =  0)))  \mvee{}  (|x  -  y|  \mleq{}  (r(4)/r(n  +  1)))))))


By

---

Latex:
(InstLemma  `rless\_ibs\_wf`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  All  (RepUR  ``rless\_ibs``)
  THEN  D  0)

---

Home Index