Metamath Proof Explorer

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 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⋅ 𝑷 B ∈ 𝑷

Proof

Step Hyp Ref Expression
1 df-mp ⊢ ⋅ 𝑷 = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y ⋅ 𝑸 z
2 mulclnq ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y ⋅ 𝑸 z ∈ 𝑸
3 ltmnq ⊢ h ∈ 𝑸 → f < 𝑸 g ↔ h ⋅ 𝑸 f < 𝑸 h ⋅ 𝑸 g
4 mulcomnq ⊢ x ⋅ 𝑸 y = y ⋅ 𝑸 x
5 mulclprlem ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B ∧ x ∈ 𝑸 → x < 𝑸 g ⋅ 𝑸 h → x ∈ A ⋅ 𝑷 B
6 1 2 3 4 5 genpcl ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⋅ 𝑷 B ∈ 𝑷