Step * 1 1 2 of Lemma es-increasing-sequence

.....upcase..... 
1. es EO@i'
2. : ℕ+@i
3. : ℕm ─→ E@i
4. ∀i:ℕ1. (f i <loc (i 1))@i
5. : ℤ
6. 0 < d
7. ∀i:ℕm. ∀j:ℕi.  (((i j) ≤ (d 1))  (f j <loc i))
⊢ ∀i:ℕm. ∀j:ℕi.  (((i j) ≤ d)  (f j <loc i))
BY
((Auto THEN AssertBY ⌈(f j <loc (j 1))⌉ (BackThruHyp THEN Auto)⋅ THEN Decide ⌈(j 1) ∈ ℤ⌉⋅THENA Auto) }

1
1. es EO@i'
2. : ℕ+@i
3. : ℕm ─→ E@i
4. ∀i:ℕ1. (f i <loc (i 1))@i
5. : ℤ
6. 0 < d
7. ∀i:ℕm. ∀j:ℕi.  (((i j) ≤ (d 1))  (f j <loc i))
8. : ℕm@i
9. : ℕi@i
10. (i j) ≤ d@i
11. (f j <loc (j 1))
12. (j 1) ∈ ℤ
⊢ (f j <loc i)

2
1. es EO@i'
2. : ℕ+@i
3. : ℕm ─→ E@i
4. ∀i:ℕ1. (f i <loc (i 1))@i
5. : ℤ
6. 0 < d
7. ∀i:ℕm. ∀j:ℕi.  (((i j) ≤ (d 1))  (f j <loc i))
8. : ℕm@i
9. : ℕi@i
10. (i j) ≤ d@i
11. (f j <loc (j 1))
12. ¬(i (j 1) ∈ ℤ)
⊢ (f j <loc i)


Latex:


.....upcase..... 
1.  es  :  EO@i'
2.  m  :  \mBbbN{}\msupplus{}@i
3.  f  :  \mBbbN{}m  {}\mrightarrow{}  E@i
4.  \mforall{}i:\mBbbN{}m  -  1.  (f  i  <loc  f  (i  +  1))@i
5.  d  :  \mBbbZ{}
6.  0  <  d
7.  \mforall{}i:\mBbbN{}m.  \mforall{}j:\mBbbN{}i.    (((i  -  j)  \mleq{}  (d  -  1))  {}\mRightarrow{}  (f  j  <loc  f  i))
\mvdash{}  \mforall{}i:\mBbbN{}m.  \mforall{}j:\mBbbN{}i.    (((i  -  j)  \mleq{}  d)  {}\mRightarrow{}  (f  j  <loc  f  i))


By

((Auto  THEN  AssertBY  \mkleeneopen{}(f  j  <loc  f  (j  +  1))\mkleeneclose{}  (BackThruHyp  4  THEN  Auto)\mcdot{}  THEN  Decide  \mkleeneopen{}i  =  (j  +  1)\mkleeneclose{}\mcdot{})
  THENA  Auto
  )




Home Index