Metamath Proof Explorer

Theorem xadddilem

Description: Lemma for xadddi . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xadddilem 
|- ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> A e. RR )
2 recn 
 |-  ( A e. RR -> A e. CC )
3 recn 
 |-  ( B e. RR -> B e. CC )
4 recn 
 |-  ( C e. RR -> C e. CC )
5 adddi 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
6 2 3 4 5 syl3an 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
7 6 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
8 readdcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
9 rexmul 
 |-  ( ( A e. RR /\ ( B + C ) e. RR ) -> ( A *e ( B + C ) ) = ( A x. ( B + C ) ) )
10 8 9 sylan2 
 |-  ( ( A e. RR /\ ( B e. RR /\ C e. RR ) ) -> ( A *e ( B + C ) ) = ( A x. ( B + C ) ) )
11 10 anassrs 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A *e ( B + C ) ) = ( A x. ( B + C ) ) )
12 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
13 12 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A x. B ) e. RR )
14 remulcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
15 14 adantlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A x. C ) e. RR )
16 13 15 rexaddd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A x. B ) +e ( A x. C ) ) = ( ( A x. B ) + ( A x. C ) ) )
17 7 11 16 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A *e ( B + C ) ) = ( ( A x. B ) +e ( A x. C ) ) )
18 rexadd 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B +e C ) = ( B + C ) )
19 18 adantll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( B +e C ) = ( B + C ) )
20 19 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A *e ( B +e C ) ) = ( A *e ( B + C ) ) )
21 rexmul 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A *e B ) = ( A x. B ) )
22 21 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A *e B ) = ( A x. B ) )
23 rexmul 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A *e C ) = ( A x. C ) )
24 23 adantlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A *e C ) = ( A x. C ) )
25 22 24 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A x. B ) +e ( A x. C ) ) )
26 17 20 25 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
27 1 26 sylanl1 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C e. RR ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
28 rexr 
 |-  ( A e. RR -> A e. RR* )
29 28 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR* /\ C e. RR* ) -> A e. RR* )
30 xmulpnf1 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo )
31 29 30 sylan 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( A *e +oo ) = +oo )
32 31 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) -> ( A *e +oo ) = +oo )
33 21 12 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A *e B ) e. RR )
34 1 33 sylan 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) -> ( A *e B ) e. RR )
35 rexr 
 |-  ( ( A *e B ) e. RR -> ( A *e B ) e. RR* )
36 renemnf 
 |-  ( ( A *e B ) e. RR -> ( A *e B ) =/= -oo )
37 xaddpnf1 
 |-  ( ( ( A *e B ) e. RR* /\ ( A *e B ) =/= -oo ) -> ( ( A *e B ) +e +oo ) = +oo )
38 35 36 37 syl2anc 
 |-  ( ( A *e B ) e. RR -> ( ( A *e B ) +e +oo ) = +oo )
39 34 38 syl 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) -> ( ( A *e B ) +e +oo ) = +oo )
40 32 39 eqtr4d 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) -> ( A *e +oo ) = ( ( A *e B ) +e +oo ) )
41 40 adantr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = +oo ) -> ( A *e +oo ) = ( ( A *e B ) +e +oo ) )
42 oveq2 
 |-  ( C = +oo -> ( B +e C ) = ( B +e +oo ) )
43 rexr 
 |-  ( B e. RR -> B e. RR* )
44 renemnf 
 |-  ( B e. RR -> B =/= -oo )
45 xaddpnf1 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( B +e +oo ) = +oo )
46 43 44 45 syl2anc 
 |-  ( B e. RR -> ( B +e +oo ) = +oo )
47 46 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) -> ( B +e +oo ) = +oo )
48 42 47 sylan9eqr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = +oo ) -> ( B +e C ) = +oo )
49 48 oveq2d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = +oo ) -> ( A *e ( B +e C ) ) = ( A *e +oo ) )
50 oveq2 
 |-  ( C = +oo -> ( A *e C ) = ( A *e +oo ) )
51 50 32 sylan9eqr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = +oo ) -> ( A *e C ) = +oo )
52 51 oveq2d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = +oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e B ) +e +oo ) )
53 41 49 52 3eqtr4d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = +oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
54 xmulmnf1 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e -oo ) = -oo )
55 29 54 sylan 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( A *e -oo ) = -oo )
56 55 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) -> ( A *e -oo ) = -oo )
57 56 adantr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = -oo ) -> ( A *e -oo ) = -oo )
58 34 adantr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = -oo ) -> ( A *e B ) e. RR )
59 renepnf 
 |-  ( ( A *e B ) e. RR -> ( A *e B ) =/= +oo )
