Metamath Proof Explorer

Theorem addcomd

Description: Addition is commutative. 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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
addcomd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion addcomd ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )

Proof

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