Metamath Proof Explorer

Theorem decaddcom

Description: Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023)

Ref Expression
Hypotheses decaddcom.a ⊢ 𝐴 ∈ ℕ0
decaddcom.b ⊢ 𝐵 ∈ ℕ0
decaddcom.c ⊢ 𝐶 ∈ ℕ0
Assertion decaddcom ( 𝐴 𝐵 + 𝐶 ) = ( 𝐴 𝐶 + 𝐵 )

Proof

Step Hyp Ref Expression
1 decaddcom.a ⊢ 𝐴 ∈ ℕ0
2 decaddcom.b ⊢ 𝐵 ∈ ℕ0
3 decaddcom.c ⊢ 𝐶 ∈ ℕ0
4 eqid ⊢ 𝐴 𝐵 = 𝐴 𝐵
5 eqid ⊢ ( 𝐵 + 𝐶 ) = ( 𝐵 + 𝐶 )
6 1 2 3 4 5 decaddi ⊢ ( 𝐴 𝐵 + 𝐶 ) = 𝐴 ( 𝐵 + 𝐶 )
7 eqid ⊢ 𝐴 𝐶 = 𝐴 𝐶
8 3 nn0cni ⊢ 𝐶 ∈ ℂ
9 2 nn0cni ⊢ 𝐵 ∈ ℂ
10 8 9 addcomi ⊢ ( 𝐶 + 𝐵 ) = ( 𝐵 + 𝐶 )
11 1 3 2 7 10 decaddi ⊢ ( 𝐴 𝐶 + 𝐵 ) = 𝐴 ( 𝐵 + 𝐶 )
12 6 11 eqtr4i ⊢ ( 𝐴 𝐵 + 𝐶 ) = ( 𝐴 𝐶 + 𝐵 )