Nuprl Lemma : qmul-qdiv-cancel4

[a,b,c:ℚ].  ((b/a) c) (b c) ∈ ℚ supposing ¬(a 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 squash: T prop: true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q
Lemmas referenced :  equal_wf squash_wf true_wf qmul_assoc_qrng qdiv_wf qmul_wf iff_weakening_equal rationals_wf qmul-qdiv-cancel2 not_wf equal-wf-T-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality because_Cache independent_isectElimination natural_numberEquality sqequalRule imageMemberEquality baseClosed productElimination independent_functionElimination isect_memberEquality axiomEquality

Latex:
\mforall{}[a,b,c:\mBbbQ{}].    ((b/a)  *  a  *  c)  =  (b  *  c)  supposing  \mneg{}(a  =  0)



Date html generated: 2018_05_21-PM-11_51_00
Last ObjectModification: 2017_07_26-PM-06_44_16

Theory : rationals


Home Index