Step
*
1
1
1
of Lemma
better-not-not-Ramsey
.....assertion.....
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. ∀[s:StrictInc]. ⇃(∃n,m,p,q:ℕ. ((n < m ∧ R[s n;s m]) ∧ p < q ∧ (¬R[s p;s q])))
3. ∀s:StrictInc. ⇃(∃m:ℕ. ∃n,p:{m + 1...}. (R[s m;s n] ∧ (¬R[s m;s p])))
4. ¬(∀s:StrictInc. ∃n:ℕ. (¬homogeneous(R;n;s)))
⊢ ⇃(∀s:StrictInc. ∃m:ℕ. ∃n,p:{m + 1...}. (R[s m;s n] ∧ (¬R[s m;s p])))
BY
{ (BLemma `all-quotient-true` THEN EAuto 2) }
Latex:
Latex:
.....assertion.....
1. R : \mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbP{}
2. \mforall{}[s:StrictInc]. \00D9(\mexists{}n,m,p,q:\mBbbN{}. ((n < m \mwedge{} R[s n;s m]) \mwedge{} p < q \mwedge{} (\mneg{}R[s p;s q])))
3. \mforall{}s:StrictInc. \00D9(\mexists{}m:\mBbbN{}. \mexists{}n,p:\{m + 1...\}. (R[s m;s n] \mwedge{} (\mneg{}R[s m;s p])))
4. \mneg{}(\mforall{}s:StrictInc. \mexists{}n:\mBbbN{}. (\mneg{}homogeneous(R;n;s)))
\mvdash{} \00D9(\mforall{}s:StrictInc. \mexists{}m:\mBbbN{}. \mexists{}n,p:\{m + 1...\}. (R[s m;s n] \mwedge{} (\mneg{}R[s m;s p])))
By
Latex:
(BLemma `all-quotient-true` THEN EAuto 2)
Home
Index