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

Proof

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