### Nuprl Lemma : qinv-wf

`∀[r:ℤ ⋃ (ℤ × ℤ-o)]. 1/r ∈ ℤ ⋃ (ℤ × ℤ-o) supposing ¬↑qeq(r;0)`

Proof

Definitions occuring in Statement :  qinv: `1/r` qeq: `qeq(r;s)` int_nzero: `ℤ-o` b-union: `A ⋃ B` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` member: `t ∈ T` product: `x:A × B[x]` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` prop: `ℙ` subtype_rel: `A ⊆r B` qinv: `1/r` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` btrue: `tt` bfalse: `ff` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` not: `¬A` implies: `P `` Q` sq_type: `SQType(T)` all: `∀x:A. B[x]` guard: `{T}` false: `False` so_lambda: `λ2x.t[x]` so_apply: `x[s]` qeq: `qeq(r;s)` evalall: `evalall(t)` eq_int: `(i =z j)` assert: `↑b` true: `True` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top`
Lemmas referenced :  int_formula_prop_wf int_term_value_var_lemma int_term_value_mul_lemma int_term_value_constant_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermVar_wf itermMultiply_wf itermConstant_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int int_nzero_properties assert_of_eq_int set-valueall-type product-valueall-type ifthenelse_wf nequal_wf equal_wf int_subtype_base subtype_base_sq evalall-reduce int-valueall-type valueall-type-has-valueall b-union_wf int_nzero_wf subtype_rel_b-union-left qeq_wf assert_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination thin hypothesisEquality natural_numberEquality applyEquality intEquality productEquality isect_memberEquality because_Cache imageElimination productElimination unionElimination equalityElimination independent_isectElimination callbyvalueReduce isintReduceTrue imageMemberEquality dependent_pairEquality independent_pairEquality dependent_set_memberEquality lambdaFormation independent_functionElimination instantiate cumulativity dependent_functionElimination voidElimination universeEquality lambdaEquality sqleReflexivity multiplyEquality setElimination rename dependent_pairFormation int_eqEquality voidEquality computeAll

Latex:
\mforall{}[r:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})].  1/r  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})  supposing  \mneg{}\muparrow{}qeq(r;0)

Date html generated: 2016_05_15-PM-10_38_06
Last ObjectModification: 2016_01_16-PM-09_37_10

Theory : rationals

Home Index