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

Theorem mulclpr 7052
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 6949 . . . 4 ·P = (𝑤P, 𝑣P ↦ ⟨{𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (1st𝑤) ∧ 𝑧 ∈ (1st𝑣) ∧ 𝑥 = (𝑦 ·Q 𝑧))}, {𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (2nd𝑤) ∧ 𝑧 ∈ (2nd𝑣) ∧ 𝑥 = (𝑦 ·Q 𝑧))}⟩)
21genpelxp 6991 . . 3 ((𝐴P𝐵P) → (𝐴 ·P 𝐵) ∈ (𝒫 Q × 𝒫 Q))
3 mulclnq 6856 . . . 4 ((𝑦Q𝑧Q) → (𝑦 ·Q 𝑧) ∈ Q)
41, 3genpml 6997 . . 3 ((𝐴P𝐵P) → ∃𝑞Q 𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)))
51, 3genpmu 6998 . . 3 ((𝐴P𝐵P) → ∃𝑟Q 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))
62, 4, 5jca32 303 . 2 ((𝐴P𝐵P) → ((𝐴 ·P 𝐵) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞Q 𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∧ ∃𝑟Q 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
7 ltmnqg 6881 . . . . 5 ((𝑥Q𝑦Q𝑧Q) → (𝑥 <Q 𝑦 ↔ (𝑧 ·Q 𝑥) <Q (𝑧 ·Q 𝑦)))
8 mulcomnqg 6863 . . . . 5 ((𝑥Q𝑦Q) → (𝑥 ·Q 𝑦) = (𝑦 ·Q 𝑥))
9 mulnqprl 7048 . . . . 5 ((((𝐴P𝑢 ∈ (1st𝐴)) ∧ (𝐵P𝑡 ∈ (1st𝐵))) ∧ 𝑥Q) → (𝑥 <Q (𝑢 ·Q 𝑡) → 𝑥 ∈ (1st ‘(𝐴 ·P 𝐵))))
101, 3, 7, 8, 9genprndl 7001 . . . 4 ((𝐴P𝐵P) → ∀𝑞Q (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st ‘(𝐴 ·P 𝐵)))))
11 mulnqpru 7049 . . . . 5 ((((𝐴P𝑢 ∈ (2nd𝐴)) ∧ (𝐵P𝑡 ∈ (2nd𝐵))) ∧ 𝑥Q) → ((𝑢 ·Q 𝑡) <Q 𝑥𝑥 ∈ (2nd ‘(𝐴 ·P 𝐵))))
121, 3, 7, 8, 11genprndu 7002 . . . 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 7003 . . 3 ((𝐴P𝐵P) → ∀𝑞Q ¬ (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴 ·P 𝐵))))
15 mullocpr 7051 . . 3 ((𝐴P𝐵P) → ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
1613, 14, 153jca 1121 . 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 6956 . 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 922  wcel 1436  wral 2355  wrex 2356  𝒫 cpw 3409   class class class wbr 3814   × cxp 4402  cfv 4972  (class class class)co 5594  1st c1st 5847  2nd c2nd 5848  Qcnq 6760   ·Q cmq 6763   <Q cltq 6765  Pcnp 6771   ·P cmp 6774
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3922  ax-sep 3925  ax-nul 3933  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-setind 4319  ax-iinf 4369
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2616  df-sbc 2829  df-csb 2922  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-iun 3709  df-br 3815  df-opab 3869  df-mpt 3870  df-tr 3905  df-eprel 4083  df-id 4087  df-po 4090  df-iso 4091  df-iord 4160  df-on 4162  df-suc 4165  df-iom 4372  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-ov 5597  df-oprab 5598  df-mpt2 5599  df-1st 5849  df-2nd 5850  df-recs 6005  df-irdg 6070  df-1o 6116  df-2o 6117  df-oadd 6120  df-omul 6121  df-er 6225  df-ec 6227  df-qs 6231  df-ni 6784  df-pli 6785  df-mi 6786  df-lti 6787  df-plpq 6824  df-mpq 6825  df-enq 6827  df-nqqs 6828  df-plqqs 6829  df-mqqs 6830  df-1nqqs 6831  df-rq 6832  df-ltnqqs 6833  df-enq0 6904  df-nq0 6905  df-0nq0 6906  df-plq0 6907  df-mq0 6908  df-inp 6946  df-imp 6949
This theorem is referenced by:  mulnqprlemfl  7055  mulnqprlemfu  7056  mulnqpr  7057  mulassprg  7061  distrlem1prl  7062  distrlem1pru  7063  distrlem4prl  7064  distrlem4pru  7065  distrlem5prl  7066  distrlem5pru  7067  distrprg  7068  1idpr  7072  recexprlemex  7117  ltmprr  7122  mulcmpblnrlemg  7207  mulcmpblnr  7208  mulclsr  7221  mulcomsrg  7224  mulasssrg  7225  distrsrg  7226  m1m1sr  7228  1idsr  7235  00sr  7236  recexgt0sr  7240  mulgt0sr  7244  mulextsr1lem  7246  mulextsr1  7247  recidpirq  7316
  Copyright terms: Public domain W3C validator