Nuprl Lemma : qmul-ident-div

[r,s:ℚ].  ((r/r) s) s ∈ ℚ supposing ¬(r 0 ∈ ℚ)


Proof




Definitions occuring in Statement :  qdiv: (r/s) qmul: s 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 prop: true: True squash: T subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q
Lemmas referenced :  not_wf equal-wf-T-base rationals_wf equal_wf squash_wf true_wf qmul_wf qdiv-self iff_weakening_equal qmul_one_qrng
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality baseClosed sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry natural_numberEquality applyEquality lambdaEquality imageElimination universeEquality independent_isectElimination imageMemberEquality productElimination independent_functionElimination

Latex:
\mforall{}[r,s:\mBbbQ{}].    ((r/r)  *  s)  =  s  supposing  \mneg{}(r  =  0)



Date html generated: 2018_05_21-PM-11_50_39
Last ObjectModification: 2017_07_26-PM-06_44_04

Theory : rationals


Home Index