# Metamath Proof Explorer

## Theorem divdir

Description: Distribution of division over addition. (Contributed by NM, 31-Jul-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion divdir $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A + B C = A C + B C$

### Proof

Step Hyp Ref Expression
1 simp1 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ∈ ℂ$
2 simp2 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ$
3 reccl $⊢ C ∈ ℂ ∧ C ≠ 0 → 1 C ∈ ℂ$
4 3 3ad2ant3 $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → 1 C ∈ ℂ$
5 1 2 4 adddird $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A + B ⁢ 1 C = A ⁢ 1 C + B ⁢ 1 C$
6 1 2 addcld $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A + B ∈ ℂ$
7 simp3l $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ$
8 simp3r $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ≠ 0$
9 divrec $⊢ A + B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A + B C = A + B ⁢ 1 C$
10 6 7 8 9 syl3anc $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A + B C = A + B ⁢ 1 C$
11 divrec $⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = A ⁢ 1 C$
12 1 7 8 11 syl3anc $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = A ⁢ 1 C$
13 divrec $⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C = B ⁢ 1 C$
14 2 7 8 13 syl3anc $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C = B ⁢ 1 C$
15 12 14 oveq12d $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C + B C = A ⁢ 1 C + B ⁢ 1 C$
16 5 10 15 3eqtr4d $⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A + B C = A C + B C$