Theorem mulclpr

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

	Ref	Expression
Assertion	mulclpr	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 ·P 𝐵 ) ∈ P )

Proof

Step	Hyp	Ref	Expression
1		df-mp	⊢ ·P = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 ·Q 𝑧 ) } )
2		mulclnq	⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 ·Q 𝑧 ) ∈ Q )
3		ltmnq	⊢ ( ℎ ∈ Q → ( 𝑓 <Q 𝑔 ↔ ( ℎ ·Q 𝑓 ) <Q ( ℎ ·Q 𝑔 ) ) )
4		mulcomnq	⊢ ( 𝑥 ·Q 𝑦 ) = ( 𝑦 ·Q 𝑥 )
5		mulclprlem	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) → 𝑥 ∈ ( 𝐴 ·P 𝐵 ) ) )
6	1 2 3 4 5	genpcl	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 ·P 𝐵 ) ∈ P )