Metamath Proof Explorer

Theorem muldivdir

Description: Distribution of division over addition with a multiplication. (Contributed by AV, 1-Jul-2021)

Ref Expression
Assertion muldivdir ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C⁢A+BC=A+BC

Proof

Step Hyp Ref Expression
1 simp3l ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C∈ℂ
2 simp1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A∈ℂ
3 1 2 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C⁢A∈ℂ
4 divdir ⊢C⁢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C⁢A+BC=C⁢AC+BC
5 3 4 syld3an1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C⁢A+BC=C⁢AC+BC
6 3anass ⊢A∈ℂ∧C∈ℂ∧C≠0↔A∈ℂ∧C∈ℂ∧C≠0
7 6 biimpri ⊢A∈ℂ∧C∈ℂ∧C≠0→A∈ℂ∧C∈ℂ∧C≠0
8 7 3adant2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A∈ℂ∧C∈ℂ∧C≠0
9 divcan3 ⊢A∈ℂ∧C∈ℂ∧C≠0→C⁢AC=A
10 8 9 syl ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C⁢AC=A
11 10 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C⁢AC+BC=A+BC
12 5 11 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→C⁢A+BC=A+BC