Theorem addasspr

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.)

	Ref	Expression
Assertion	addasspr	$$⊢\left(A{+}_{𝑷}B\right){+}_{𝑷}C=A{+}_{𝑷}\left(B{+}_{𝑷}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-plp	$$⊢{+}_{𝑷}=\left(w\in 𝑷,v\in 𝑷⟼\left\{x|\exists y\in w\exists z\in vx=y{+}_{𝑸}z\right\}\right)$$
2		addclnq	$$⊢\left(y\in 𝑸\wedge z\in 𝑸\right)\to y{+}_{𝑸}z\in 𝑸$$
3		dmplp	$$⊢\mathrm{dom}{+}_{𝑷}=𝑷\times 𝑷$$
4		addclpr	$$⊢\left(f\in 𝑷\wedge g\in 𝑷\right)\to f{+}_{𝑷}g\in 𝑷$$
5		addassnq	$$⊢\left(f{+}_{𝑸}g\right){+}_{𝑸}h=f{+}_{𝑸}\left(g{+}_{𝑸}h\right)$$
6	1 2 3 4 5	genpass	$$⊢\left(A{+}_{𝑷}B\right){+}_{𝑷}C=A{+}_{𝑷}\left(B{+}_{𝑷}C\right)$$