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+BC=AC+BC

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→1C∈ℂ
4 3 3ad2ant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→1C∈ℂ
5 1 2 4 adddird ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A+B⁢1C=A⁢1C+B⁢1C
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+BC=A+B⁢1C
10 6 7 8 9 syl3anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A+BC=A+B⁢1C
11 divrec ⊢A∈ℂ∧C∈ℂ∧C≠0→AC=A⁢1C
12 1 7 8 11 syl3anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC=A⁢1C
13 divrec ⊢B∈ℂ∧C∈ℂ∧C≠0→BC=B⁢1C
14 2 7 8 13 syl3anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→BC=B⁢1C
15 12 14 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC+BC=A⁢1C+B⁢1C
16 5 10 15 3eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A+BC=AC+BC