Nuprl Lemma : qinv_thru_op_q

[a,b:ℚ].  (-(a b) (-(b) -(a)) ∈ ℚ)


Proof




Definitions occuring in Statement :  qmul: s qadd: s rationals: uall: [x:A]. B[x] minus: -n natural_number: $n equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B guard: {T} uimplies: supposing a qadd_grp: <ℚ+> grp_car: |g| pi1: fst(t) grp_inv: ~ pi2: snd(t) grp_op: * infix_ap: y
Lemmas referenced :  grp_inv_thru_op qadd_grp_wf grp_subtype_igrp abgrp_subtype_grp subtype_rel_transitivity abgrp_wf grp_wf igrp_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis applyEquality instantiate independent_isectElimination sqequalRule

Latex:
\mforall{}[a,b:\mBbbQ{}].    (-(a  +  b)  =  (-(b)  +  -(a)))



Date html generated: 2020_05_20-AM-09_13_51
Last ObjectModification: 2020_02_03-PM-02_55_10

Theory : rationals


Home Index