Step
*
1
of Lemma
assert-b-exists
1. n : ℤ
2. [%1] : 0 < n
3. ∀P:ℕn - 1 ⟶ 𝔹. (↑(∃i<n - 1.P[i])_b
⇐⇒ ∃i:ℕn - 1. (↑P[i]))
4. P : ℕn ⟶ 𝔹
5. ↑(∃i<n - 1.P[i])_b
⇐⇒ ∃i:ℕn - 1. (↑P[i])
6. 1 ≤ n
⊢ (↑P[n - 1]) ∨ (∃i:ℕn - 1. (↑P[i]))
⇐⇒ ∃i:ℕn. (↑P[i])
BY
{ (Auto THEN SplitOrHyps THEN ExRepD THEN Try (Decide ⌜i = (n - 1) ∈ ℤ⌝⋅) THEN Auto) }
Latex:
Latex:
1. n : \mBbbZ{}
2. [\%1] : 0 < n
3. \mforall{}P:\mBbbN{}n - 1 {}\mrightarrow{} \mBbbB{}. (\muparrow{}(\mexists{}i<n - 1.P[i])\_b \mLeftarrow{}{}\mRightarrow{} \mexists{}i:\mBbbN{}n - 1. (\muparrow{}P[i]))
4. P : \mBbbN{}n {}\mrightarrow{} \mBbbB{}
5. \muparrow{}(\mexists{}i<n - 1.P[i])\_b \mLeftarrow{}{}\mRightarrow{} \mexists{}i:\mBbbN{}n - 1. (\muparrow{}P[i])
6. 1 \mleq{} n
\mvdash{} (\muparrow{}P[n - 1]) \mvee{} (\mexists{}i:\mBbbN{}n - 1. (\muparrow{}P[i])) \mLeftarrow{}{}\mRightarrow{} \mexists{}i:\mBbbN{}n. (\muparrow{}P[i])
By
Latex:
(Auto THEN SplitOrHyps THEN ExRepD THEN Try (Decide \mkleeneopen{}i = (n - 1)\mkleeneclose{}\mcdot{}) THEN Auto)
Home
Index