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 e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )

Proof

Step Hyp Ref Expression
1 1cnd 
 |-  ( ( A e. CC /\ B e. CC ) -> 1 e. CC )
2 1 1 addcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 1 + 1 ) e. CC )
3 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
4 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
5 2 3 4 adddid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) )
6 3 4 addcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
7 1p1times 
 |-  ( ( A + B ) e. CC -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
8 6 7 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
9 1p1times 
 |-  ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
10 1p1times 
 |-  ( B e. CC -> ( ( 1 + 1 ) x. B ) = ( B + B ) )
11 9 10 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) = ( ( A + A ) + ( B + B ) ) )
12 5 8 11 3eqtr3rd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + A ) + ( B + B ) ) = ( ( A + B ) + ( A + B ) ) )
13 3 3 addcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + A ) e. CC )
14 13 4 4 addassd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + A ) + B ) + B ) = ( ( A + A ) + ( B + B ) ) )
15 6 3 4 addassd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) + A ) + B ) = ( ( A + B ) + ( A + B ) ) )
16 12 14 15 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) )
17 13 4 addcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + A ) + B ) e. CC )
18 6 3 addcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + A ) e. CC )
19 addcan2 
 |-  ( ( ( ( A + A ) + B ) e. CC /\ ( ( A + B ) + A ) e. CC /\ B e. CC ) -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
20 17 18 4 19 syl3anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
21 16 20 mpbid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + A ) + B ) = ( ( A + B ) + A ) )
22 3 3 4 addassd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + A ) + B ) = ( A + ( A + B ) ) )
23 3 4 3 addassd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + A ) = ( A + ( B + A ) ) )
24 21 22 23 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + ( A + B ) ) = ( A + ( B + A ) ) )
25 4 3 addcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B + A ) e. CC )
26 addcan 
 |-  ( ( A e. CC /\ ( A + B ) e. CC /\ ( B + A ) e. CC ) -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
27 3 6 25 26 syl3anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
28 24 27 mpbid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )