Nuprl Lemma : mon_ident_q
∀[a:ℚ]. (((a + 0) = a ∈ ℚ) ∧ ((0 + a) = a ∈ ℚ))
Proof
Definitions occuring in Statement : 
qadd: r + s
, 
rationals: ℚ
, 
uall: ∀[x:A]. B[x]
, 
and: P ∧ Q
, 
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
, 
grp: Group{i}
, 
mon: Mon
, 
imon: IMonoid
, 
prop: ℙ
, 
qadd_grp: <ℚ+>
, 
grp_car: |g|
, 
pi1: fst(t)
, 
grp_op: *
, 
pi2: snd(t)
, 
grp_id: e
, 
infix_ap: x f y
Lemmas referenced : 
mon_ident, 
qadd_grp_wf, 
grp_sig_wf, 
monoid_p_wf, 
grp_car_wf, 
grp_op_wf, 
grp_id_wf, 
inverse_wf, 
grp_inv_wf, 
comm_wf
Rules used in proof : 
cut, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isectElimination, 
thin, 
hypothesis, 
applyEquality, 
sqequalRule, 
lambdaEquality_alt, 
setElimination, 
rename, 
hypothesisEquality, 
setIsType, 
universeIsType, 
because_Cache
Latex:
\mforall{}[a:\mBbbQ{}].  (((a  +  0)  =  a)  \mwedge{}  ((0  +  a)  =  a))
Date html generated:
2020_05_20-AM-09_13_45
Last ObjectModification:
2020_01_28-PM-03_40_52
Theory : rationals
Home
Index