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