Metamath Proof Explorer

Theorem addcom

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 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A

Proof

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