Metamath Proof Explorer

Theorem subaddmulsub

Description: The difference with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023)

Ref Expression
Assertion subaddmulsub ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → E − A + B ⁢ C − D = E - A ⁢ C - B ⁢ C + A ⁢ D + B ⁢ D

Proof

Step Hyp Ref Expression
1 addmulsub ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ⁢ C − D = A ⁢ C + B ⁢ C - A ⁢ D + B ⁢ D
2 1 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → A + B ⁢ C − D = A ⁢ C + B ⁢ C - A ⁢ D + B ⁢ D
3 2 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → E − A + B ⁢ C − D = E − A ⁢ C + B ⁢ C - A ⁢ D + B ⁢ D
4 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → E ∈ ℂ
5 simp1l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → A ∈ ℂ
6 simp2l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → C ∈ ℂ
7 5 6 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → A ⁢ C ∈ ℂ
8 simp1r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → B ∈ ℂ
9 8 6 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → B ⁢ C ∈ ℂ
10 7 9 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → A ⁢ C + B ⁢ C ∈ ℂ
11 simp2r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → D ∈ ℂ
12 5 11 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → A ⁢ D ∈ ℂ
13 8 11 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → B ⁢ D ∈ ℂ
14 12 13 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → A ⁢ D + B ⁢ D ∈ ℂ
15 4 10 14 subsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → E − A ⁢ C + B ⁢ C - A ⁢ D + B ⁢ D = E − A ⁢ C + B ⁢ C + A ⁢ D + B ⁢ D
16 4 7 9 subsub4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → E - A ⁢ C - B ⁢ C = E − A ⁢ C + B ⁢ C
17 16 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → E − A ⁢ C + B ⁢ C = E - A ⁢ C - B ⁢ C
18 17 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → E − A ⁢ C + B ⁢ C + A ⁢ D + B ⁢ D = E - A ⁢ C - B ⁢ C + A ⁢ D + B ⁢ D
19 3 15 18 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ E ∈ ℂ → E − A + B ⁢ C − D = E - A ⁢ C - B ⁢ C + A ⁢ D + B ⁢ D