---

Step * 1 1 of Lemma rneq-if-rabs2


1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. 4 < |x - y| n
⊢ eval m = 4 * n in
  if ((x m) + 4) < (y m)  then inl m  else (inr m ) ∈ x ≠ y
BY
{ ((CallByValueReduce 0 THENA Auto)
   THEN (RWO "rabs-as-rmax" (-1) THENA Auto)
   THEN RepUR ``rmax rsub`` -1
   THEN RW (AddrC [2;2;1] UnfoldTopAbC) (-1)
   THEN Reduce -1
   THEN (RWO "radd-approx" (-1) THENA Auto)
   THEN RepUR ``rminus`` -1
   THEN (FLemma `imax_strict_ub` [-1] THENA Auto)
   THEN MoveToConcl (-1)
   THEN ((GenConcl ⌜(4 * n) = m ∈ ℕ+⌝⋅ THENM D 0) THENA Auto)
   THEN (Decide ⌜(x m) + 4 < y m⌝⋅ THENA Auto)
   THEN (Reduce 0 THENA Auto)
   THEN Unfold `rneq` 0
   THEN (MemCD THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN Assert ⌜4 < (x m) + (-(y m))⌝ ⋅
   THEN Auto) }

1
.....assertion..... 
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. 4 < imax(((x (4 * n)) + (-(y (4 * n)))) ÷ 4;-(((x (4 * n)) + (-(y (4 * n)))) ÷ 4))
5. m : ℕ+
6. (4 * n) = m ∈ ℕ+
7. 4 < ((x m) + (-(y m))) ÷ 4 ∨ 4 < -(((x m) + (-(y m))) ÷ 4)
8. ¬(x m) + 4 < y m
⊢ 4 < (x m) + (-(y m))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
4.  4  <  |x  -  y|  n
\mvdash{}  eval  m  =  4  *  n  in
    if  ((x  m)  +  4)  <  (y  m)    then  inl  m    else  (inr  m  )  \mmember{}  x  \mneq{}  y


By

---

Latex:
((CallByValueReduce  0  THENA  Auto)
  THEN  (RWO  "rabs-as-rmax"  (-1)  THENA  Auto)
  THEN  RepUR  ``rmax  rsub``  -1
  THEN  RW  (AddrC  [2;2;1]  UnfoldTopAbC)  (-1)
  THEN  Reduce  -1
  THEN  (RWO  "radd-approx"  (-1)  THENA  Auto)
  THEN  RepUR  ``rminus``  -1
  THEN  (FLemma  `imax\_strict\_ub`  [-1]  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  ((GenConcl  \mkleeneopen{}(4  *  n)  =  m\mkleeneclose{}\mcdot{}  THENM  D  0)  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}(x  m)  +  4  <  y  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Reduce  0  THENA  Auto)
  THEN  Unfold  `rneq`  0
  THEN  (MemCD  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  Assert  \mkleeneopen{}4  <  (x  m)  +  (-(y  m))\mkleeneclose{}  \mcdot{}
  THEN  Auto)

---

Home Index