---

Step * of Lemma absval_ubound

No Annotations
∀[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:
No  Annotations
\mforall{}[i:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    uiff(|i|  \mleq{}  n;((-n)  \mleq{}  i)  \mwedge{}  (i  \mleq{}  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