---

Step * 1 2 1 1 2 1 2 1 2 of Lemma path-end-mem-basic


1. k : ℤ
2. 0 < k
3. ∀Z:i:ℕk - 1 ⟶ {z:ℝ| z ∈ [r0, r1)} . ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕk - 1. ((Z i) ≤ z)
4. Z : i:ℕk ⟶ {z:ℝ| z ∈ [r0, r1)} 
5. z : {z:ℝ| (r0 ≤ z) ∧ (z < r1)} 
6. ∀i:ℕk - 1. ((Z i) ≤ z)
7. i : ℕk
⊢ (Z i) ≤ rmax(z;Z (k - 1))
BY
{ (Decide ⌜i = (k - 1) ∈ ℤ⌝⋅ THEN Auto) }

1
1. k : ℤ
2. 0 < k
3. ∀Z:i:ℕk - 1 ⟶ {z:ℝ| z ∈ [r0, r1)} . ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕk - 1. ((Z i) ≤ z)
4. Z : i:ℕk ⟶ {z:ℝ| z ∈ [r0, r1)} 
5. z : {z:ℝ| (r0 ≤ z) ∧ (z < r1)} 
6. ∀i:ℕk - 1. ((Z i) ≤ z)
7. i : ℕk
8. i = (k - 1) ∈ ℤ
⊢ (Z i) ≤ rmax(z;Z (k - 1))

2
1. k : ℤ
2. 0 < k
3. ∀Z:i:ℕk - 1 ⟶ {z:ℝ| z ∈ [r0, r1)} . ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕk - 1. ((Z i) ≤ z)
4. Z : i:ℕk ⟶ {z:ℝ| z ∈ [r0, r1)} 
5. z : {z:ℝ| (r0 ≤ z) ∧ (z < r1)} 
6. ∀i:ℕk - 1. ((Z i) ≤ z)
7. i : ℕk
8. ¬(i = (k - 1) ∈ ℤ)
⊢ (Z i) ≤ rmax(z;Z (k - 1))

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  0  <  k
3.  \mforall{}Z:i:\mBbbN{}k  -  1  {}\mrightarrow{}  \{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\}  .  \mexists{}z:\{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\}  .  \mforall{}i:\mBbbN{}k  -  1.  ((Z  i)  \mleq{}  z)
4.  Z  :  i:\mBbbN{}k  {}\mrightarrow{}  \{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\} 
5.  z  :  \{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\} 
6.  \mforall{}i:\mBbbN{}k  -  1.  ((Z  i)  \mleq{}  z)
7.  i  :  \mBbbN{}k
\mvdash{}  (Z  i)  \mleq{}  rmax(z;Z  (k  -  1))


By

---

Latex:
(Decide  \mkleeneopen{}i  =  (k  -  1)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index