![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > axaddcom | GIF version |
Description: Addition commutes. Axiom
for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly, nor should the proven axiom ax-addcom 7208 be used later.
Instead, use addcom 7382.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.) |
Ref | Expression |
---|---|
axaddcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-c 7119 | . 2 ⊢ ℂ = (R × R) | |
2 | oveq1 5571 | . . 3 ⊢ (〈𝑥, 𝑦〉 = 𝐴 → (〈𝑥, 𝑦〉 + 〈𝑧, 𝑤〉) = (𝐴 + 〈𝑧, 𝑤〉)) | |
3 | oveq2 5572 | . . 3 ⊢ (〈𝑥, 𝑦〉 = 𝐴 → (〈𝑧, 𝑤〉 + 〈𝑥, 𝑦〉) = (〈𝑧, 𝑤〉 + 𝐴)) | |
4 | 2, 3 | eqeq12d 2097 | . 2 ⊢ (〈𝑥, 𝑦〉 = 𝐴 → ((〈𝑥, 𝑦〉 + 〈𝑧, 𝑤〉) = (〈𝑧, 𝑤〉 + 〈𝑥, 𝑦〉) ↔ (𝐴 + 〈𝑧, 𝑤〉) = (〈𝑧, 𝑤〉 + 𝐴))) |
5 | oveq2 5572 | . . 3 ⊢ (〈𝑧, 𝑤〉 = 𝐵 → (𝐴 + 〈𝑧, 𝑤〉) = (𝐴 + 𝐵)) | |
6 | oveq1 5571 | . . 3 ⊢ (〈𝑧, 𝑤〉 = 𝐵 → (〈𝑧, 𝑤〉 + 𝐴) = (𝐵 + 𝐴)) | |
7 | 5, 6 | eqeq12d 2097 | . 2 ⊢ (〈𝑧, 𝑤〉 = 𝐵 → ((𝐴 + 〈𝑧, 𝑤〉) = (〈𝑧, 𝑤〉 + 𝐴) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) |
8 | addcomsrg 7064 | . . . . 5 ⊢ ((𝑥 ∈ R ∧ 𝑧 ∈ R) → (𝑥 +R 𝑧) = (𝑧 +R 𝑥)) | |
9 | 8 | ad2ant2r 493 | . . . 4 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → (𝑥 +R 𝑧) = (𝑧 +R 𝑥)) |
10 | addcomsrg 7064 | . . . . 5 ⊢ ((𝑦 ∈ R ∧ 𝑤 ∈ R) → (𝑦 +R 𝑤) = (𝑤 +R 𝑦)) | |
11 | 10 | ad2ant2l 492 | . . . 4 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → (𝑦 +R 𝑤) = (𝑤 +R 𝑦)) |
12 | 9, 11 | opeq12d 3598 | . . 3 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → 〈(𝑥 +R 𝑧), (𝑦 +R 𝑤)〉 = 〈(𝑧 +R 𝑥), (𝑤 +R 𝑦)〉) |
13 | addcnsr 7134 | . . 3 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → (〈𝑥, 𝑦〉 + 〈𝑧, 𝑤〉) = 〈(𝑥 +R 𝑧), (𝑦 +R 𝑤)〉) | |
14 | addcnsr 7134 | . . . 4 ⊢ (((𝑧 ∈ R ∧ 𝑤 ∈ R) ∧ (𝑥 ∈ R ∧ 𝑦 ∈ R)) → (〈𝑧, 𝑤〉 + 〈𝑥, 𝑦〉) = 〈(𝑧 +R 𝑥), (𝑤 +R 𝑦)〉) | |
15 | 14 | ancoms 264 | . . 3 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → (〈𝑧, 𝑤〉 + 〈𝑥, 𝑦〉) = 〈(𝑧 +R 𝑥), (𝑤 +R 𝑦)〉) |
16 | 12, 13, 15 | 3eqtr4d 2125 | . 2 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → (〈𝑥, 𝑦〉 + 〈𝑧, 𝑤〉) = (〈𝑧, 𝑤〉 + 〈𝑥, 𝑦〉)) |
17 | 1, 4, 7, 16 | 2optocl 4463 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 = wceq 1285 ∈ wcel 1434 〈cop 3419 (class class class)co 5564 Rcnr 6619 +R cplr 6623 ℂcc 7111 + caddc 7116 |
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 3913 ax-sep 3916 ax-nul 3924 ax-pow 3968 ax-pr 3992 ax-un 4216 ax-setind 4308 ax-iinf 4357 |
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 2612 df-sbc 2825 df-csb 2918 df-dif 2984 df-un 2986 df-in 2988 df-ss 2995 df-nul 3268 df-pw 3402 df-sn 3422 df-pr 3423 df-op 3425 df-uni 3622 df-int 3657 df-iun 3700 df-br 3806 df-opab 3860 df-mpt 3861 df-tr 3896 df-eprel 4072 df-id 4076 df-po 4079 df-iso 4080 df-iord 4149 df-on 4151 df-suc 4154 df-iom 4360 df-xp 4397 df-rel 4398 df-cnv 4399 df-co 4400 df-dm 4401 df-rn 4402 df-res 4403 df-ima 4404 df-iota 4917 df-fun 4954 df-fn 4955 df-f 4956 df-f1 4957 df-fo 4958 df-f1o 4959 df-fv 4960 df-ov 5567 df-oprab 5568 df-mpt2 5569 df-1st 5819 df-2nd 5820 df-recs 5975 df-irdg 6040 df-1o 6086 df-2o 6087 df-oadd 6090 df-omul 6091 df-er 6194 df-ec 6196 df-qs 6200 df-ni 6626 df-pli 6627 df-mi 6628 df-lti 6629 df-plpq 6666 df-mpq 6667 df-enq 6669 df-nqqs 6670 df-plqqs 6671 df-mqqs 6672 df-1nqqs 6673 df-rq 6674 df-ltnqqs 6675 df-enq0 6746 df-nq0 6747 df-0nq0 6748 df-plq0 6749 df-mq0 6750 df-inp 6788 df-iplp 6790 df-enr 7035 df-nr 7036 df-plr 7037 df-c 7119 df-add 7124 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |