Metamath Proof Explorer

Theorem rediv23d

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

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

Proof

Step Hyp Ref Expression
1 rediv23d.a ⊢ φ → A ∈ ℝ
2 rediv23d.b ⊢ φ → B ∈ ℝ
3 rediv23d.c ⊢ φ → C ∈ ℝ
4 rediv23d.z ⊢ φ → C ≠ 0
5 3 4 sn-rereccld ⊢ φ → 1 / ℝ C ∈ ℝ
6 5 recnd ⊢ φ → 1 / ℝ C ∈ ℂ
7 1 recnd ⊢ φ → A ∈ ℂ
8 2 recnd ⊢ φ → B ∈ ℂ
9 6 7 8 mulassd ⊢ φ → 1 / ℝ C ⁢ A ⁢ B = 1 / ℝ C ⁢ A ⁢ B
10 1 3 4 redivrec2d ⊢ φ → A / ℝ C = 1 / ℝ C ⁢ A
11 10 oveq1d ⊢ φ → A / ℝ C ⁢ B = 1 / ℝ C ⁢ A ⁢ B
12 1 2 remulcld ⊢ φ → A ⁢ B ∈ ℝ
13 12 3 4 redivrec2d ⊢ φ → A ⁢ B / ℝ C = 1 / ℝ C ⁢ A ⁢ B
14 9 11 13 3eqtr4rd ⊢ φ → A ⁢ B / ℝ C = A / ℝ C ⁢ B