| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. Axiom 10 of 23 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-addass 6894. |
| Ref | Expression |
|---|---|
| axaddass |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfcnqs 6857 |
. 2
| |
| 2 | addcnsrec 6858 |
. 2
| |
| 3 | addcnsrec 6858 |
. 2
| |
| 4 | addcnsrec 6858 |
. 2
| |
| 5 | addcnsrec 6858 |
. 2
| |
| 6 | addclsr 6787 |
. . . 4
| |
| 7 | addclsr 6787 |
. . . 4
| |
| 8 | 6, 7 | anim12i 632 |
. . 3
|
| 9 | 8 | an4s 941 |
. 2
|
| 10 | addclsr 6787 |
. . . 4
| |
| 11 | addclsr 6787 |
. . . 4
| |
| 12 | 10, 11 | anim12i 632 |
. . 3
|
| 13 | 12 | an4s 941 |
. 2
|
| 14 | visset 2572 |
. . 3
| |
| 15 | visset 2572 |
. . 3
| |
| 16 | 14, 15 | addasssr 6792 |
. 2
|
| 17 | visset 2572 |
. . 3
| |
| 18 | visset 2572 |
. . 3
| |
| 19 | 17, 18 | addasssr 6792 |
. 2
|
| 20 | 1, 2, 3, 4, 5, 9, 13, 16, 19 | ecoprass 5583 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1621 ax-gen 1622 ax-8 1623 ax-9 1624 ax-10 1625 ax-11 1626 ax-12 1627 ax-13 1628 ax-14 1629 ax-17 1634 ax-4 1637 ax-5o 1639 ax-6o 1642 ax-9o 1792 ax-10o 1810 ax-16 1883 ax-11o 1893 ax-ext 2152 ax-rep 3628 ax-sep 3638 ax-nul 3645 ax-pow 3681 ax-pr 3719 ax-un 3961 ax-inf2 6008 |
| This theorem depends on definitions: df-bi 232 df-or 434 df-an 435 df-3or 1131 df-3an 1132 df-ex 1645 df-sb 1845 df-eu 2070 df-mo 2071 df-clab 2158 df-cleq 2163 df-clel 2166 df-ne 2297 df-ral 2389 df-rex 2390 df-reu 2391 df-rab 2392 df-v 2571 df-sbc 2731 df-csb 2806 df-dif 2862 df-un 2864 df-in 2866 df-ss 2868 df-pss 2870 df-nul 3115 df-if 3213 df-pw 3261 df-sn 3274 df-pr 3275 df-tp 3277 df-op 3278 df-uni 3399 df-int 3433 df-iun 3470 df-br 3540 df-opab 3598 df-tr 3612 df-eprel 3776 df-id 3779 df-po 3784 df-so 3796 df-fr 3814 df-we 3830 df-ord 3846 df-on 3847 df-lim 3848 df-suc 3849 df-om 4118 df-xp 4165 df-rel 4166 df-cnv 4167 df-co 4168 df-dm 4169 df-rn 4170 df-res 4171 df-ima 4172 df-fun 4173 df-fn 4174 df-f 4175 df-fv 4179 df-opr 5022 df-oprab 5023 df-1st 5166 df-2nd 5167 df-rdg 5344 df-1o 5384 df-oadd 5386 df-omul 5387 df-er 5519 df-ec 5521 df-qs 5524 df-ni 6595 df-pli 6596 df-mi 6597 df-lti 6598 df-plpq 6630 df-mpq 6631 df-enq 6632 df-nq 6633 df-plq 6634 df-mq 6635 df-rq 6636 df-ltq 6637 df-1q 6638 df-np 6681 df-plp 6683 df-ltp 6685 df-plpr 6759 df-enr 6761 df-nr 6762 df-plr 6763 df-c 6835 df-plus 6840 |