mulclpr - Intuitionistic Logic Explorer

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

Theorem mulclpr 7792

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.

Step	Hyp	Ref	Expression
1		df-imp 7689	. . . 4 ⊢ ·_P = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^st ‘𝑤) ∧ 𝑧 ∈ (1^st ‘𝑣) ∧ 𝑥 = (𝑦 ·_Q 𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^nd ‘𝑤) ∧ 𝑧 ∈ (2^nd ‘𝑣) ∧ 𝑥 = (𝑦 ·_Q 𝑧))}⟩)
2	1	genpelxp 7731	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·_P 𝐵) ∈ (𝒫 Q × 𝒫 Q))
3		mulclnq 7596	. . . 4 ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦 ·_Q 𝑧) ∈ Q)
4	1, 3	genpml 7737	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑞 ∈ Q 𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)))
5	1, 3	genpmu 7738	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑟 ∈ Q 𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)))
6	2, 4, 5	jca32 310	. 2 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((𝐴 ·_P 𝐵) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)))))
7		ltmnqg 7621	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <_Q 𝑦 ↔ (𝑧 ·_Q 𝑥) <_Q (𝑧 ·_Q 𝑦)))
8		mulcomnqg 7603	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ·_Q 𝑦) = (𝑦 ·_Q 𝑥))
9		mulnqprl 7788	. . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝑢 ∈ (1^st ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝑡 ∈ (1^st ‘𝐵))) ∧ 𝑥 ∈ Q) → (𝑥 <_Q (𝑢 ·_Q 𝑡) → 𝑥 ∈ (1^st ‘(𝐴 ·_P 𝐵))))
10	1, 3, 7, 8, 9	genprndl 7741	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(𝐴 ·_P 𝐵)))))
11		mulnqpru 7789	. . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝑢 ∈ (2^nd ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝑡 ∈ (2^nd ‘𝐵))) ∧ 𝑥 ∈ Q) → ((𝑢 ·_Q 𝑡) <_Q 𝑥 → 𝑥 ∈ (2^nd ‘(𝐴 ·_P 𝐵))))
12	1, 3, 7, 8, 11	genprndu 7742	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑟 ∈ Q (𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑞 ∈ (2^nd ‘(𝐴 ·_P 𝐵)))))
13	10, 12	jca 306	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(𝐴 ·_P 𝐵)))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑞 ∈ (2^nd ‘(𝐴 ·_P 𝐵))))))
14	1, 3, 7, 8	genpdisj 7743	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∧ 𝑞 ∈ (2^nd ‘(𝐴 ·_P 𝐵))))
15		mullocpr 7791	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_Q 𝑟 → (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∨ 𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)))))
16	13, 14, 15	3jca 1203	. 2 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(𝐴 ·_P 𝐵)))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑞 ∈ (2^nd ‘(𝐴 ·_P 𝐵))))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∧ 𝑞 ∈ (2^nd ‘(𝐴 ·_P 𝐵))) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_Q 𝑟 → (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∨ 𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵))))))
17		elnp1st2nd 7696	. 2 ⊢ ((𝐴 ·_P 𝐵) ∈ P ↔ (((𝐴 ·_P 𝐵) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)))) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(𝐴 ·_P 𝐵)))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑞 ∈ (2^nd ‘(𝐴 ·_P 𝐵))))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∧ 𝑞 ∈ (2^nd ‘(𝐴 ·_P 𝐵))) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_Q 𝑟 → (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∨ 𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)))))))
18	6, 16, 17	sylanbrc 417	1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·_P 𝐵) ∈ P)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 715 ∧ w3a 1004 ∈ wcel 2202 ∀wral 2510 ∃wrex 2511 𝒫 cpw 3652 class class class wbr 4088 × cxp 4723 ‘cfv 5326 (class class class)co 6018 1^st c1st 6301 2^nd c2nd 6302 Qcnq 7500 ·_Q cmq 7503 <_Q cltq 7505 Pcnp 7511 ·_P cmp 7514

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-ral 2515 df-rex 2516 df-reu 2517 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-eprel 4386 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-ov 6021 df-oprab 6022 df-mpo 6023 df-1st 6303 df-2nd 6304 df-recs 6471 df-irdg 6536 df-1o 6582 df-2o 6583 df-oadd 6586 df-omul 6587 df-er 6702 df-ec 6704 df-qs 6708 df-ni 7524 df-pli 7525 df-mi 7526 df-lti 7527 df-plpq 7564 df-mpq 7565 df-enq 7567 df-nqqs 7568 df-plqqs 7569 df-mqqs 7570 df-1nqqs 7571 df-rq 7572 df-ltnqqs 7573 df-enq0 7644 df-nq0 7645 df-0nq0 7646 df-plq0 7647 df-mq0 7648 df-inp 7686 df-imp 7689

This theorem is referenced by: mulnqprlemfl 7795 mulnqprlemfu 7796 mulnqpr 7797 mulassprg 7801 distrlem1prl 7802 distrlem1pru 7803 distrlem4prl 7804 distrlem4pru 7805 distrlem5prl 7806 distrlem5pru 7807 distrprg 7808 1idpr 7812 recexprlemex 7857 ltmprr 7862 mulcmpblnrlemg 7960 mulcmpblnr 7961 mulclsr 7974 mulcomsrg 7977 mulasssrg 7978 distrsrg 7979 m1m1sr 7981 1idsr 7988 00sr 7989 recexgt0sr 7993 mulgt0sr 7998 mulextsr1lem 8000 mulextsr1 8001 recidpirq 8078

W3C validator