Nuprl Lemma : weak-Markov-principle2-alt

`∀a:ℕ*. ((∀c:ℕ*. ((¬(a = c ∈ ℕ*)) ∨ (¬(0 = c ∈ ℕ*)))) `` (∃n:ℕ. 0 < a n))`

Proof

Definitions occuring in Statement :  nat-star-0: `0` nat-star: `ℕ*` nat: `ℕ` less_than: `a < b` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` apply: `f a` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  nat-star-0: `0` guard: `{T}` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` prop: `ℙ` and: `P ∧ Q` top: `Top` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` ge: `i ≥ j ` nat: `ℕ` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` decidable: `Dec(P)` nat-star: `ℕ*` not: `¬A` or: `P ∨ Q` implies: `P `` Q` member: `t ∈ T` all: `∀x:A. B[x]`
Lemmas referenced :  int_formula_prop_le_lemma intformle_wf decidable__le int_term_value_constant_lemma itermConstant_wf or_wf nat-star_wf nat-star-0_wf equal-wf-base-T exists_wf less_than_wf all_wf not_wf equal_wf int_formula_prop_wf le_wf zero-le-nat int_formula_prop_not_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformnot_wf itermVar_wf intformeq_wf intformand_wf full-omega-unsat nat_properties nat_wf decidable__equal_nat weak-Markov-principle2
Rules used in proof :  inrFormation baseClosed functionEquality because_Cache independent_pairFormation sqequalRule voidEquality voidElimination isect_memberEquality intEquality int_eqEquality lambdaEquality approximateComputation independent_isectElimination natural_numberEquality equalityTransitivity isectElimination dependent_pairFormation applyEquality functionExtensionality dependent_set_memberEquality rename setElimination equalitySymmetry inlFormation unionElimination independent_functionElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution hypothesis lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution extract_by_obid introduction cut

Latex:
\mforall{}a:\mBbbN{}*.  ((\mforall{}c:\mBbbN{}*.  ((\mneg{}(a  =  c))  \mvee{}  (\mneg{}(0  =  c))))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  0  <  a  n))

Date html generated: 2017_09_29-PM-06_06_48
Last ObjectModification: 2017_09_05-PM-02_39_55

Theory : continuity

Home Index