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 + B C = A + B C

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 + B C = C ⁢ A C + B C
5 3 4 syld3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B C = C ⁢ A C + B C
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 ⁢ A C = A
10 8 9 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C = A
11 10 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C + B C = A + B C
12 5 11 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B C = A + B C