This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnapbmcpd

Description: ((a+b)-c)+d = ((a+d)+b)-c holds for complex numbers a,b,c,d. (Contributed by Alexander van der Vekens, 23-Mar-2018)

Ref Expression
Assertion cnapbmcpd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐵 ) − 𝐶 ) + 𝐷 ) = ( ( ( 𝐴 + 𝐷 ) + 𝐵 ) − 𝐶 ) )

Proof

Step Hyp Ref Expression
1 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
2 1 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
3 simpr ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → 𝐷 ∈ ℂ )
4 3 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → 𝐷 ∈ ℂ )
5 simpl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → 𝐶 ∈ ℂ )
6 5 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → 𝐶 ∈ ℂ )
7 2 4 6 addsubd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐵 ) + 𝐷 ) − 𝐶 ) = ( ( ( 𝐴 + 𝐵 ) − 𝐶 ) + 𝐷 ) )
8 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → 𝐴 ∈ ℂ )
10 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → 𝐵 ∈ ℂ )
12 9 11 4 add32d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) + 𝐷 ) = ( ( 𝐴 + 𝐷 ) + 𝐵 ) )
13 12 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐵 ) + 𝐷 ) − 𝐶 ) = ( ( ( 𝐴 + 𝐷 ) + 𝐵 ) − 𝐶 ) )
14 7 13 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐵 ) − 𝐶 ) + 𝐷 ) = ( ( ( 𝐴 + 𝐷 ) + 𝐵 ) − 𝐶 ) )