Nuprl Lemma : qadd_inv_assoc_q

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


Proof




Definitions occuring in Statement :  qmul: s qadd: s rationals: uall: [x:A]. B[x] and: P ∧ Q minus: -n natural_number: $n equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B abgrp: AbGrp iabgrp: IAbGrp{i} grp: Group{i} igrp: IGroup mon: Mon imon: IMonoid qadd_grp: <ℚ+> grp_car: |g| pi1: fst(t) grp_op: * pi2: snd(t) grp_inv: ~ infix_ap: y
Lemmas referenced :  iabgrp_op_inv_assoc qadd_grp_wf subtype_rel_self iabgrp_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis applyEquality sqequalRule instantiate

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



Date html generated: 2020_05_20-AM-09_14_06
Last ObjectModification: 2020_02_04-PM-02_00_13

Theory : rationals


Home Index