Nuprl Lemma : qinv-zero

[c:ℚ]. ¬(1/c 0 ∈ ℚsupposing ¬(c 0 ∈ ℚ)


Proof




Definitions occuring in Statement :  qinv: 1/r rationals: uimplies: supposing a uall: [x:A]. B[x] not: ¬A natural_number: $n equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a not: ¬A implies:  Q false: False all: x:A. B[x] subtype_rel: A ⊆B or: P ∨ Q qdiv: (r/s) prop: qless: r < s grp_lt: a < b set_lt: a <b assert: b ifthenelse: if then else fi  set_blt: a <b b band: p ∧b q infix_ap: y set_le: b pi2: snd(t) oset_of_ocmon: g↓oset dset_of_mon: g↓set grp_le: b pi1: fst(t) qadd_grp: <ℚ+> q_le: q_le(r;s) callbyvalueall: callbyvalueall evalall: evalall(t) qmul: s btrue: tt bor: p ∨bq qpositive: qpositive(r) qsub: s qadd: s lt_int: i <j bfalse: ff qeq: qeq(r;s) eq_int: (i =z j) bnot: ¬bb uiff: uiff(P;Q) and: P ∧ Q
Lemmas referenced :  qless_trichot_qorder qinv-negative qless_wf qmul_wf qinv-positive equal-wf-T-base rationals_wf qinv_wf assert-qeq int-subtype-rationals assert_wf qeq_wf2 not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin extract_by_obid sqequalHypSubstitution dependent_functionElimination hypothesisEquality natural_numberEquality hypothesis applyEquality because_Cache sqequalRule unionElimination isectElimination independent_isectElimination equalitySymmetry hyp_replacement Error :applyLambdaEquality,  voidElimination independent_functionElimination addLevel impliesFunctionality productElimination baseClosed lambdaEquality isect_memberEquality equalityTransitivity

Latex:
\mforall{}[c:\mBbbQ{}].  \mneg{}(1/c  =  0)  supposing  \mneg{}(c  =  0)



Date html generated: 2016_10_26-AM-06_32_48
Last ObjectModification: 2016_07_12-AM-07_56_12

Theory : rationals


Home Index