Theorem resubdi

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

	Ref	Expression
Assertion	resubdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · ( 𝐵 −ℝ 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) −ℝ ( 𝐴 · 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		remulcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
2	1	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
3		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
4		rersubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
5	4	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
6	3 5	remulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · ( 𝐵 −ℝ 𝐶 ) ) ∈ ℝ )
7	3	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
8		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
9	8	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
10	5	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℂ )
11	7 9 10	adddid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) ) = ( ( 𝐴 · 𝐶 ) + ( 𝐴 · ( 𝐵 −ℝ 𝐶 ) ) ) )
12		repncan3	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
13	12	ancoms	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
14	13	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
15	14	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) ) = ( 𝐴 · 𝐵 ) )
16	11 15	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 𝐶 ) + ( 𝐴 · ( 𝐵 −ℝ 𝐶 ) ) ) = ( 𝐴 · 𝐵 ) )
17	2 6 16	reladdrsub	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · ( 𝐵 −ℝ 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) −ℝ ( 𝐴 · 𝐶 ) ) )