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

Theorem mulclpr 6552
 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 ((A P B P) → (A ·P B) P)

Proof of Theorem mulclpr
Dummy variables 𝑞 𝑟 𝑡 u v w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-imp 6451 . . . 4 ·P = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y ·Q z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y ·Q z))}⟩)
21genpelxp 6493 . . 3 ((A P B P) → (A ·P B) (𝒫 Q × 𝒫 Q))
3 mulclnq 6360 . . . 4 ((y Q z Q) → (y ·Q z) Q)
41, 3genpml 6499 . . 3 ((A P B P) → 𝑞 Q 𝑞 (1st ‘(A ·P B)))
51, 3genpmu 6500 . . 3 ((A P B P) → 𝑟 Q 𝑟 (2nd ‘(A ·P B)))
62, 4, 5jca32 293 . 2 ((A P B P) → ((A ·P B) (𝒫 Q × 𝒫 Q) (𝑞 Q 𝑞 (1st ‘(A ·P B)) 𝑟 Q 𝑟 (2nd ‘(A ·P B)))))
7 ltmnqg 6385 . . . . 5 ((x Q y Q z Q) → (x <Q y ↔ (z ·Q x) <Q (z ·Q y)))
8 mulcomnqg 6367 . . . . 5 ((x Q y Q) → (x ·Q y) = (y ·Q x))
9 mulnqprl 6548 . . . . 5 ((((A P u (1stA)) (B P 𝑡 (1stB))) x Q) → (x <Q (u ·Q 𝑡) → x (1st ‘(A ·P B))))
101, 3, 7, 8, 9genprndl 6503 . . . 4 ((A P B P) → 𝑞 Q (𝑞 (1st ‘(A ·P B)) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st ‘(A ·P B)))))
11 mulnqpru 6549 . . . . 5 ((((A P u (2ndA)) (B P 𝑡 (2ndB))) x Q) → ((u ·Q 𝑡) <Q xx (2nd ‘(A ·P B))))
121, 3, 7, 8, 11genprndu 6504 . . . 4 ((A P B P) → 𝑟 Q (𝑟 (2nd ‘(A ·P B)) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd ‘(A ·P B)))))
1310, 12jca 290 . . 3 ((A P B P) → (𝑞 Q (𝑞 (1st ‘(A ·P B)) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st ‘(A ·P B)))) 𝑟 Q (𝑟 (2nd ‘(A ·P B)) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd ‘(A ·P B))))))
141, 3, 7, 8genpdisj 6505 . . 3 ((A P B P) → 𝑞 Q ¬ (𝑞 (1st ‘(A ·P B)) 𝑞 (2nd ‘(A ·P B))))
15 mullocpr 6551 . . 3 ((A P B P) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B)))))
1613, 14, 153jca 1083 . 2 ((A P B P) → ((𝑞 Q (𝑞 (1st ‘(A ·P B)) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st ‘(A ·P B)))) 𝑟 Q (𝑟 (2nd ‘(A ·P B)) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd ‘(A ·P B))))) 𝑞 Q ¬ (𝑞 (1st ‘(A ·P B)) 𝑞 (2nd ‘(A ·P B))) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B))))))
17 elnp1st2nd 6458 . 2 ((A ·P B) P ↔ (((A ·P B) (𝒫 Q × 𝒫 Q) (𝑞 Q 𝑞 (1st ‘(A ·P B)) 𝑟 Q 𝑟 (2nd ‘(A ·P B)))) ((𝑞 Q (𝑞 (1st ‘(A ·P B)) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st ‘(A ·P B)))) 𝑟 Q (𝑟 (2nd ‘(A ·P B)) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd ‘(A ·P B))))) 𝑞 Q ¬ (𝑞 (1st ‘(A ·P B)) 𝑞 (2nd ‘(A ·P B))) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B)))))))
186, 16, 17sylanbrc 394 1 ((A P B P) → (A ·P B) P)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301  𝒫 cpw 3351   class class class wbr 3755   × cxp 4286  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264   ·Q cmq 6267
 Copyright terms: Public domain W3C validator