Metamath Proof Explorer

Theorem xrge0adddir

Description: Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
2 simpl1 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C e. ( 0 [,) +oo ) ) -> A e. ( 0 [,] +oo ) )
3 1 2 sselid 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C e. ( 0 [,) +oo ) ) -> A e. RR* )
4 simpl2 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C e. ( 0 [,) +oo ) ) -> B e. ( 0 [,] +oo ) )
5 1 4 sselid 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C e. ( 0 [,) +oo ) ) -> B e. RR* )
6 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
7 simpr 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C e. ( 0 [,) +oo ) ) -> C e. ( 0 [,) +oo ) )
8 6 7 sselid 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C e. ( 0 [,) +oo ) ) -> C e. RR )
9 xadddir 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( ( A +e B ) *e C ) = ( ( A *e C ) +e ( B *e C ) ) )
10 3 5 8 9 syl3anc 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C e. ( 0 [,) +oo ) ) -> ( ( A +e B ) *e C ) = ( ( A *e C ) +e ( B *e C ) ) )
11 simpll1 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> A e. ( 0 [,] +oo ) )
12 1 11 sselid 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> A e. RR* )
13 simpll2 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> B e. ( 0 [,] +oo ) )
14 1 13 sselid 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> B e. RR* )
15 12 14 xaddcld 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( A +e B ) e. RR* )
16 simpr 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> 0 < A )
17 xrge0addgt0 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) -> 0 < ( A +e B ) )
18 11 13 16 17 syl21anc 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> 0 < ( A +e B ) )
19 xmulpnf1 
 |-  ( ( ( A +e B ) e. RR* /\ 0 < ( A +e B ) ) -> ( ( A +e B ) *e +oo ) = +oo )
20 15 18 19 syl2anc 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( ( A +e B ) *e +oo ) = +oo )
21 oveq2 
 |-  ( C = +oo -> ( ( A +e B ) *e C ) = ( ( A +e B ) *e +oo ) )
22 21 ad2antlr 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( ( A +e B ) *e C ) = ( ( A +e B ) *e +oo ) )
23 simpll3 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> C e. ( 0 [,] +oo ) )
24 ge0xmulcl 
 |-  ( ( B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( B *e C ) e. ( 0 [,] +oo ) )
25 13 23 24 syl2anc 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( B *e C ) e. ( 0 [,] +oo ) )
26 1 25 sselid 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( B *e C ) e. RR* )
27 xrge0neqmnf 
 |-  ( ( B *e C ) e. ( 0 [,] +oo ) -> ( B *e C ) =/= -oo )
28 25 27 syl 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( B *e C ) =/= -oo )
29 xaddpnf2 
 |-  ( ( ( B *e C ) e. RR* /\ ( B *e C ) =/= -oo ) -> ( +oo +e ( B *e C ) ) = +oo )
30 26 28 29 syl2anc 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( +oo +e ( B *e C ) ) = +oo )
31 20 22 30 3eqtr4d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( ( A +e B ) *e C ) = ( +oo +e ( B *e C ) ) )
32 oveq2 
 |-  ( C = +oo -> ( A *e C ) = ( A *e +oo ) )
33 32 ad2antlr 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( A *e C ) = ( A *e +oo ) )
34 xmulpnf1 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo )
35 12 16 34 syl2anc 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( A *e +oo ) = +oo )
36 33 35 eqtrd 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( A *e C ) = +oo )
37 36 oveq1d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( ( A *e C ) +e ( B *e C ) ) = ( +oo +e ( B *e C ) ) )
38 31 37 eqtr4d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 < A ) -> ( ( A +e B ) *e C ) = ( ( A *e C ) +e ( B *e C ) ) )
39 simpll3 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> C e. ( 0 [,] +oo ) )
40 1 39 sselid 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> C e. RR* )
41 xmul02 
 |-  ( C e. RR* -> ( 0 *e C ) = 0 )
42 40 41 syl 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( 0 *e C ) = 0 )
43 42 oveq1d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( ( 0 *e C ) +e ( B *e C ) ) = ( 0 +e ( B *e C ) ) )
44 oveq1 
 |-  ( 0 = A -> ( 0 *e C ) = ( A *e C ) )
45 44 adantl 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( 0 *e C ) = ( A *e C ) )
46 45 oveq1d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( ( 0 *e C ) +e ( B *e C ) ) = ( ( A *e C ) +e ( B *e C ) ) )
47 simpll2 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> B e. ( 0 [,] +oo ) )
48 1 47 sselid 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> B e. RR* )
49 48 40 xmulcld 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( B *e C ) e. RR* )
50 xaddid2 
 |-  ( ( B *e C ) e. RR* -> ( 0 +e ( B *e C ) ) = ( B *e C ) )
51 49 50 syl 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( 0 +e ( B *e C ) ) = ( B *e C ) )
52 43 46 51 3eqtr3d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( ( A *e C ) +e ( B *e C ) ) = ( B *e C ) )
53 xaddid2 
 |-  ( B e. RR* -> ( 0 +e B ) = B )
54 48 53 syl 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( 0 +e B ) = B )
55 54 oveq1d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( ( 0 +e B ) *e C ) = ( B *e C ) )
56 oveq1 
 |-  ( 0 = A -> ( 0 +e B ) = ( A +e B ) )
57 56 oveq1d 
 |-  ( 0 = A -> ( ( 0 +e B ) *e C ) = ( ( A +e B ) *e C ) )
58 57 adantl 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( ( 0 +e B ) *e C ) = ( ( A +e B ) *e C ) )
59 52 55 58 3eqtr2rd 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) /\ 0 = A ) -> ( ( A +e B ) *e C ) = ( ( A *e C ) +e ( B *e C ) ) )
60 0xr 
 |-  0 e. RR*
61 60 a1i 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) -> 0 e. RR* )
62 simpl1 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) -> A e. ( 0 [,] +oo ) )
63 1 62 sselid 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) -> A e. RR* )
64 pnfxr 
 |-  +oo e. RR*
65 64 a1i 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) -> +oo e. RR* )
66 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ A e. ( 0 [,] +oo ) ) -> 0 <_ A )
67 61 65 62 66 syl3anc 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) -> 0 <_ A )
68 xrleloe 
 |-  ( ( 0 e. RR* /\ A e. RR* ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
69 68 biimpa 
 |-  ( ( ( 0 e. RR* /\ A e. RR* ) /\ 0 <_ A ) -> ( 0 < A \/ 0 = A ) )
70 61 63 67 69 syl21anc 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) -> ( 0 < A \/ 0 = A ) )
71 38 59 70 mpjaodan 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) /\ C = +oo ) -> ( ( A +e B ) *e C ) = ( ( A *e C ) +e ( B *e C ) ) )
72 0lepnf 
 |-  0 <_ +oo
73 eliccelico 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> ( C e. ( 0 [,] +oo ) <-> ( C e. ( 0 [,) +oo ) \/ C = +oo ) ) )
74 60 64 72 73 mp3an 
 |-  ( C e. ( 0 [,] +oo ) <-> ( C e. ( 0 [,) +oo ) \/ C = +oo ) )
75 74 3anbi3i 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) <-> ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ ( C e. ( 0 [,) +oo ) \/ C = +oo ) ) )
76 75 simp3bi 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( C e. ( 0 [,) +oo ) \/ C = +oo ) )
77 10 71 76 mpjaodan 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( ( A +e B ) *e C ) = ( ( A *e C ) +e ( B *e C ) ) )