mulclpr - Intuitionistic Logic Explorer

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

Theorem mulclpr 7639

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 7536	. . . 4 ⊢ ·_P = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^st ‘𝑤) ∧ 𝑧 ∈ (1^st ‘𝑣) ∧ 𝑥 = (𝑦 ·_Q 𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^nd ‘𝑤) ∧ 𝑧 ∈ (2^nd ‘𝑣) ∧ 𝑥 = (𝑦 ·_Q 𝑧))}⟩)
2	1	genpelxp 7578	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·_P 𝐵) ∈ (𝒫 Q × 𝒫 Q))
3		mulclnq 7443	. . . 4 ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦 ·_Q 𝑧) ∈ Q)
4	1, 3	genpml 7584	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑞 ∈ Q 𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)))
5	1, 3	genpmu 7585	. . 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 7468	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <_Q 𝑦 ↔ (𝑧 ·_Q 𝑥) <_Q (𝑧 ·_Q 𝑦)))
8		mulcomnqg 7450	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ·_Q 𝑦) = (𝑦 ·_Q 𝑥))
9		mulnqprl 7635	. . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝑢 ∈ (1^st ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝑡 ∈ (1^st ‘𝐵))) ∧ 𝑥 ∈ Q) → (𝑥 <_Q (𝑢 ·_Q 𝑡) → 𝑥 ∈ (1^st ‘(𝐴 ·_P 𝐵))))
10	1, 3, 7, 8, 9	genprndl 7588	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(𝐴 ·_P 𝐵)))))
11		mulnqpru 7636	. . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝑢 ∈ (2^nd ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝑡 ∈ (2^nd ‘𝐵))) ∧ 𝑥 ∈ Q) → ((𝑢 ·_Q 𝑡) <_Q 𝑥 → 𝑥 ∈ (2^nd ‘(𝐴 ·_P 𝐵))))
12	1, 3, 7, 8, 11	genprndu 7589	. . . 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 7590	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∧ 𝑞 ∈ (2^nd ‘(𝐴 ·_P 𝐵))))
15		mullocpr 7638	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_Q 𝑟 → (𝑞 ∈ (1^st ‘(𝐴 ·_P 𝐵)) ∨ 𝑟 ∈ (2^nd ‘(𝐴 ·_P 𝐵)))))
16	13, 14, 15	3jca 1179	. 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 7543	. 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 709 ∧ w3a 980 ∈ wcel 2167 ∀wral 2475 ∃wrex 2476 𝒫 cpw 3605 class class class wbr 4033 × cxp 4661 ‘cfv 5258 (class class class)co 5922 1^st c1st 6196 2^nd c2nd 6197 Qcnq 7347 ·_Q cmq 7350 <_Q cltq 7352 Pcnp 7358 ·_P cmp 7361

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-ral 2480 df-rex 2481 df-reu 2482 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-eprel 4324 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-irdg 6428 df-1o 6474 df-2o 6475 df-oadd 6478 df-omul 6479 df-er 6592 df-ec 6594 df-qs 6598 df-ni 7371 df-pli 7372 df-mi 7373 df-lti 7374 df-plpq 7411 df-mpq 7412 df-enq 7414 df-nqqs 7415 df-plqqs 7416 df-mqqs 7417 df-1nqqs 7418 df-rq 7419 df-ltnqqs 7420 df-enq0 7491 df-nq0 7492 df-0nq0 7493 df-plq0 7494 df-mq0 7495 df-inp 7533 df-imp 7536

This theorem is referenced by: mulnqprlemfl 7642 mulnqprlemfu 7643 mulnqpr 7644 mulassprg 7648 distrlem1prl 7649 distrlem1pru 7650 distrlem4prl 7651 distrlem4pru 7652 distrlem5prl 7653 distrlem5pru 7654 distrprg 7655 1idpr 7659 recexprlemex 7704 ltmprr 7709 mulcmpblnrlemg 7807 mulcmpblnr 7808 mulclsr 7821 mulcomsrg 7824 mulasssrg 7825 distrsrg 7826 m1m1sr 7828 1idsr 7835 00sr 7836 recexgt0sr 7840 mulgt0sr 7845 mulextsr1lem 7847 mulextsr1 7848 recidpirq 7925

W3C validator