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	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{\cdot }_{𝑷}B\in 𝑷$$

Proof

Step	Hyp	Ref	Expression
1		df-mp	$$⊢{\cdot }_{𝑷}=\left(w\in 𝑷,v\in 𝑷⟼\left\{x|\exists y\in w\exists z\in vx=y{\cdot }_{𝑸}z\right\}\right)$$
2		mulclnq	$$⊢\left(y\in 𝑸\wedge z\in 𝑸\right)\to y{\cdot }_{𝑸}z\in 𝑸$$
3		ltmnq	$$⊢h\in 𝑸\to \left(f{<}_{𝑸}g\leftrightarrow \left(h{\cdot }_{𝑸}f\right){<}_{𝑸}\left(h{\cdot }_{𝑸}g\right)\right)$$
4		mulcomnq	$$⊢x{\cdot }_{𝑸}y=y{\cdot }_{𝑸}x$$
5		mulclprlem	$$⊢\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{\cdot }_{𝑸}h\right)\to x\in \left(A{\cdot }_{𝑷}B\right)\right)$$
6	1 2 3 4 5	genpcl	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{\cdot }_{𝑷}B\in 𝑷$$