This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem redivdird

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

Ref Expression
Hypotheses rediv23d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
rediv23d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
rediv23d.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
rediv23d.z ⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion redivdird ( 𝜑 → ( ( 𝐴 + 𝐵 ) /ℝ 𝐶 ) = ( ( 𝐴 /ℝ 𝐶 ) + ( 𝐵 /ℝ 𝐶 ) ) )

Proof

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