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

Metamath Proof Explorer

Theorem resubdi

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

Ref Expression
Assertion resubdi 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( B -R C ) ) = ( ( A x. B ) -R ( A x. C ) ) )

Proof

Step Hyp Ref Expression
1 remulcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
2 1 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
3 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
4 rersubcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
5 4 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
6 3 5 remulcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( B -R C ) ) e. RR )
7 3 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
8 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
9 8 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. CC )
10 5 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B -R C ) e. CC )
11 7 9 10 adddid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( C + ( B -R C ) ) ) = ( ( A x. C ) + ( A x. ( B -R C ) ) ) )
12 repncan3 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + ( B -R C ) ) = B )
13 12 ancoms 
 |-  ( ( B e. RR /\ C e. RR ) -> ( C + ( B -R C ) ) = B )
14 13 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + ( B -R C ) ) = B )
15 14 oveq2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( C + ( B -R C ) ) ) = ( A x. B ) )
16 11 15 eqtr3d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) + ( A x. ( B -R C ) ) ) = ( A x. B ) )
17 2 6 16 reladdrsub 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( B -R C ) ) = ( ( A x. B ) -R ( A x. C ) ) )