60 xaddmnf1 
 |-  ( ( ( A *e B ) e. RR* /\ ( A *e B ) =/= +oo ) -> ( ( A *e B ) +e -oo ) = -oo )
61 35 59 60 syl2anc 
 |-  ( ( A *e B ) e. RR -> ( ( A *e B ) +e -oo ) = -oo )
62 58 61 syl 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = -oo ) -> ( ( A *e B ) +e -oo ) = -oo )
63 57 62 eqtr4d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = -oo ) -> ( A *e -oo ) = ( ( A *e B ) +e -oo ) )
64 oveq2 
 |-  ( C = -oo -> ( B +e C ) = ( B +e -oo ) )
65 renepnf 
 |-  ( B e. RR -> B =/= +oo )
66 xaddmnf1 
 |-  ( ( B e. RR* /\ B =/= +oo ) -> ( B +e -oo ) = -oo )
67 43 65 66 syl2anc 
 |-  ( B e. RR -> ( B +e -oo ) = -oo )
68 67 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) -> ( B +e -oo ) = -oo )
69 64 68 sylan9eqr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = -oo ) -> ( B +e C ) = -oo )
70 69 oveq2d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = -oo ) -> ( A *e ( B +e C ) ) = ( A *e -oo ) )
71 oveq2 
 |-  ( C = -oo -> ( A *e C ) = ( A *e -oo ) )
72 71 56 sylan9eqr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = -oo ) -> ( A *e C ) = -oo )
73 72 oveq2d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = -oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e B ) +e -oo ) )
74 63 70 73 3eqtr4d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) /\ C = -oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
75 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> C e. RR* )
76 elxr 
 |-  ( C e. RR* <-> ( C e. RR \/ C = +oo \/ C = -oo ) )
77 75 76 sylib 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( C e. RR \/ C = +oo \/ C = -oo ) )
78 77 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) -> ( C e. RR \/ C = +oo \/ C = -oo ) )
79 27 53 74 78 mpjao3dan 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B e. RR ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
80 31 ad2antrr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C e. RR ) -> ( A *e +oo ) = +oo )
81 1 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) -> A e. RR )
82 23 14 eqeltrd 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A *e C ) e. RR )
83 81 82 sylan 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C e. RR ) -> ( A *e C ) e. RR )
84 rexr 
 |-  ( ( A *e C ) e. RR -> ( A *e C ) e. RR* )
85 renemnf 
 |-  ( ( A *e C ) e. RR -> ( A *e C ) =/= -oo )
86 xaddpnf2 
 |-  ( ( ( A *e C ) e. RR* /\ ( A *e C ) =/= -oo ) -> ( +oo +e ( A *e C ) ) = +oo )
87 84 85 86 syl2anc 
 |-  ( ( A *e C ) e. RR -> ( +oo +e ( A *e C ) ) = +oo )
88 83 87 syl 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C e. RR ) -> ( +oo +e ( A *e C ) ) = +oo )
89 80 88 eqtr4d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C e. RR ) -> ( A *e +oo ) = ( +oo +e ( A *e C ) ) )
90 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) -> B = +oo )
91 90 oveq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) -> ( B +e C ) = ( +oo +e C ) )
92 rexr 
 |-  ( C e. RR -> C e. RR* )
93 renemnf 
 |-  ( C e. RR -> C =/= -oo )
94 xaddpnf2 
 |-  ( ( C e. RR* /\ C =/= -oo ) -> ( +oo +e C ) = +oo )
95 92 93 94 syl2anc 
 |-  ( C e. RR -> ( +oo +e C ) = +oo )
96 91 95 sylan9eq 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C e. RR ) -> ( B +e C ) = +oo )
97 96 oveq2d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C e. RR ) -> ( A *e ( B +e C ) ) = ( A *e +oo ) )
98 oveq2 
 |-  ( B = +oo -> ( A *e B ) = ( A *e +oo ) )
99 98 31 sylan9eqr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) -> ( A *e B ) = +oo )
100 99 adantr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C e. RR ) -> ( A *e B ) = +oo )
101 100 oveq1d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C e. RR ) -> ( ( A *e B ) +e ( A *e C ) ) = ( +oo +e ( A *e C ) ) )
102 89 97 101 3eqtr4d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C e. RR ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
103 pnfxr 
 |-  +oo e. RR*
104 pnfnemnf 
 |-  +oo =/= -oo
105 xaddpnf1 
 |-  ( ( +oo e. RR* /\ +oo =/= -oo ) -> ( +oo +e +oo ) = +oo )
106 103 104 105 mp2an 
 |-  ( +oo +e +oo ) = +oo
107 31 31 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( ( A *e +oo ) +e ( A *e +oo ) ) = ( +oo +e +oo ) )
108 106 107 31 3eqtr4a 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( ( A *e +oo ) +e ( A *e +oo ) ) = ( A *e +oo ) )
109 108 ad2antrr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C = +oo ) -> ( ( A *e +oo ) +e ( A *e +oo ) ) = ( A *e +oo ) )
110 98 50 oveqan12d 
 |-  ( ( B = +oo /\ C = +oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e +oo ) +e ( A *e +oo ) ) )
111 110 adantll 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C = +oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e +oo ) +e ( A *e +oo ) ) )
112 oveq12 
 |-  ( ( B = +oo /\ C = +oo ) -> ( B +e C ) = ( +oo +e +oo ) )
113 112 106 eqtrdi 
 |-  ( ( B = +oo /\ C = +oo ) -> ( B +e C ) = +oo )
114 113 oveq2d 
 |-  ( ( B = +oo /\ C = +oo ) -> ( A *e ( B +e C ) ) = ( A *e +oo ) )
115 114 adantll 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C = +oo ) -> ( A *e ( B +e C ) ) = ( A *e +oo ) )
116 109 111 115 3eqtr4rd 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C = +oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
117 pnfaddmnf 
 |-  ( +oo +e -oo ) = 0
118 31 55 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( ( A *e +oo ) +e ( A *e -oo ) ) = ( +oo +e -oo ) )
119 xmul01 
 |-  ( A e. RR* -> ( A *e 0 ) = 0 )
120 1 28 119 3syl 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( A *e 0 ) = 0 )
121 117 118 120 3eqtr4a 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( ( A *e +oo ) +e ( A *e -oo ) ) = ( A *e 0 ) )
122 121 ad2antrr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C = -oo ) -> ( ( A *e +oo ) +e ( A *e -oo ) ) = ( A *e 0 ) )
123 98 71 oveqan12d 
 |-  ( ( B = +oo /\ C = -oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e +oo ) +e ( A *e -oo ) ) )
124 123 adantll 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C = -oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e +oo ) +e ( A *e -oo ) ) )
125 oveq12 
 |-  ( ( B = +oo /\ C = -oo ) -> ( B +e C ) = ( +oo +e -oo ) )
126 125 117 eqtrdi 
 |-  ( ( B = +oo /\ C = -oo ) -> ( B +e C ) = 0 )
127 126 oveq2d 
 |-  ( ( B = +oo /\ C = -oo ) -> ( A *e ( B +e C ) ) = ( A *e 0 ) )
128 127 adantll 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C = -oo ) -> ( A *e ( B +e C ) ) = ( A *e 0 ) )
129 122 124 128 3eqtr4rd 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) /\ C = -oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
130 77 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) -> ( C e. RR \/ C = +oo \/ C = -oo ) )
131 102 116 129 130 mpjao3dan 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = +oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
132 55 ad2antrr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C e. RR ) -> ( A *e -oo ) = -oo )
133 1 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) -> A e. RR )
134 133 82 sylan 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C e. RR ) -> ( A *e C ) e. RR )
135 renepnf 
 |-  ( ( A *e C ) e. RR -> ( A *e C ) =/= +oo )
136 xaddmnf2 
 |-  ( ( ( A *e C ) e. RR* /\ ( A *e C ) =/= +oo ) -> ( -oo +e ( A *e C ) ) = -oo )
137 84 135 136 syl2anc 
 |-  ( ( A *e C ) e. RR -> ( -oo +e ( A *e C ) ) = -oo )
138 134 137 syl 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C e. RR ) -> ( -oo +e ( A *e C ) ) = -oo )
139 132 138 eqtr4d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C e. RR ) -> ( A *e -oo ) = ( -oo +e ( A *e C ) ) )
140 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) -> B = -oo )
141 140 oveq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) -> ( B +e C ) = ( -oo +e C ) )
142 renepnf 
 |-  ( C e. RR -> C =/= +oo )
