---

Step * 2 1 of Lemma increasing_split

.....antecedent..... 
1. m : ℤ
2. [%1] : 0 < m
3. ∀[P:ℕm - 1 ⟶ ℙ]
     ((∀i:ℕm - 1. Dec(P i))
     ⇒ (∃n,k:ℕ
          ∃f:ℕn ⟶ ℕm - 1
           ∃g:ℕk ⟶ ℕm - 1
            (increasing(f;n)
            ∧ increasing(g;k)
            ∧ (∀i:ℕn. (P (f i)))
            ∧ (∀j:ℕk. (¬(P (g j))))
            ∧ (∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))
4. [P] : ℕm ⟶ ℙ
5. ∀i:ℕm. Dec(P i)
⊢ ∀i:ℕm - 1. Dec(P i)
BY
{ ParallelLast }

---

Latex:

---

Latex:
.....antecedent..... 
1.  m  :  \mBbbZ{}
2.  [\%1]  :  0  <  m
3.  \mforall{}[P:\mBbbN{}m  -  1  {}\mrightarrow{}  \mBbbP{}]
          ((\mforall{}i:\mBbbN{}m  -  1.  Dec(P  i))
          {}\mRightarrow{}  (\mexists{}n,k:\mBbbN{}
                    \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m  -  1
                      \mexists{}g:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m  -  1
                        (increasing(f;n)
                        \mwedge{}  increasing(g;k)
                        \mwedge{}  (\mforall{}i:\mBbbN{}n.  (P  (f  i)))
                        \mwedge{}  (\mforall{}j:\mBbbN{}k.  (\mneg{}(P  (g  j))))
                        \mwedge{}  (\mforall{}i:\mBbbN{}m  -  1.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j))))))))
4.  [P]  :  \mBbbN{}m  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}i:\mBbbN{}m.  Dec(P  i)
\mvdash{}  \mforall{}i:\mBbbN{}m  -  1.  Dec(P  i)


By

---

Latex:
ParallelLast

---

Home Index