### Nuprl Lemma : qinv_wf

[r:ℚ]. 1/r ∈ ℚ supposing ¬↑qeq(r;0)

Proof

Definitions occuring in Statement :  qinv: 1/r rationals: qeq: qeq(r;s) assert: b uimplies: supposing a uall: [x:A]. B[x] not: ¬A member: t ∈ T natural_number: \$n
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T rationals: all: x:A. B[x] quotient: x,y:A//B[x; y] and: P ∧ Q subtype_rel: A ⊆B squash: T prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] sq_type: SQType(T) implies:  Q guard: {T} true: True b-union: A ⋃ B tunion: x:A.B[x] bool: 𝔹 unit: Unit ifthenelse: if then else fi  pi2: snd(t) not: ¬A false: False qeq: qeq(r;s) callbyvalueall: callbyvalueall evalall: evalall(t) btrue: tt qinv: 1/r has-value: (a)↓ has-valueall: has-valueall(a) uiff: uiff(P;Q) so_lambda: λ2x.t[x] so_apply: x[s] bfalse: ff rev_uimplies: rev_uimplies(P;Q) int_nzero: -o nequal: a ≠ b ∈  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top
Lemmas referenced :  rationals_wf b-union_wf int_nzero_wf bool_wf qeq_wf qeq_refl qeq-functionality subtype_rel_b-union-left member_wf squash_wf true_wf istype-universe quotient-member-eq qeq-equiv qinv-wf subtype_base_sq bool_subtype_base equal-wf-T-base assert_wf istype-void valueall-type-has-valueall int-valueall-type evalall-reduce eqtt_to_assert assert_of_eq_int int_subtype_base product-valueall-type eq_int_wf set-valueall-type nequal_wf int_nzero_properties decidable__equal_int full-omega-unsat intformnot_wf intformeq_wf itermMultiply_wf itermVar_wf itermConstant_wf istype-int int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_mul_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf intformand_wf int_formula_prop_and_lemma equal_wf not_wf int-subtype-rationals qeq-wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule sqequalHypSubstitution axiomEquality equalityTransitivity hypothesis equalitySymmetry universeIsType extract_by_obid isectElimination thin intEquality productEquality promote_hyp lambdaFormation_alt equalityIsType3 hypothesisEquality baseClosed inhabitedIsType pointwiseFunctionality pertypeElimination productElimination natural_numberEquality applyEquality independent_isectElimination productIsType equalityIsType4 dependent_functionElimination lambdaEquality_alt imageElimination universeEquality because_Cache instantiate cumulativity independent_functionElimination imageMemberEquality unionElimination equalityElimination functionIsType equalityIsType1 callbyvalueReduce sqleReflexivity isintReduceTrue independent_pairEquality multiplyEquality setElimination rename approximateComputation dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation lambdaFormation

Latex:
\mforall{}[r:\mBbbQ{}].  1/r  \mmember{}  \mBbbQ{}  supposing  \mneg{}\muparrow{}qeq(r;0)

Date html generated: 2019_10_16-AM-11_47_12
Last ObjectModification: 2018_10_11-PM-01_25_28

Theory : rationals

Home Index