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