---

Step * 1 of Lemma Ramsey-n-3


1. n : ℕ
2. N : ℕ+
3. g : ℕN ⟶ ℕN ⟶ ℕn
4. f : ℕ3 ⟶ ℕN
5. Inj(ℕ3;ℕN;f)
6. ∀a,b,c,d:ℕ3.  (f a < f b ⇒ f c < f d ⇒ ((g (f a) (f b)) = (g (f c) (f d)) ∈ ℤ))
⊢ ∃i,j,k:ℕN. (i < j ∧ j < k ∧ ((g i j) = (g i k) ∈ ℤ) ∧ ((g i k) = (g j k) ∈ ℤ))
BY
{ (Unfold `inject` -2
   THEN (Assert f 0 < f 1 ∨ f 1 < f 0 BY
               ((Assert ¬((f 0) = (f 1) ∈ ℕN) BY
                       ((D 0 THENA Auto) THEN FHyp 5 [-1] THEN Auto))
                THEN (Assert ¬((f 0) = (f 1) ∈ ℤ) BY
                            (ParallelLast THEN HypSubst' (-1) 0 THEN Auto))
                THEN Lemmaize [-1]
                THEN Auto))
   THEN (Assert f 0 < f 2 ∨ f 2 < f 0 BY
               ((Assert ¬((f 0) = (f 2) ∈ ℕN) BY
                       ((D 0 THENA Auto) THEN FHyp 5 [-1] THEN Auto))
                THEN (Assert ¬((f 0) = (f 2) ∈ ℤ) BY
                            (ParallelLast THEN HypSubst' (-1) 0 THEN Auto))
                THEN Lemmaize [-1]
                THEN Auto))
   THEN (Assert f 1 < f 2 ∨ f 2 < f 1 BY
               ((Assert ¬((f 1) = (f 2) ∈ ℕN) BY
                       ((D 0 THENA Auto) THEN FHyp 5 [-1] THEN Auto))
                THEN (Assert ¬((f 1) = (f 2) ∈ ℤ) BY
                            (ParallelLast THEN HypSubst' (-1) 0 THEN Auto))
                THEN Lemmaize [-1]
                THEN Auto))) }

1
1. n : ℕ
2. N : ℕ+
3. g : ℕN ⟶ ℕN ⟶ ℕn
4. f : ℕ3 ⟶ ℕN
5. ∀a1,a2:ℕ3.  (((f a1) = (f a2) ∈ ℕN) ⇒ (a1 = a2 ∈ ℕ3))
6. ∀a,b,c,d:ℕ3.  (f a < f b ⇒ f c < f d ⇒ ((g (f a) (f b)) = (g (f c) (f d)) ∈ ℤ))
7. f 0 < f 1 ∨ f 1 < f 0
8. f 0 < f 2 ∨ f 2 < f 0
9. f 1 < f 2 ∨ f 2 < f 1
⊢ ∃i,j,k:ℕN. (i < j ∧ j < k ∧ ((g i j) = (g i k) ∈ ℤ) ∧ ((g i k) = (g j k) ∈ ℤ))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  N  :  \mBbbN{}\msupplus{}
3.  g  :  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}n
4.  f  :  \mBbbN{}3  {}\mrightarrow{}  \mBbbN{}N
5.  Inj(\mBbbN{}3;\mBbbN{}N;f)
6.  \mforall{}a,b,c,d:\mBbbN{}3.    (f  a  <  f  b  {}\mRightarrow{}  f  c  <  f  d  {}\mRightarrow{}  ((g  (f  a)  (f  b))  =  (g  (f  c)  (f  d))))
\mvdash{}  \mexists{}i,j,k:\mBbbN{}N.  (i  <  j  \mwedge{}  j  <  k  \mwedge{}  ((g  i  j)  =  (g  i  k))  \mwedge{}  ((g  i  k)  =  (g  j  k)))


By

---

Latex:
(Unfold  `inject`  -2
  THEN  (Assert  f  0  <  f  1  \mvee{}  f  1  <  f  0  BY
                          ((Assert  \mneg{}((f  0)  =  (f  1))  BY
                                          ((D  0  THENA  Auto)  THEN  FHyp  5  [-1]  THEN  Auto))
                            THEN  (Assert  \mneg{}((f  0)  =  (f  1))  BY
                                                    (ParallelLast  THEN  HypSubst'  (-1)  0  THEN  Auto))
                            THEN  Lemmaize  [-1]
                            THEN  Auto))
  THEN  (Assert  f  0  <  f  2  \mvee{}  f  2  <  f  0  BY
                          ((Assert  \mneg{}((f  0)  =  (f  2))  BY
                                          ((D  0  THENA  Auto)  THEN  FHyp  5  [-1]  THEN  Auto))
                            THEN  (Assert  \mneg{}((f  0)  =  (f  2))  BY
                                                    (ParallelLast  THEN  HypSubst'  (-1)  0  THEN  Auto))
                            THEN  Lemmaize  [-1]
                            THEN  Auto))
  THEN  (Assert  f  1  <  f  2  \mvee{}  f  2  <  f  1  BY
                          ((Assert  \mneg{}((f  1)  =  (f  2))  BY
                                          ((D  0  THENA  Auto)  THEN  FHyp  5  [-1]  THEN  Auto))
                            THEN  (Assert  \mneg{}((f  1)  =  (f  2))  BY
                                                    (ParallelLast  THEN  HypSubst'  (-1)  0  THEN  Auto))
                            THEN  Lemmaize  [-1]
                            THEN  Auto)))

---

Home Index