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

Metamath Proof Explorer

Theorem rediv23d

Description: A "commutative"/associative law for division. (Contributed by SN, 9-Apr-2026)

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

Proof

Step Hyp Ref Expression
1 rediv23d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 rediv23d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 rediv23d.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 rediv23d.z ⊢ ( 𝜑 → 𝐶 ≠ 0 )
5 3 4 sn-rereccld ⊢ ( 𝜑 → ( 1 /ℝ 𝐶 ) ∈ ℝ )
6 5 recnd ⊢ ( 𝜑 → ( 1 /ℝ 𝐶 ) ∈ ℂ )
7 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
8 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
9 6 7 8 mulassd ⊢ ( 𝜑 → ( ( ( 1 /ℝ 𝐶 ) · 𝐴 ) · 𝐵 ) = ( ( 1 /ℝ 𝐶 ) · ( 𝐴 · 𝐵 ) ) )
10 1 3 4 redivrec2d ⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐶 ) = ( ( 1 /ℝ 𝐶 ) · 𝐴 ) )
11 10 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) · 𝐵 ) = ( ( ( 1 /ℝ 𝐶 ) · 𝐴 ) · 𝐵 ) )
12 1 2 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
13 12 3 4 redivrec2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) /ℝ 𝐶 ) = ( ( 1 /ℝ 𝐶 ) · ( 𝐴 · 𝐵 ) ) )
14 9 11 13 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) /ℝ 𝐶 ) = ( ( 𝐴 /ℝ 𝐶 ) · 𝐵 ) )