Metamath Proof Explorer

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 
|- ( ph -> A e. CC )
addcomd.2 
|- ( ph -> B e. CC )
Assertion addcomd 
|- ( ph -> ( A + B ) = ( B + A ) )

Proof

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