HomeRelated theorems
GIF version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Addition of complex numbers is commutative. Axiom 9 of 25 for real and complex numbers, derived from ZF set theory. |
| Ref | Expression |
|---|---|
| axaddcom | ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ) → (A + B) = (B + A)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfcnqs 5254 | . 2 ⊢ ℂ = ((R × R) / ◡E) | |
| 2 | addcnsrec 5255 | . 2 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ (z ∈ R ⋀ w ∈ R)) → ([⟨x, y⟩]◡E + [⟨z, w⟩]◡E) = [⟨(x +R z), (y +R w)⟩]◡E) | |
| 3 | addcnsrec 5255 | . 2 ⊢ (((z ∈ R ⋀ w ∈ R) ⋀ (x ∈ R ⋀ y ∈ R)) → ([⟨z, w⟩]◡E + [⟨x, y⟩]◡E) = [⟨(z +R x), (w +R y)⟩]◡E) | |
| 4 | visset 1809 | . . 3 ⊢ x ∈ V | |
| 5 | visset 1809 | . . 3 ⊢ z ∈ V | |
| 6 | 4, 5 | addcomsr 5188 | . 2 ⊢ (x +R z) = (z +R x) |
| 7 | visset 1809 | . . 3 ⊢ y ∈ V | |
| 8 | visset 1809 | . . 3 ⊢ w ∈ V | |
| 9 | 7, 8 | addcomsr 5188 | . 2 ⊢ (y +R w) = (w +R y) |
| 10 | 1, 2, 3, 6, 9 | ecoprcom 4320 | 1 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ) → (A + B) = (B + A)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 3 ⋀ wa 223 = wceq 954 ∈ wcel 956 Ecep 2827 ◡ccnv 3169 (class class class)co 3965 Rcnr 4985 +R cplr 4989 ℂcc 5224 + caddc 5229 |
| This theorem is referenced by: addcomt 5297 addcom 5314 addid2t 5321 add12t 5328 add23t 5329 add42t 5331 cnegextlem1 5337 cnegextlem3 5339 addcan 5343 addcan2t 5345 subsub23t 5368 addsubt 5376 addsub12t 5378 pncan2t 5390 negsubdi2t 5450 sub23t 5457 nnncan1t 5459 sub4t 5468 pnpcan2t 5471 ppncant 5473 ltadd2t 5618 leadd2t 5620 ltsubadd2t 5622 lesubadd2t 5624 ltaddsub2t 5626 leaddsub2t 5628 addgtge0t 5642 ltaddpos2t 5645 addge02t 5666 conjmult 5773 recp1lt1 5869 recrecltt 5870 nnleltp1t 5921 nn0nnaddclt 6093 zaddclt 6132 zneo 6167 zneoOLD 6168 shftval2t 6304 shftval4t 6306 fzshftralt 6474 seqzval2t 6505 subsqt 6593 bernneq2 6604 rimul 6695 imret 6730 fsumrev 6987 fsumshft 6989 bcxmas 7034 climshft2 7063 climaddc2 7075 efaddlem14 7313 ef1tllem 7343 cosnegt 7405 addcost 7421 sincossqt 7423 cos2tt 7425 absefit 7444 demoivre 7446 nn0ennn 7459 ioo2bl 7876 cnaddabl 8091 addinv 8093 ipval2 8320 hhph 9019 golem1 10171 stcltrlem1 10176 cdj3lem3b 10335 truni1 10458 2wsms 10546 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2689 ax-sep 2699 ax-nul 2706 ax-pow 2738 ax-pr 2775 ax-un 2865 ax-inf2 4617 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2500 df-int 2530 df-iun 2564 df-br 2616 df-opab 2663 df-tr 2677 df-eprel 2829 df-id 2832 df-po 2839 df-so 2849 df-fr 2916 df-we 2933 df-ord 2950 df-on 2951 df-lim 2952 df-suc 2953 df-om 3132 df-xp 3184 df-rel 3185 df-cnv 3186 df-co 3187 df-dm 3188 df-rn 3189 df-res 3190 df-ima 3191 df-fun 3192 df-fn 3193 df-f 3194 df-fv 3198 df-rdg 3934 df-opr 3967 df-oprab 3968 df-1st 4080 df-2nd 4081 df-1o 4134 df-oadd 4136 df-omul 4137 df-er 4262 df-ec 4264 df-qs 4267 df-ni 4992 df-pli 4993 df-mi 4994 df-lti 4995 df-plpq 5027 df-mpq 5028 df-enq 5029 df-nq 5030 df-plq 5031 df-mq 5032 df-rq 5033 df-ltq 5034 df-1q 5035 df-np 5078 df-plp 5080 df-ltp 5082 df-plpr 5156 df-enr 5158 df-nr 5159 df-plr 5160 df-c 5232 df-plus 5237 |