### Nuprl Lemma : qpositive_wf

`∀[r:ℚ]. (qpositive(r) ∈ 𝔹)`

Proof

Definitions occuring in Statement :  qpositive: `qpositive(r)` rationals: `ℚ` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  btrue: `tt` bfalse: `ff` or: `P ∨ Q` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` int_nzero: `ℤ-o` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` true: `True` squash: `↓T` uiff: `uiff(P;Q)` has-valueall: `has-valueall(a)` has-value: `(a)↓` callbyvalueall: callbyvalueall uimplies: `b supposing a` prop: `ℙ` qeq: `qeq(r;s)` qpositive: `qpositive(r)` pi2: `snd(t)` ifthenelse: `if b then t else f fi ` unit: `Unit` bool: `𝔹` tunion: `⋃x:A.B[x]` b-union: `A ⋃ B` implies: `P `` Q` all: `∀x:A. B[x]` and: `P ∧ Q` quotient: `x,y:A//B[x; y]` rationals: `ℚ` member: `t ∈ T` uall: `∀[x:A]. B[x]` top: `Top` not: `¬A` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` decidable: `Dec(P)` nequal: `a ≠ b ∈ T ` gt: `i > j` guard: `{T}` sq_type: `SQType(T)` cand: `A c∧ B`
Lemmas referenced :  assert_of_lt_int assert_of_band assert_of_bor iff_weakening_uiff iff_transitivity iff_wf assert_wf less_than_wf or_wf eq_int_wf band_wf bor_wf iff_imp_equal_bool nequal_wf set-valueall-type product-valueall-type int_subtype_base true_wf squash_wf lt_int_wf assert_of_eq_int eqtt_to_assert evalall-reduce int-valueall-type valueall-type-has-valueall rationals_wf equal-wf-base equal_wf qeq_wf equal-wf-T-base int_nzero_wf b-union_wf bool_wf int_formula_prop_wf int_formula_prop_or_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformor_wf itermVar_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__lt int_nzero_properties neg_mul_arg_bounds gt_wf pos_mul_arg_bounds subtype_base_sq full-omega-unsat intformeq_wf int_formula_prop_eq_lemma decidable__equal_int int_entire int_term_value_mul_lemma itermMultiply_wf int_formual_prop_imp_lemma intformimplies_wf
Rules used in proof :  orFunctionality impliesFunctionality addLevel isintReduceTrue independent_pairFormation rename setElimination multiplyEquality independent_pairEquality closedConclusion baseApply imageMemberEquality natural_numberEquality lambdaEquality applyEquality callbyvalueReduce independent_isectElimination axiomEquality dependent_functionElimination baseClosed hypothesisEquality independent_functionElimination equalityElimination unionElimination imageElimination because_Cache lambdaFormation productEquality intEquality isectElimination equalitySymmetry equalityTransitivity thin productElimination pertypeElimination sqequalRule hypothesis extract_by_obid pointwiseFunctionalityForEquality sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution computeAll voidEquality voidElimination isect_memberEquality int_eqEquality dependent_pairFormation levelHypothesis andLevelFunctionality cumulativity instantiate promote_hyp inlFormation approximateComputation inrFormation

Latex:
\mforall{}[r:\mBbbQ{}].  (qpositive(r)  \mmember{}  \mBbbB{})

Date html generated: 2018_05_21-PM-11_46_06
Last ObjectModification: 2017_07_26-PM-06_43_05

Theory : rationals

Home Index