![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > addclpr | Structured version Visualization version GIF version |
Description: Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |
Ref | Expression |
---|---|
addclpr | ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) ∈ P) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-plp 9968 | . 2 ⊢ +P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦 +Q 𝑧)}) | |
2 | addclnq 9930 | . 2 ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦 +Q 𝑧) ∈ Q) | |
3 | ltanq 9956 | . 2 ⊢ (ℎ ∈ Q → (𝑓 <Q 𝑔 ↔ (ℎ +Q 𝑓) <Q (ℎ +Q 𝑔))) | |
4 | addcomnq 9936 | . 2 ⊢ (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥) | |
5 | addclprlem2 10002 | . 2 ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔 +Q ℎ) → 𝑥 ∈ (𝐴 +P 𝐵))) | |
6 | 1, 2, 3, 4, 5 | genpcl 9993 | 1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) ∈ P) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2127 (class class class)co 6801 +Q cplq 9840 Pcnp 9844 +P cpp 9846 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-inf2 8699 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-ral 3043 df-rex 3044 df-reu 3045 df-rmo 3046 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-pss 3719 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-tp 4314 df-op 4316 df-uni 4577 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-tr 4893 df-id 5162 df-eprel 5167 df-po 5175 df-so 5176 df-fr 5213 df-we 5215 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-pred 5829 df-ord 5875 df-on 5876 df-lim 5877 df-suc 5878 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-om 7219 df-1st 7321 df-2nd 7322 df-wrecs 7564 df-recs 7625 df-rdg 7663 df-1o 7717 df-oadd 7721 df-omul 7722 df-er 7899 df-ni 9857 df-pli 9858 df-mi 9859 df-lti 9860 df-plpq 9893 df-mpq 9894 df-ltpq 9895 df-enq 9896 df-nq 9897 df-erq 9898 df-plq 9899 df-mq 9900 df-1nq 9901 df-rq 9902 df-ltnq 9903 df-np 9966 df-plp 9968 |
This theorem is referenced by: addasspr 10007 distrlem1pr 10010 distrlem4pr 10011 ltaddpr 10019 ltexprlem7 10027 ltaprlem 10029 ltapr 10030 addcanpr 10031 enrer 10049 addcmpblnr 10053 mulcmpblnr 10055 ltsrpr 10061 1sr 10065 m1r 10066 addclsr 10067 mulclsr 10068 addasssr 10072 mulasssr 10074 distrsr 10075 m1p1sr 10076 m1m1sr 10077 ltsosr 10078 0lt1sr 10079 0idsr 10081 1idsr 10082 00sr 10083 ltasr 10084 recexsrlem 10087 mulgt0sr 10089 mappsrpr 10092 |
Copyright terms: Public domain | W3C validator |