---

Step * 2 2 2 1 1 1 of Lemma increasing_split


1. m : ℤ
2. 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)
6. n : ℕ
7. k : ℕ
8. f : ℕn ⟶ ℕm - 1
9. g : ℕk ⟶ ℕm - 1
10. increasing(f;n)
11. increasing(g;k)
12. ∀i:ℕn. (P (f i))
13. ∀j:ℕk. (¬(P (g j)))
14. ∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))
15. ¬(P (m - 1))
16. i : ℕ(k + 1) - 1
⊢ if (i =z k) then m - 1 else g i fi  < if (i + 1 =z k) then m - 1 else g (i + 1) fi 
BY
{ (Repeat SplitOnConclITE THEN Auto') }

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  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)
6.  n  :  \mBbbN{}
7.  k  :  \mBbbN{}
8.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m  -  1
9.  g  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m  -  1
10.  increasing(f;n)
11.  increasing(g;k)
12.  \mforall{}i:\mBbbN{}n.  (P  (f  i))
13.  \mforall{}j:\mBbbN{}k.  (\mneg{}(P  (g  j)))
14.  \mforall{}i:\mBbbN{}m  -  1.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j))))
15.  \mneg{}(P  (m  -  1))
16.  i  :  \mBbbN{}(k  +  1)  -  1
\mvdash{}  if  (i  =\msubz{}  k)  then  m  -  1  else  g  i  fi    <  if  (i  +  1  =\msubz{}  k)  then  m  -  1  else  g  (i  +  1)  fi 


By

---

Latex:
(Repeat  SplitOnConclITE  THEN  Auto')

---

Home Index