Nuprl Lemma : qadd_ac_1_q

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


Proof




Definitions occuring in Statement :  qadd: s rationals: uall: [x:A]. B[x] 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 iabmonoid: IAbMonoid imon: IMonoid prop: so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a all: x:A. B[x] implies:  Q qadd_grp: <ℚ+> grp_car: |g| pi1: fst(t) grp_op: * pi2: snd(t) infix_ap: y
Lemmas referenced :  abmonoid_ac_1 qadd_grp_wf subtype_rel_sets 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 instantiate setEquality cumulativity hypothesisEquality setElimination rename because_Cache lambdaEquality_alt setIsType universeIsType independent_isectElimination lambdaFormation_alt

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



Date html generated: 2020_05_20-AM-09_14_12
Last ObjectModification: 2020_02_04-PM-01_46_29

Theory : rationals


Home Index