---

Step * of Lemma increasing_split

∀m:ℕ
  ∀[P:ℕm ⟶ ℙ]
    ((∀i:ℕm. Dec(P i))
    ⇒ (∃n,k:ℕ
         ∃f:ℕn ⟶ ℕm
          ∃g:ℕk ⟶ ℕm
           (increasing(f;n)
           ∧ increasing(g;k)
           ∧ (∀i:ℕn. (P (f i)))
           ∧ (∀j:ℕk. (¬(P (g j))))
           ∧ (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))
BY
{ ((D 0 THENA Auto) THEN NatInd 1) }

1
.....basecase..... 
∀[P:ℕ0 ⟶ ℙ]
  ((∀i:ℕ0. Dec(P i))
  ⇒ (∃n,k:ℕ
       ∃f:ℕn ⟶ ℕ0
        ∃g:ℕk ⟶ ℕ0
         (increasing(f;n)
         ∧ increasing(g;k)
         ∧ (∀i:ℕn. (P (f i)))
         ∧ (∀j:ℕk. (¬(P (g j))))
         ∧ (∀i:ℕ0. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))

2
.....upcase..... 
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) ∈ ℤ)))))))
⊢ ∀[P:ℕm ⟶ ℙ]
    ((∀i:ℕm. Dec(P i))
    ⇒ (∃n,k:ℕ
         ∃f:ℕn ⟶ ℕm
          ∃g:ℕk ⟶ ℕm
           (increasing(f;n)
           ∧ increasing(g;k)
           ∧ (∀i:ℕn. (P (f i)))
           ∧ (∀j:ℕk. (¬(P (g j))))
           ∧ (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))

---

Latex:

---

Latex:
\mforall{}m:\mBbbN{}
    \mforall{}[P:\mBbbN{}m  {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}i:\mBbbN{}m.  Dec(P  i))
        {}\mRightarrow{}  (\mexists{}n,k:\mBbbN{}
                  \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m
                    \mexists{}g:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m
                      (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.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j))))))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  NatInd  1)

---

Home Index