![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addassprg | GIF version |
Description: Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.) |
Ref | Expression |
---|---|
addassprg | ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 +P 𝐵) +P 𝐶) = (𝐴 +P (𝐵 +P 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iplp 6797 | . 2 ⊢ +P = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦 +Q 𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2nd ‘𝑤) ∧ 𝑧 ∈ (2nd ‘𝑣) ∧ 𝑥 = (𝑦 +Q 𝑧))}〉) | |
2 | addclnq 6704 | . 2 ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦 +Q 𝑧) ∈ Q) | |
3 | dmplp 6869 | . 2 ⊢ dom +P = (P × P) | |
4 | addclpr 6866 | . 2 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓 +P 𝑔) ∈ P) | |
5 | addassnqg 6711 | . 2 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓 +Q 𝑔) +Q ℎ) = (𝑓 +Q (𝑔 +Q ℎ))) | |
6 | 1, 2, 3, 4, 5 | genpassg 6855 | 1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 +P 𝐵) +P 𝐶) = (𝐴 +P (𝐵 +P 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 920 = wceq 1285 ∈ wcel 1434 (class class class)co 5565 +Q cplq 6611 Pcnp 6620 +P cpp 6622 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-coll 3914 ax-sep 3917 ax-nul 3925 ax-pow 3969 ax-pr 3993 ax-un 4217 ax-setind 4309 ax-iinf 4358 |
This theorem depends on definitions: df-bi 115 df-dc 777 df-3or 921 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ne 2250 df-ral 2358 df-rex 2359 df-reu 2360 df-rab 2362 df-v 2613 df-sbc 2826 df-csb 2919 df-dif 2985 df-un 2987 df-in 2989 df-ss 2996 df-nul 3269 df-pw 3403 df-sn 3423 df-pr 3424 df-op 3426 df-uni 3623 df-int 3658 df-iun 3701 df-br 3807 df-opab 3861 df-mpt 3862 df-tr 3897 df-eprel 4073 df-id 4077 df-po 4080 df-iso 4081 df-iord 4150 df-on 4152 df-suc 4155 df-iom 4361 df-xp 4398 df-rel 4399 df-cnv 4400 df-co 4401 df-dm 4402 df-rn 4403 df-res 4404 df-ima 4405 df-iota 4918 df-fun 4955 df-fn 4956 df-f 4957 df-f1 4958 df-fo 4959 df-f1o 4960 df-fv 4961 df-ov 5568 df-oprab 5569 df-mpt2 5570 df-1st 5820 df-2nd 5821 df-recs 5976 df-irdg 6041 df-1o 6087 df-2o 6088 df-oadd 6091 df-omul 6092 df-er 6195 df-ec 6197 df-qs 6201 df-ni 6633 df-pli 6634 df-mi 6635 df-lti 6636 df-plpq 6673 df-mpq 6674 df-enq 6676 df-nqqs 6677 df-plqqs 6678 df-mqqs 6679 df-1nqqs 6680 df-rq 6681 df-ltnqqs 6682 df-enq0 6753 df-nq0 6754 df-0nq0 6755 df-plq0 6756 df-mq0 6757 df-inp 6795 df-iplp 6797 |
This theorem is referenced by: ltaprlem 6947 ltaprg 6948 caucvgprlemcanl 6973 caucvgprprlemexb 7036 caucvgprprlemaddq 7037 enrer 7051 addcmpblnr 7055 mulcmpblnrlemg 7056 ltsrprg 7063 addasssrg 7072 mulasssrg 7074 distrsrg 7075 m1p1sr 7076 m1m1sr 7077 lttrsr 7078 ltsosr 7080 0idsr 7083 1idsr 7084 ltasrg 7086 recexgt0sr 7089 mulgt0sr 7093 mulextsr1lem 7095 srpospr 7098 prsradd 7101 prsrlt 7102 pitonnlem1p1 7153 pitoregt0 7156 recidpirqlemcalc 7164 |
Copyright terms: Public domain | W3C validator |