Metamath Proof Explorer

Theorem xrge0adddi

Description: Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Assertion xrge0adddi 
|- ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( C *e ( A +e B ) ) = ( ( C *e A ) +e ( C *e B ) ) )

Proof

Step Hyp Ref Expression
1 xrge0adddir 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( ( A +e B ) *e C ) = ( ( A *e C ) +e ( B *e C ) ) )
2 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
3 simp1 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> A e. ( 0 [,] +oo ) )
4 2 3 sselid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> A e. RR* )
5 simp2 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> B e. ( 0 [,] +oo ) )
6 2 5 sselid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> B e. RR* )
7 4 6 xaddcld 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( A +e B ) e. RR* )
8 simp3 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> C e. ( 0 [,] +oo ) )
9 2 8 sselid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> C e. RR* )
10 xmulcom 
 |-  ( ( ( A +e B ) e. RR* /\ C e. RR* ) -> ( ( A +e B ) *e C ) = ( C *e ( A +e B ) ) )
11 7 9 10 syl2anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( ( A +e B ) *e C ) = ( C *e ( A +e B ) ) )
12 xmulcom 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A *e C ) = ( C *e A ) )
13 4 9 12 syl2anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( A *e C ) = ( C *e A ) )
14 xmulcom 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B *e C ) = ( C *e B ) )
15 6 9 14 syl2anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( B *e C ) = ( C *e B ) )
16 13 15 oveq12d 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( ( A *e C ) +e ( B *e C ) ) = ( ( C *e A ) +e ( C *e B ) ) )
17 1 11 16 3eqtr3d 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( C *e ( A +e B ) ) = ( ( C *e A ) +e ( C *e B ) ) )