# Metamath Proof Explorer

Description: Addition commutes. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion addcom ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}={B}+{A}$

### Proof

Step Hyp Ref Expression
1 1cnd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to 1\in ℂ$
2 1 1 addcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to 1+1\in ℂ$
3 simpl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}\in ℂ$
4 simpr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {B}\in ℂ$
5 2 3 4 adddid ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(1+1\right)\left({A}+{B}\right)=\left(1+1\right){A}+\left(1+1\right){B}$
6 3 4 addcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}\in ℂ$
7 1p1times ${⊢}{A}+{B}\in ℂ\to \left(1+1\right)\left({A}+{B}\right)={A}+{B}+{A}+{B}$
8 6 7 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(1+1\right)\left({A}+{B}\right)={A}+{B}+{A}+{B}$
9 1p1times ${⊢}{A}\in ℂ\to \left(1+1\right){A}={A}+{A}$
10 1p1times ${⊢}{B}\in ℂ\to \left(1+1\right){B}={B}+{B}$
11 9 10 oveqan12d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(1+1\right){A}+\left(1+1\right){B}={A}+{A}+{B}+{B}$
12 5 8 11 3eqtr3rd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{A}+{B}+{B}={A}+{B}+{A}+{B}$
13 3 3 addcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{A}\in ℂ$
14 13 4 4 addassd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({A}+{A}\right)+{B}+{B}={A}+{A}+{B}+{B}$
15 6 3 4 addassd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({A}+{B}\right)+{A}+{B}={A}+{B}+{A}+{B}$
16 12 14 15 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({A}+{A}\right)+{B}+{B}=\left({A}+{B}\right)+{A}+{B}$
17 13 4 addcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{A}+{B}\in ℂ$
18 6 3 addcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}+{A}\in ℂ$
19 addcan2 ${⊢}\left({A}+{A}+{B}\in ℂ\wedge {A}+{B}+{A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({A}+{A}\right)+{B}+{B}=\left({A}+{B}\right)+{A}+{B}↔{A}+{A}+{B}={A}+{B}+{A}\right)$
20 17 18 4 19 syl3anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left({A}+{A}\right)+{B}+{B}=\left({A}+{B}\right)+{A}+{B}↔{A}+{A}+{B}={A}+{B}+{A}\right)$
21 16 20 mpbid ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{A}+{B}={A}+{B}+{A}$
22 3 3 4 addassd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{A}+{B}={A}+{A}+{B}$
23 3 4 3 addassd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}+{A}={A}+{B}+{A}$
24 21 22 23 3eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{A}+{B}={A}+{B}+{A}$
25 4 3 addcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {B}+{A}\in ℂ$
26 addcan ${⊢}\left({A}\in ℂ\wedge {A}+{B}\in ℂ\wedge {B}+{A}\in ℂ\right)\to \left({A}+{A}+{B}={A}+{B}+{A}↔{A}+{B}={B}+{A}\right)$
27 3 6 25 26 syl3anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({A}+{A}+{B}={A}+{B}+{A}↔{A}+{B}={B}+{A}\right)$
28 24 27 mpbid ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}={B}+{A}$