---

Step * 1 of Lemma radd-list_functionality_wrt_rleq


1. u : ℝ
2. v : ℝ List
3. ∀[L2:ℝ List]. radd-list(v) ≤ radd-list(L2) supposing (||v|| = ||L2|| ∈ ℤ) ∧ (∀i:ℕ||v||. (v[i] ≤ L2[i]))
4. u1 : ℝ
5. v1 : ℝ List
6. radd-list([u / v]) ≤ radd-list(v1) supposing (||[u / v]|| = ||v1|| ∈ ℤ) ∧ (∀i:ℕ||[u / v]||. ([u / v][i] ≤ v1[i]))
7. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
8. ∀i:ℕ||v|| + 1. ([u / v][i] ≤ [u1 / v1][i])
⊢ (u + radd-list(v)) ≤ (u1 + radd-list(v1))
BY
{ (InstHyp [⌜v1⌝] 3⋅ THENA (Auto THEN InstHyp [⌜i + 1⌝] (-3)⋅ THEN Auto THEN RWO "select_cons_tl" (-1) THEN Auto)) }

1
1. u : ℝ
2. v : ℝ List
3. ∀[L2:ℝ List]. radd-list(v) ≤ radd-list(L2) supposing (||v|| = ||L2|| ∈ ℤ) ∧ (∀i:ℕ||v||. (v[i] ≤ L2[i]))
4. u1 : ℝ
5. v1 : ℝ List
6. radd-list([u / v]) ≤ radd-list(v1) supposing (||[u / v]|| = ||v1|| ∈ ℤ) ∧ (∀i:ℕ||[u / v]||. ([u / v][i] ≤ v1[i]))
7. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
8. ∀i:ℕ||v|| + 1. ([u / v][i] ≤ [u1 / v1][i])
9. radd-list(v) ≤ radd-list(v1)
⊢ (u + radd-list(v)) ≤ (u1 + radd-list(v1))

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}  List
3.  \mforall{}[L2:\mBbbR{}  List]
          radd-list(v)  \mleq{}  radd-list(L2)  supposing  (||v||  =  ||L2||)  \mwedge{}  (\mforall{}i:\mBbbN{}||v||.  (v[i]  \mleq{}  L2[i]))
4.  u1  :  \mBbbR{}
5.  v1  :  \mBbbR{}  List
6.  radd-list([u  /  v])  \mleq{}  radd-list(v1) 
      supposing  (||[u  /  v]||  =  ||v1||)  \mwedge{}  (\mforall{}i:\mBbbN{}||[u  /  v]||.  ([u  /  v][i]  \mleq{}  v1[i]))
7.  (||v||  +  1)  =  (||v1||  +  1)
8.  \mforall{}i:\mBbbN{}||v||  +  1.  ([u  /  v][i]  \mleq{}  [u1  /  v1][i])
\mvdash{}  (u  +  radd-list(v))  \mleq{}  (u1  +  radd-list(v1))


By

---

Latex:
(InstHyp  [\mkleeneopen{}v1\mkleeneclose{}]  3\mcdot{}
  THENA  (Auto  THEN  InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto  THEN  RWO  "select\_cons\_tl"  (-1)  THEN  Auto)
  )

---

Home Index