---

Step * of Lemma absval_strict_ubound

∀[i:ℤ]. ∀[n:ℕ].  uiff(|i| < n;-n < i ∧ i < n)
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "absval_unfold" 0 THENA Auto)
   THEN D -1
   THEN Add ⌜-n⌝ (-1)⋅
   THEN (RW IntNormC (-1) THENA Auto)) }

1
1. i : ℤ
2. n : ℤ
3. 0 ≤ n
4. ((-1) * n) ≤ 0
⊢ uiff(if (-1) < (i)  then i  else (-i) < n;-n < i ∧ i < n)

---

Latex:

---

Latex:
\mforall{}[i:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    uiff(|i|  <  n;-n  <  i  \mwedge{}  i  <  n)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)
  THEN  D  -1
  THEN  Add  \mkleeneopen{}-n\mkleeneclose{}  (-1)\mcdot{}
  THEN  (RW  IntNormC  (-1)  THENA  Auto))

---

Home Index