Nuprl Lemma : mon_ident_q

[a:ℚ]. (((a 0) a ∈ ℚ) ∧ ((0 a) a ∈ ℚ))


Proof




Definitions occuring in Statement :  qadd: s rationals: uall: [x:A]. B[x] and: P ∧ Q natural_number: $n equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆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: 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