Theorem addclpr

Description: Closure of addition on positive reals. First statement of Proposition 9-3.5 of Gleason p. 123. (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	addclpr	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{+}_{𝑷}B\in 𝑷$$

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		ltanq	$$⊢h\in 𝑸\to \left(f{<}_{𝑸}g\leftrightarrow \left(h{+}_{𝑸}f\right){<}_{𝑸}\left(h{+}_{𝑸}g\right)\right)$$
4		addcomnq	$$⊢x{+}_{𝑸}y=y{+}_{𝑸}x$$
5		addclprlem2	$$⊢\left(\left(\left(A\in 𝑷\wedge g\in A\right)\wedge \left(B\in 𝑷\wedge h\in B\right)\right)\wedge x\in 𝑸\right)\to \left(x{<}_{𝑸}\left(g{+}_{𝑸}h\right)\to x\in \left(A{+}_{𝑷}B\right)\right)$$
6	1 2 3 4 5	genpcl	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{+}_{𝑷}B\in 𝑷$$