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

Metamath Proof Explorer

Theorem muldivdid

Description: Distribution of division over addition with a multiplication. (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Hypotheses muldivdid.1 ⊢ φ → A ∈ ℂ
muldivdid.2 ⊢ φ → B ∈ ℂ
muldivdid.3 ⊢ φ → C ∈ ℂ
muldivdid.4 ⊢ φ → B ≠ 0
Assertion muldivdid ⊢ φ → A ⁢ B + C B = A + C B

Proof

Step Hyp Ref Expression
1 muldivdid.1 ⊢ φ → A ∈ ℂ
2 muldivdid.2 ⊢ φ → B ∈ ℂ
3 muldivdid.3 ⊢ φ → C ∈ ℂ
4 muldivdid.4 ⊢ φ → B ≠ 0
5 1 2 mulcomd ⊢ φ → A ⁢ B = B ⁢ A
6 5 oveq1d ⊢ φ → A ⁢ B + C = B ⁢ A + C
7 6 oveq1d ⊢ φ → A ⁢ B + C B = B ⁢ A + C B
8 muldivdir ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⁢ A + C B = A + C B
9 1 3 2 4 8 syl112anc ⊢ φ → B ⁢ A + C B = A + C B
10 7 9 eqtrd ⊢ φ → A ⁢ B + C B = A + C B