Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addclpr | GIF version |
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.) |
Ref | Expression |
---|---|
addclpr | ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) ∈ P) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iplp 7401 | . . . 4 ⊢ +P = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦 +Q 𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦 +Q 𝑧))}〉) | |
2 | 1 | genpelxp 7444 | . . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) ∈ (𝒫 Q × 𝒫 Q)) |
3 | addclnq 7308 | . . . 4 ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦 +Q 𝑧) ∈ Q) | |
4 | 1, 3 | genpml 7450 | . . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑞 ∈ Q 𝑞 ∈ (1st ‘(𝐴 +P 𝐵))) |
5 | 1, 3 | genpmu 7451 | . . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵))) |
6 | 2, 4, 5 | jca32 308 | . 2 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((𝐴 +P 𝐵) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵))))) |
7 | ltanqg 7333 | . . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q (𝑧 +Q 𝑦))) | |
8 | addcomnqg 7314 | . . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥)) | |
9 | addnqprl 7462 | . . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (1st ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (1st ‘𝐵))) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔 +Q ℎ) → 𝑥 ∈ (1st ‘(𝐴 +P 𝐵)))) | |
10 | 1, 3, 7, 8, 9 | genprndl 7454 | . . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘(𝐴 +P 𝐵))))) |
11 | addnqpru 7463 | . . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (2nd ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (2nd ‘𝐵))) ∧ 𝑥 ∈ Q) → ((𝑔 +Q ℎ) <Q 𝑥 → 𝑥 ∈ (2nd ‘(𝐴 +P 𝐵)))) | |
12 | 1, 3, 7, 8, 11 | genprndu 7455 | . . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘(𝐴 +P 𝐵))))) |
13 | 10, 12 | jca 304 | . . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (∀𝑞 ∈ Q (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘(𝐴 +P 𝐵)))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘(𝐴 +P 𝐵)))))) |
14 | 1, 3, 7, 8 | genpdisj 7456 | . . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴 +P 𝐵)))) |
15 | addlocpr 7469 | . . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵))))) | |
16 | 13, 14, 15 | 3jca 1166 | . 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 7409 | . 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 𝐵))))))) | |
18 | 6, 16, 17 | sylanbrc 414 | 1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) ∈ P) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 698 ∧ w3a 967 ∈ wcel 2135 ∀wral 2442 ∃wrex 2443 𝒫 cpw 3554 class class class wbr 3977 × cxp 4597 ‘cfv 5183 (class class class)co 5837 1st c1st 6099 2nd c2nd 6100 Qcnq 7213 +Q cplq 7215 <Q cltq 7218 Pcnp 7224 +P cpp 7226 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-13 2137 ax-14 2138 ax-ext 2146 ax-coll 4092 ax-sep 4095 ax-nul 4103 ax-pow 4148 ax-pr 4182 ax-un 4406 ax-setind 4509 ax-iinf 4560 |
This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 968 df-3an 969 df-tru 1345 df-fal 1348 df-nf 1448 df-sb 1750 df-eu 2016 df-mo 2017 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ne 2335 df-ral 2447 df-rex 2448 df-reu 2449 df-rab 2451 df-v 2724 df-sbc 2948 df-csb 3042 df-dif 3114 df-un 3116 df-in 3118 df-ss 3125 df-nul 3406 df-pw 3556 df-sn 3577 df-pr 3578 df-op 3580 df-uni 3785 df-int 3820 df-iun 3863 df-br 3978 df-opab 4039 df-mpt 4040 df-tr 4076 df-eprel 4262 df-id 4266 df-po 4269 df-iso 4270 df-iord 4339 df-on 4341 df-suc 4344 df-iom 4563 df-xp 4605 df-rel 4606 df-cnv 4607 df-co 4608 df-dm 4609 df-rn 4610 df-res 4611 df-ima 4612 df-iota 5148 df-fun 5185 df-fn 5186 df-f 5187 df-f1 5188 df-fo 5189 df-f1o 5190 df-fv 5191 df-ov 5840 df-oprab 5841 df-mpo 5842 df-1st 6101 df-2nd 6102 df-recs 6265 df-irdg 6330 df-1o 6376 df-2o 6377 df-oadd 6380 df-omul 6381 df-er 6493 df-ec 6495 df-qs 6499 df-ni 7237 df-pli 7238 df-mi 7239 df-lti 7240 df-plpq 7277 df-mpq 7278 df-enq 7280 df-nqqs 7281 df-plqqs 7282 df-mqqs 7283 df-1nqqs 7284 df-rq 7285 df-ltnqqs 7286 df-enq0 7357 df-nq0 7358 df-0nq0 7359 df-plq0 7360 df-mq0 7361 df-inp 7399 df-iplp 7401 |
This theorem is referenced by: addnqprlemfl 7492 addnqprlemfu 7493 addnqpr 7494 addassprg 7512 distrlem1prl 7515 distrlem1pru 7516 distrlem4prl 7517 distrlem4pru 7518 distrprg 7521 ltaddpr 7530 ltexpri 7546 addcanprleml 7547 addcanprlemu 7548 ltaprlem 7551 ltaprg 7552 prplnqu 7553 addextpr 7554 caucvgprlemcanl 7577 cauappcvgprlemladdru 7589 cauappcvgprlemladdrl 7590 cauappcvgprlemladd 7591 cauappcvgprlem1 7592 caucvgprlemladdrl 7611 caucvgprlem1 7612 caucvgprprlemnbj 7626 caucvgprprlemopu 7632 caucvgprprlemloc 7636 caucvgprprlemexbt 7639 caucvgprprlemexb 7640 caucvgprprlemaddq 7641 caucvgprprlem2 7643 enrer 7668 addcmpblnr 7672 mulcmpblnrlemg 7673 mulcmpblnr 7674 ltsrprg 7680 1sr 7684 m1r 7685 addclsr 7686 mulclsr 7687 addasssrg 7689 mulasssrg 7691 distrsrg 7692 m1p1sr 7693 m1m1sr 7694 lttrsr 7695 ltsosr 7697 0lt1sr 7698 0idsr 7700 1idsr 7701 00sr 7702 ltasrg 7703 recexgt0sr 7706 mulgt0sr 7711 aptisr 7712 mulextsr1lem 7713 mulextsr1 7714 archsr 7715 srpospr 7716 prsrcl 7717 prsradd 7719 prsrlt 7720 caucvgsrlemcau 7726 caucvgsrlemgt1 7728 mappsrprg 7737 map2psrprg 7738 pitonnlem1p1 7779 pitonnlem2 7780 pitonn 7781 pitoregt0 7782 pitore 7783 recnnre 7784 recidpirqlemcalc 7790 recidpirq 7791 |
Copyright terms: Public domain | W3C validator |