### Nuprl Lemma : rsqrt_2-irrational

`irrational(rsqrt(r(2)))`

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

Proof

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: `P `` 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: `b 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

Latex:
irrational(rsqrt(r(2)))

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

Theory : reals

Home Index