143 xaddmnf2 
 |-  ( ( C e. RR* /\ C =/= +oo ) -> ( -oo +e C ) = -oo )
144 92 142 143 syl2anc 
 |-  ( C e. RR -> ( -oo +e C ) = -oo )
145 141 144 sylan9eq 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C e. RR ) -> ( B +e C ) = -oo )
146 145 oveq2d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C e. RR ) -> ( A *e ( B +e C ) ) = ( A *e -oo ) )
147 oveq2 
 |-  ( B = -oo -> ( A *e B ) = ( A *e -oo ) )
148 147 55 sylan9eqr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) -> ( A *e B ) = -oo )
149 148 adantr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C e. RR ) -> ( A *e B ) = -oo )
150 149 oveq1d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C e. RR ) -> ( ( A *e B ) +e ( A *e C ) ) = ( -oo +e ( A *e C ) ) )
151 139 146 150 3eqtr4d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C e. RR ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
152 55 31 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( ( A *e -oo ) +e ( A *e +oo ) ) = ( -oo +e +oo ) )
153 mnfaddpnf 
 |-  ( -oo +e +oo ) = 0
154 152 153 eqtrdi 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( ( A *e -oo ) +e ( A *e +oo ) ) = 0 )
155 120 154 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( A *e 0 ) = ( ( A *e -oo ) +e ( A *e +oo ) ) )
156 155 ad2antrr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C = +oo ) -> ( A *e 0 ) = ( ( A *e -oo ) +e ( A *e +oo ) ) )
157 oveq12 
 |-  ( ( B = -oo /\ C = +oo ) -> ( B +e C ) = ( -oo +e +oo ) )
158 157 153 eqtrdi 
 |-  ( ( B = -oo /\ C = +oo ) -> ( B +e C ) = 0 )
159 158 oveq2d 
 |-  ( ( B = -oo /\ C = +oo ) -> ( A *e ( B +e C ) ) = ( A *e 0 ) )
160 159 adantll 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C = +oo ) -> ( A *e ( B +e C ) ) = ( A *e 0 ) )
161 147 50 oveqan12d 
 |-  ( ( B = -oo /\ C = +oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e -oo ) +e ( A *e +oo ) ) )
162 161 adantll 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C = +oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e -oo ) +e ( A *e +oo ) ) )
163 156 160 162 3eqtr4d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C = +oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
164 mnfxr 
 |-  -oo e. RR*
165 mnfnepnf 
 |-  -oo =/= +oo
166 xaddmnf1 
 |-  ( ( -oo e. RR* /\ -oo =/= +oo ) -> ( -oo +e -oo ) = -oo )
167 164 165 166 mp2an 
 |-  ( -oo +e -oo ) = -oo
168 55 55 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( ( A *e -oo ) +e ( A *e -oo ) ) = ( -oo +e -oo ) )
169 167 168 55 3eqtr4a 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( ( A *e -oo ) +e ( A *e -oo ) ) = ( A *e -oo ) )
170 169 ad2antrr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C = -oo ) -> ( ( A *e -oo ) +e ( A *e -oo ) ) = ( A *e -oo ) )
171 147 71 oveqan12d 
 |-  ( ( B = -oo /\ C = -oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e -oo ) +e ( A *e -oo ) ) )
172 171 adantll 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C = -oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( ( A *e -oo ) +e ( A *e -oo ) ) )
173 oveq12 
 |-  ( ( B = -oo /\ C = -oo ) -> ( B +e C ) = ( -oo +e -oo ) )
174 173 167 eqtrdi 
 |-  ( ( B = -oo /\ C = -oo ) -> ( B +e C ) = -oo )
175 174 oveq2d 
 |-  ( ( B = -oo /\ C = -oo ) -> ( A *e ( B +e C ) ) = ( A *e -oo ) )
176 175 adantll 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C = -oo ) -> ( A *e ( B +e C ) ) = ( A *e -oo ) )
177 170 172 176 3eqtr4rd 
 |-  ( ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) /\ C = -oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
178 77 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) -> ( C e. RR \/ C = +oo \/ C = -oo ) )
179 151 163 177 178 mpjao3dan 
 |-  ( ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) /\ B = -oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
180 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> B e. RR* )
181 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
182 180 181 sylib 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( B e. RR \/ B = +oo \/ B = -oo ) )
183 79 131 179 182 mpjao3dan 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )