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	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 +P 𝐵 ) ∈ P )

Proof

Step	Hyp	Ref	Expression
1		df-plp	⊢ +P = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 +Q 𝑧 ) } )
2		addclnq	⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 +Q 𝑧 ) ∈ Q )
3		ltanq	⊢ ( ℎ ∈ Q → ( 𝑓 <Q 𝑔 ↔ ( ℎ +Q 𝑓 ) <Q ( ℎ +Q 𝑔 ) ) )
4		addcomnq	⊢ ( 𝑥 +Q 𝑦 ) = ( 𝑦 +Q 𝑥 )
5		addclprlem2	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 +Q ℎ ) → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) )
6	1 2 3 4 5	genpcl	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 +P 𝐵 ) ∈ P )