Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulclpr GIF version

Theorem mulclpr 6813
 Description: Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 13-Mar-1996.)
Assertion
Ref Expression
mulclpr ((𝐴P𝐵P) → (𝐴 ·P 𝐵) ∈ P)

Proof of Theorem mulclpr
Dummy variables 𝑞 𝑟 𝑡 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-imp 6710 . . . 4 ·P = (𝑤P, 𝑣P ↦ ⟨{𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (1st𝑤) ∧ 𝑧 ∈ (1st𝑣) ∧ 𝑥 = (𝑦 ·Q 𝑧))}, {𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (2nd𝑤) ∧ 𝑧 ∈ (2nd𝑣) ∧ 𝑥 = (𝑦 ·Q 𝑧))}⟩)
21genpelxp 6752 . . 3 ((𝐴P𝐵P) → (𝐴 ·P 𝐵) ∈ (𝒫 Q × 𝒫 Q))
3 mulclnq 6617 . . . 4 ((𝑦Q𝑧Q) → (𝑦 ·Q 𝑧) ∈ Q)
41, 3genpml 6758 . . 3 ((𝐴P𝐵P) → ∃𝑞Q 𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)))
51, 3genpmu 6759 . . 3 ((𝐴P𝐵P) → ∃𝑟Q 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))
62, 4, 5jca32 303 . 2 ((𝐴P𝐵P) → ((𝐴 ·P 𝐵) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞Q 𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∧ ∃𝑟Q 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
7 ltmnqg 6642 . . . . 5 ((𝑥Q𝑦Q𝑧Q) → (𝑥 <Q 𝑦 ↔ (𝑧 ·Q 𝑥) <Q (𝑧 ·Q 𝑦)))
8 mulcomnqg 6624 . . . . 5 ((𝑥Q𝑦Q) → (𝑥 ·Q 𝑦) = (𝑦 ·Q 𝑥))
9 mulnqprl 6809 . . . . 5 ((((𝐴P𝑢 ∈ (1st𝐴)) ∧ (𝐵P𝑡 ∈ (1st𝐵))) ∧ 𝑥Q) → (𝑥 <Q (𝑢 ·Q 𝑡) → 𝑥 ∈ (1st ‘(𝐴 ·P 𝐵))))
101, 3, 7, 8, 9genprndl 6762 . . . 4 ((𝐴P𝐵P) → ∀𝑞Q (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st ‘(𝐴 ·P 𝐵)))))
11 mulnqpru 6810 . . . . 5 ((((𝐴P𝑢 ∈ (2nd𝐴)) ∧ (𝐵P𝑡 ∈ (2nd𝐵))) ∧ 𝑥Q) → ((𝑢 ·Q 𝑡) <Q 𝑥𝑥 ∈ (2nd ‘(𝐴 ·P 𝐵))))
121, 3, 7, 8, 11genprndu 6763 . . . 4 ((𝐴P𝐵P) → ∀𝑟Q (𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
1310, 12jca 300 . . 3 ((𝐴P𝐵P) → (∀𝑞Q (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st ‘(𝐴 ·P 𝐵)))) ∧ ∀𝑟Q (𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd ‘(𝐴 ·P 𝐵))))))
141, 3, 7, 8genpdisj 6764 . . 3 ((𝐴P𝐵P) → ∀𝑞Q ¬ (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴 ·P 𝐵))))
15 mullocpr 6812 . . 3 ((𝐴P𝐵P) → ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
1613, 14, 153jca 1119 . 2 ((𝐴P𝐵P) → ((∀𝑞Q (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st ‘(𝐴 ·P 𝐵)))) ∧ ∀𝑟Q (𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd ‘(𝐴 ·P 𝐵))))) ∧ ∀𝑞Q ¬ (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴 ·P 𝐵))) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵))))))
17 elnp1st2nd 6717 . 2 ((𝐴 ·P 𝐵) ∈ P ↔ (((𝐴 ·P 𝐵) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞Q 𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∧ ∃𝑟Q 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))) ∧ ((∀𝑞Q (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st ‘(𝐴 ·P 𝐵)))) ∧ ∀𝑟Q (𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd ‘(𝐴 ·P 𝐵))))) ∧ ∀𝑞Q ¬ (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴 ·P 𝐵))) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))))
186, 16, 17sylanbrc 408 1 ((𝐴P𝐵P) → (𝐴 ·P 𝐵) ∈ P)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 662   ∧ w3a 920   ∈ wcel 1434  ∀wral 2349  ∃wrex 2350  𝒫 cpw 3384   class class class wbr 3787   × cxp 4363  ‘cfv 4926  (class class class)co 5537  1st c1st 5790  2nd c2nd 5791  Qcnq 6521   ·Q cmq 6524
 Copyright terms: Public domain W3C validator