addclpr - Intuitionistic Logic Explorer

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

Theorem addclpr 7756

Description: Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. Combination of Lemma 11.13 and Lemma 11.16 in [BauerTaylor], p. 53. (Contributed by NM, 13-Mar-1996.)

**Assertion**
Ref	Expression
addclpr	⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +_P 𝐵) ∈ P)

Proof of Theorem addclpr Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑔 ℎ 𝑞 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iplp 7687	. . . 4 ⊢ +_P = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^st ‘𝑤) ∧ 𝑧 ∈ (1^st ‘𝑣) ∧ 𝑥 = (𝑦 +_Q 𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^nd ‘𝑤) ∧ 𝑧 ∈ (2^nd ‘𝑣) ∧ 𝑥 = (𝑦 +_Q 𝑧))}⟩)
2	1	genpelxp 7730	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +_P 𝐵) ∈ (𝒫 Q × 𝒫 Q))
3		addclnq 7594	. . . 4 ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦 +_Q 𝑧) ∈ Q)
4	1, 3	genpml 7736	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑞 ∈ Q 𝑞 ∈ (1^st ‘(𝐴 +_P 𝐵)))
5	1, 3	genpmu 7737	. . 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		ltanqg 7619	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <_Q 𝑦 ↔ (𝑧 +_Q 𝑥) <_Q (𝑧 +_Q 𝑦)))
8		addcomnqg 7600	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 +_Q 𝑦) = (𝑦 +_Q 𝑥))
9		addnqprl 7748	. . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (1^st ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (1^st ‘𝐵))) ∧ 𝑥 ∈ Q) → (𝑥 <_Q (𝑔 +_Q ℎ) → 𝑥 ∈ (1^st ‘(𝐴 +_P 𝐵))))
10	1, 3, 7, 8, 9	genprndl 7740	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q (𝑞 ∈ (1^st ‘(𝐴 +_P 𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘(𝐴 +_P 𝐵)))))
11		addnqpru 7749	. . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (2^nd ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (2^nd ‘𝐵))) ∧ 𝑥 ∈ Q) → ((𝑔 +_Q ℎ) <_Q 𝑥 → 𝑥 ∈ (2^nd ‘(𝐴 +_P 𝐵))))
12	1, 3, 7, 8, 11	genprndu 7741	. . . 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 7742	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^st ‘(𝐴 +_P 𝐵)) ∧ 𝑞 ∈ (2^nd ‘(𝐴 +_P 𝐵))))
15		addlocpr 7755	. . 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 7695	. 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 6017 1^st c1st 6300 2^nd c2nd 6301 Qcnq 7499 +_Q cplq 7501 <_Q cltq 7504 Pcnp 7510 +_P cpp 7512

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 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-irdg 6535 df-1o 6581 df-2o 6582 df-oadd 6585 df-omul 6586 df-er 6701 df-ec 6703 df-qs 6707 df-ni 7523 df-pli 7524 df-mi 7525 df-lti 7526 df-plpq 7563 df-mpq 7564 df-enq 7566 df-nqqs 7567 df-plqqs 7568 df-mqqs 7569 df-1nqqs 7570 df-rq 7571 df-ltnqqs 7572 df-enq0 7643 df-nq0 7644 df-0nq0 7645 df-plq0 7646 df-mq0 7647 df-inp 7685 df-iplp 7687

This theorem is referenced by: addnqprlemfl 7778 addnqprlemfu 7779 addnqpr 7780 addassprg 7798 distrlem1prl 7801 distrlem1pru 7802 distrlem4prl 7803 distrlem4pru 7804 distrprg 7807 ltaddpr 7816 ltexpri 7832 addcanprleml 7833 addcanprlemu 7834 ltaprlem 7837 ltaprg 7838 prplnqu 7839 addextpr 7840 caucvgprlemcanl 7863 cauappcvgprlemladdru 7875 cauappcvgprlemladdrl 7876 cauappcvgprlemladd 7877 cauappcvgprlem1 7878 caucvgprlemladdrl 7897 caucvgprlem1 7898 caucvgprprlemnbj 7912 caucvgprprlemopu 7918 caucvgprprlemloc 7922 caucvgprprlemexbt 7925 caucvgprprlemexb 7926 caucvgprprlemaddq 7927 caucvgprprlem2 7929 enrer 7954 addcmpblnr 7958 mulcmpblnrlemg 7959 mulcmpblnr 7960 ltsrprg 7966 1sr 7970 m1r 7971 addclsr 7972 mulclsr 7973 addasssrg 7975 mulasssrg 7977 distrsrg 7978 m1p1sr 7979 m1m1sr 7980 lttrsr 7981 ltsosr 7983 0lt1sr 7984 0idsr 7986 1idsr 7987 00sr 7988 ltasrg 7989 recexgt0sr 7992 mulgt0sr 7997 aptisr 7998 mulextsr1lem 7999 mulextsr1 8000 archsr 8001 srpospr 8002 prsrcl 8003 prsradd 8005 prsrlt 8006 caucvgsrlemcau 8012 caucvgsrlemgt1 8014 mappsrprg 8023 map2psrprg 8024 pitonnlem1p1 8065 pitonnlem2 8066 pitonn 8067 pitoregt0 8068 pitore 8069 recnnre 8070 recidpirqlemcalc 8076 recidpirq 8077

W3C validator