Metamath Proof Explorer

Theorem addcomd

Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses muld.1 ⊢φ→A∈ℂ
addcomd.2 ⊢φ→B∈ℂ
Assertion addcomd ⊢φ→A+B=B+A

Proof

Step Hyp Ref Expression
1 muld.1 ⊢φ→A∈ℂ
2 addcomd.2 ⊢φ→B∈ℂ
3 1cnd ⊢φ→1∈ℂ
4 3 3 addcld ⊢φ→1+1∈ℂ
5 4 1 2 adddid ⊢φ→1+1⁢A+B=1+1⁢A+1+1⁢B
6 1 2 addcld ⊢φ→A+B∈ℂ
7 1p1times ⊢A+B∈ℂ→1+1⁢A+B=A+B+A+B
8 6 7 syl ⊢φ→1+1⁢A+B=A+B+A+B
9 1p1times ⊢A∈ℂ→1+1⁢A=A+A
10 1 9 syl ⊢φ→1+1⁢A=A+A
11 1p1times ⊢B∈ℂ→1+1⁢B=B+B
12 2 11 syl ⊢φ→1+1⁢B=B+B
13 10 12 oveq12d ⊢φ→1+1⁢A+1+1⁢B=A+A+B+B
14 5 8 13 3eqtr3rd ⊢φ→A+A+B+B=A+B+A+B
15 1 1 addcld ⊢φ→A+A∈ℂ
16 15 2 2 addassd ⊢φ→A+A+B+B=A+A+B+B
17 6 1 2 addassd ⊢φ→A+B+A+B=A+B+A+B
18 14 16 17 3eqtr4d ⊢φ→A+A+B+B=A+B+A+B
19 15 2 addcld ⊢φ→A+A+B∈ℂ
20 6 1 addcld ⊢φ→A+B+A∈ℂ
21 addcan2 ⊢A+A+B∈ℂ∧A+B+A∈ℂ∧B∈ℂ→A+A+B+B=A+B+A+B↔A+A+B=A+B+A
22 19 20 2 21 syl3anc ⊢φ→A+A+B+B=A+B+A+B↔A+A+B=A+B+A
23 18 22 mpbid ⊢φ→A+A+B=A+B+A
24 1 1 2 addassd ⊢φ→A+A+B=A+A+B
25 1 2 1 addassd ⊢φ→A+B+A=A+B+A
26 23 24 25 3eqtr3d ⊢φ→A+A+B=A+B+A
27 2 1 addcld ⊢φ→B+A∈ℂ
28 addcan ⊢A∈ℂ∧A+B∈ℂ∧B+A∈ℂ→A+A+B=A+B+A↔A+B=B+A
29 1 6 27 28 syl3anc ⊢φ→A+A+B=A+B+A↔A+B=B+A
30 26 29 mpbid ⊢φ→A+B=B+A