resubdi

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

		Ref	Expression
	Assertion	resubdi	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A (B -_{ℝ} C) = A B -_{ℝ} A C$

Step	Hyp	Ref	Expression
1		remulcl	$⊢ (A \in ℝ \land C \in ℝ) \to A C \in ℝ$
2	1	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A C \in ℝ$
3		simp1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
4		rersubcl	$⊢ (B \in ℝ \land C \in ℝ) \to B -_{ℝ} C \in ℝ$
5	4	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B -_{ℝ} C \in ℝ$
6	3 5	remulcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A (B -_{ℝ} C) \in ℝ$
7	3	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
8		simp3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to C \in ℝ$
9	8	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to C \in ℂ$
10	5	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B -_{ℝ} C \in ℂ$
11	7 9 10	adddid	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A (C + (B -_{ℝ} C)) = A C + A (B -_{ℝ} C)$
12		repncan3	$⊢ (C \in ℝ \land B \in ℝ) \to C + (B -_{ℝ} C) = B$
13	12	ancoms	$⊢ (B \in ℝ \land C \in ℝ) \to C + (B -_{ℝ} C) = B$
14	13	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to C + (B -_{ℝ} C) = B$
15	14	oveq2d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A (C + (B -_{ℝ} C)) = A B$
16	11 15	eqtr3d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A C + A (B -_{ℝ} C) = A B$
17	2 6 16	reladdrsub	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A (B -_{ℝ} C) = A B -_{ℝ} A C$

Metamath Proof Explorer