Nuprl Lemma : rsqrt_2-irrational


This theorem is one of freek's list of 100 theorems


Definitions occuring in Statement :  irrational: irrational(x) rsqrt: rsqrt(x) int-to-real: r(n) natural_number: $n
Definitions unfolded in proof :  or: P ∨ Q uall: [x:A]. B[x] prop: implies:  Q not: ¬A false: False less_than': less_than'(a;b) and: P ∧ Q le: A ≤ B nat: member: t ∈ T all: x:A. B[x] exists: x:A. B[x] int_seg: {i..j-} decidable: Dec(P) uimplies: supposing a sq_type: SQType(T) guard: {T} true: True lelt: i ≤ j < k satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top
Lemmas referenced :  decidable__equal_int subtype_base_sq int_subtype_base int_seg_properties int_seg_subtype false_wf int_seg_cases satisfiable-full-omega-tt intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf rsqrt-irrational le_wf
Rules used in proof :  unionElimination hypothesisEquality isectElimination hypothesis lambdaFormation independent_pairFormation sqequalRule natural_numberEquality dependent_set_memberEquality thin dependent_functionElimination sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution sqequalHypSubstitution lemma_by_obid cut productElimination introduction extract_by_obid setElimination rename instantiate cumulativity intEquality independent_isectElimination because_Cache independent_functionElimination equalityTransitivity equalitySymmetry voidElimination promote_hyp hypothesis_subsumption addEquality dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidEquality computeAll


Date html generated: 2016_10_26-AM-11_11_43
Last ObjectModification: 2016_09_07-PM-11_56_02

Theory : reals

Home Index