Step
*
2
1
of Lemma
weak-Markov-principle2
1. a : ℕ*
2. ∀c:ℕ*. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬(0 = (c n) ∈ ℤ)))))
3. ∀c:ℕ ⟶ ℕ
∃i:ℕ
(((i = 0 ∈ ℤ)
⇒ (¬¬(∃n:ℕ. (¬((a n) = (nat-star-retract(c) n) ∈ ℤ)))))
∧ ((¬(i = 0 ∈ ℤ))
⇒ (¬¬(∃n:ℕ. (¬(0 = (nat-star-retract(c) n) ∈ ℤ))))))
4. F : c:(ℕ ⟶ ℕ) ⟶ ℕ
5. ∀c:ℕ ⟶ ℕ
((((F c) = 0 ∈ ℤ)
⇒ (¬¬(∃n:ℕ. (¬((a n) = (nat-star-retract(c) n) ∈ ℤ)))))
∧ ((¬((F c) = 0 ∈ ℤ))
⇒ (¬¬(∃n:ℕ. (¬(0 = (nat-star-retract(c) n) ∈ ℤ))))))
6. ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ))
⇒ ((F f) = (F g) ∈ ℕ)))
⊢ ∃n:ℕ. 0 < a n
BY
{ (Assert (F 0) = 0 ∈ ℤ BY
SupposeNot) }
1
1. a : ℕ*
2. ∀c:ℕ*. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬(0 = (c n) ∈ ℤ)))))
3. ∀c:ℕ ⟶ ℕ
∃i:ℕ
(((i = 0 ∈ ℤ)
⇒ (¬¬(∃n:ℕ. (¬((a n) = (nat-star-retract(c) n) ∈ ℤ)))))
∧ ((¬(i = 0 ∈ ℤ))
⇒ (¬¬(∃n:ℕ. (¬(0 = (nat-star-retract(c) n) ∈ ℤ))))))
4. F : c:(ℕ ⟶ ℕ) ⟶ ℕ
5. ∀c:ℕ ⟶ ℕ
((((F c) = 0 ∈ ℤ)
⇒ (¬¬(∃n:ℕ. (¬((a n) = (nat-star-retract(c) n) ∈ ℤ)))))
∧ ((¬((F c) = 0 ∈ ℤ))
⇒ (¬¬(∃n:ℕ. (¬(0 = (nat-star-retract(c) n) ∈ ℤ))))))
6. ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ))
⇒ ((F f) = (F g) ∈ ℕ)))
7. ¬((F 0) = 0 ∈ ℤ)
⊢ (F 0) = 0 ∈ ℤ
2
1. a : ℕ*
2. ∀c:ℕ*. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬(0 = (c n) ∈ ℤ)))))
3. ∀c:ℕ ⟶ ℕ
∃i:ℕ
(((i = 0 ∈ ℤ)
⇒ (¬¬(∃n:ℕ. (¬((a n) = (nat-star-retract(c) n) ∈ ℤ)))))
∧ ((¬(i = 0 ∈ ℤ))
⇒ (¬¬(∃n:ℕ. (¬(0 = (nat-star-retract(c) n) ∈ ℤ))))))
4. F : c:(ℕ ⟶ ℕ) ⟶ ℕ
5. ∀c:ℕ ⟶ ℕ
((((F c) = 0 ∈ ℤ)
⇒ (¬¬(∃n:ℕ. (¬((a n) = (nat-star-retract(c) n) ∈ ℤ)))))
∧ ((¬((F c) = 0 ∈ ℤ))
⇒ (¬¬(∃n:ℕ. (¬(0 = (nat-star-retract(c) n) ∈ ℤ))))))
6. ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ))
⇒ ((F f) = (F g) ∈ ℕ)))
7. (F 0) = 0 ∈ ℤ
⊢ ∃n:ℕ. 0 < a n
Latex:
Latex:
1. a : \mBbbN{}*
2. \mforall{}c:\mBbbN{}*. ((\mneg{}\mneg{}(\mexists{}n:\mBbbN{}. (\mneg{}((a n) = (c n))))) \mvee{} (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}. (\mneg{}(0 = (c n))))))
3. \mforall{}c:\mBbbN{} {}\mrightarrow{} \mBbbN{}
\mexists{}i:\mBbbN{}
(((i = 0) {}\mRightarrow{} (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}. (\mneg{}((a n) = (nat-star-retract(c) n))))))
\mwedge{} ((\mneg{}(i = 0)) {}\mRightarrow{} (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}. (\mneg{}(0 = (nat-star-retract(c) n)))))))
4. F : c:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}
5. \mforall{}c:\mBbbN{} {}\mrightarrow{} \mBbbN{}
((((F c) = 0) {}\mRightarrow{} (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}. (\mneg{}((a n) = (nat-star-retract(c) n))))))
\mwedge{} ((\mneg{}((F c) = 0)) {}\mRightarrow{} (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}. (\mneg{}(0 = (nat-star-retract(c) n)))))))
6. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}n:\mBbbN{}. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f = g) {}\mRightarrow{} ((F f) = (F g))))
\mvdash{} \mexists{}n:\mBbbN{}. 0 < a n
By
Latex:
(Assert (F 0) = 0 BY
SupposeNot)
Home
Index