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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	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	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )