Metamath Proof Explorer

Theorem resubdi

Description: Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023)

Ref Expression
Assertion resubdi ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ B - ℝ C = A ⁢ B - ℝ A ⁢ C

Proof

Step Hyp Ref Expression
1 remulcl ⊢ A ∈ ℝ ∧ C ∈ ℝ → A ⁢ C ∈ ℝ
2 1 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ C ∈ ℝ
3 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
4 rersubcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
5 4 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
6 3 5 remulcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ B - ℝ C ∈ ℝ
7 3 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℂ
8 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
9 8 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℂ
10 5 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℂ
11 7 9 10 adddid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ C + B - ℝ C = A ⁢ C + A ⁢ B - ℝ C
12 repncan3 ⊢ C ∈ ℝ ∧ B ∈ ℝ → C + B - ℝ C = B
13 12 ancoms ⊢ B ∈ ℝ ∧ C ∈ ℝ → C + B - ℝ C = B
14 13 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + B - ℝ C = B
15 14 oveq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ C + B - ℝ C = A ⁢ B
16 11 15 eqtr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ C + A ⁢ B - ℝ C = A ⁢ B
17 2 6 16 reladdrsub ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ B - ℝ C = A ⁢ B - ℝ A ⁢ C