Metamath Proof Explorer


Theorem subadd4

Description: Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006)

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

Proof

Step Hyp Ref Expression
1 subcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝐵 ) ∈ ℂ )
2 subsub2 ( ( ( 𝐴𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐴𝐵 ) − ( 𝐶𝐷 ) ) = ( ( 𝐴𝐵 ) + ( 𝐷𝐶 ) ) )
3 2 3expb ( ( ( 𝐴𝐵 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴𝐵 ) − ( 𝐶𝐷 ) ) = ( ( 𝐴𝐵 ) + ( 𝐷𝐶 ) ) )
4 1 3 sylan ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴𝐵 ) − ( 𝐶𝐷 ) ) = ( ( 𝐴𝐵 ) + ( 𝐷𝐶 ) ) )
5 addsub4 ( ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) → ( ( 𝐴 + 𝐷 ) − ( 𝐵 + 𝐶 ) ) = ( ( 𝐴𝐵 ) + ( 𝐷𝐶 ) ) )
6 5 an42s ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐷 ) − ( 𝐵 + 𝐶 ) ) = ( ( 𝐴𝐵 ) + ( 𝐷𝐶 ) ) )
7 4 6 eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴𝐵 ) − ( 𝐶𝐷 ) ) = ( ( 𝐴 + 𝐷 ) − ( 𝐵 + 𝐶 ) ) )