Metamath Proof Explorer

Theorem redivdird

Description: Distribution of division over addition. (Contributed by SN, 9-Apr-2026)

Ref Expression
Hypotheses rediv23d.a ⊢ φ → A ∈ ℝ
rediv23d.b ⊢ φ → B ∈ ℝ
rediv23d.c ⊢ φ → C ∈ ℝ
rediv23d.z ⊢ φ → C ≠ 0
Assertion redivdird ⊢ φ → A + B / ℝ C = A / ℝ C + B / ℝ C

Proof

Step Hyp Ref Expression
1 rediv23d.a ⊢ φ → A ∈ ℝ
2 rediv23d.b ⊢ φ → B ∈ ℝ
3 rediv23d.c ⊢ φ → C ∈ ℝ
4 rediv23d.z ⊢ φ → C ≠ 0
5 3 recnd ⊢ φ → C ∈ ℂ
6 1 3 4 sn-redivcld ⊢ φ → A / ℝ C ∈ ℝ
7 6 recnd ⊢ φ → A / ℝ C ∈ ℂ
8 2 3 4 sn-redivcld ⊢ φ → B / ℝ C ∈ ℝ
9 8 recnd ⊢ φ → B / ℝ C ∈ ℂ
10 5 7 9 adddid ⊢ φ → C ⁢ A / ℝ C + B / ℝ C = C ⁢ A / ℝ C + C ⁢ B / ℝ C
11 1 3 4 redivcan2d ⊢ φ → C ⁢ A / ℝ C = A
12 2 3 4 redivcan2d ⊢ φ → C ⁢ B / ℝ C = B
13 11 12 oveq12d ⊢ φ → C ⁢ A / ℝ C + C ⁢ B / ℝ C = A + B
14 10 13 eqtrd ⊢ φ → C ⁢ A / ℝ C + B / ℝ C = A + B
15 1 2 readdcld ⊢ φ → A + B ∈ ℝ
16 6 8 readdcld ⊢ φ → A / ℝ C + B / ℝ C ∈ ℝ
17 15 16 3 4 redivmuld ⊢ φ → A + B / ℝ C = A / ℝ C + B / ℝ C ↔ C ⁢ A / ℝ C + B / ℝ C = A + B
18 14 17 mpbird ⊢ φ → A + B / ℝ C = A / ℝ C + B / ℝ C