Nuprl Lemma : qadd_inv_assoc_q
∀[a,b:ℚ].  (((a + -(a) + b) = b ∈ ℚ) ∧ ((-(a) + a + b) = b ∈ ℚ))
Proof
Definitions occuring in Statement : 
qmul: r * s
, 
qadd: r + s
, 
rationals: ℚ
, 
uall: ∀[x:A]. B[x]
, 
and: P ∧ Q
, 
minus: -n
, 
natural_number: $n
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
subtype_rel: A ⊆r 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: x f 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