MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addasspr Structured version   Visualization version   GIF version

Theorem addasspr 10660
Description: Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by NM, 18-Mar-1996.) (New usage is discouraged.)
Assertion
Ref Expression
addasspr ((𝐴 +P 𝐵) +P 𝐶) = (𝐴 +P (𝐵 +P 𝐶))

Proof of Theorem addasspr
Dummy variables 𝑓 𝑔 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-plp 10621 . 2 +P = (𝑤P, 𝑣P ↦ {𝑥 ∣ ∃𝑦𝑤𝑧𝑣 𝑥 = (𝑦 +Q 𝑧)})
2 addclnq 10583 . 2 ((𝑦Q𝑧Q) → (𝑦 +Q 𝑧) ∈ Q)
3 dmplp 10650 . 2 dom +P = (P × P)
4 addclpr 10656 . 2 ((𝑓P𝑔P) → (𝑓 +P 𝑔) ∈ P)
5 addassnq 10596 . 2 ((𝑓 +Q 𝑔) +Q ) = (𝑓 +Q (𝑔 +Q ))
61, 2, 3, 4, 5genpass 10647 1 ((𝐴 +P 𝐵) +P 𝐶) = (𝐴 +P (𝐵 +P 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  (class class class)co 7231   +Q cplq 10493   +P cpp 10499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-inf2 9280
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-ov 7234  df-oprab 7235  df-mpo 7236  df-om 7663  df-1st 7779  df-2nd 7780  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-1o 8222  df-oadd 8226  df-omul 8227  df-er 8411  df-ni 10510  df-pli 10511  df-mi 10512  df-lti 10513  df-plpq 10546  df-mpq 10547  df-ltpq 10548  df-enq 10549  df-nq 10550  df-erq 10551  df-plq 10552  df-mq 10553  df-1nq 10554  df-rq 10555  df-ltnq 10556  df-np 10619  df-plp 10621
This theorem is referenced by:  ltaprlem  10682  enrer  10701  addcmpblnr  10707  mulcmpblnrlem  10708  ltsrpr  10715  addasssr  10726  mulasssr  10728  distrsr  10729  m1p1sr  10730  m1m1sr  10731  ltsosr  10732  0idsr  10735  1idsr  10736  ltasr  10738  recexsrlem  10741  mulgt0sr  10743  map2psrpr  10748
  Copyright terms: Public domain W3C validator