MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xadddilem Structured version   Unicode version

Theorem xadddilem 11498
Description: Lemma for xadddi 11499. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xadddilem  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )

Proof of Theorem xadddilem
StepHypRef Expression
1 simpl2 1000 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  B  e.  RR* )
2 elxr 11337 . . 3  |-  ( B  e.  RR*  <->  ( B  e.  RR  \/  B  = +oo  \/  B  = -oo ) )
31, 2sylib 196 . 2  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  ( B  e.  RR  \/  B  = +oo  \/  B  = -oo ) )
4 simpl3 1001 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  C  e.  RR* )
5 elxr 11337 . . . . . 6  |-  ( C  e.  RR*  <->  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )
64, 5sylib 196 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )
76adantr 465 . . . 4  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  e.  RR )  ->  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )
8 simpl1 999 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  A  e.  RR )
9 recn 9594 . . . . . . . . . 10  |-  ( A  e.  RR  ->  A  e.  CC )
10 recn 9594 . . . . . . . . . 10  |-  ( B  e.  RR  ->  B  e.  CC )
11 recn 9594 . . . . . . . . . 10  |-  ( C  e.  RR  ->  C  e.  CC )
12 adddi 9593 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
139, 10, 11, 12syl3an 1270 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
14133expa 1196 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A  x.  ( B  +  C
) )  =  ( ( A  x.  B
)  +  ( A  x.  C ) ) )
15 readdcl 9587 . . . . . . . . . 10  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( B  +  C
)  e.  RR )
16 rexmul 11475 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( B  +  C
)  e.  RR )  ->  ( A xe ( B  +  C ) )  =  ( A  x.  ( B  +  C )
) )
1715, 16sylan2 474 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( B  e.  RR  /\  C  e.  RR ) )  ->  ( A xe ( B  +  C ) )  =  ( A  x.  ( B  +  C
) ) )
1817anassrs 648 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A xe ( B  +  C ) )  =  ( A  x.  ( B  +  C )
) )
19 remulcl 9589 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
2019adantr 465 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A  x.  B )  e.  RR )
21 remulcl 9589 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( A  x.  C
)  e.  RR )
2221adantlr 714 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A  x.  C )  e.  RR )
23 rexadd 11443 . . . . . . . . 9  |-  ( ( ( A  x.  B
)  e.  RR  /\  ( A  x.  C
)  e.  RR )  ->  ( ( A  x.  B ) +e ( A  x.  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
2420, 22, 23syl2anc 661 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( ( A  x.  B ) +e ( A  x.  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
2514, 18, 243eqtr4d 2518 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A xe ( B  +  C ) )  =  ( ( A  x.  B ) +e
( A  x.  C
) ) )
26 rexadd 11443 . . . . . . . . 9  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( B +e
C )  =  ( B  +  C ) )
2726adantll 713 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( B +e C )  =  ( B  +  C
) )
2827oveq2d 6311 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A xe ( B +e C ) )  =  ( A xe ( B  +  C ) ) )
29 rexmul 11475 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A xe B )  =  ( A  x.  B ) )
3029adantr 465 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A xe B )  =  ( A  x.  B
) )
31 rexmul 11475 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( A xe C )  =  ( A  x.  C ) )
3231adantlr 714 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A xe C )  =  ( A  x.  C
) )
3330, 32oveq12d 6313 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( ( A xe B ) +e ( A xe C ) )  =  ( ( A  x.  B ) +e ( A  x.  C ) ) )
3425, 28, 333eqtr4d 2518 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
358, 34sylanl1 650 . . . . 5  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  e.  RR )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
36 rexr 9651 . . . . . . . . . . 11  |-  ( A  e.  RR  ->  A  e.  RR* )
37363ad2ant1 1017 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  ->  A  e.  RR* )
38 xmulpnf1 11478 . . . . . . . . . 10  |-  ( ( A  e.  RR*  /\  0  <  A )  ->  ( A xe +oo )  = +oo )
3937, 38sylan 471 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  ( A xe +oo )  = +oo )
4039adantr 465 . . . . . . . 8  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  e.  RR )  ->  ( A xe +oo )  = +oo )
4129, 19eqeltrd 2555 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A xe B )  e.  RR )
428, 41sylan 471 . . . . . . . . 9  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  e.  RR )  ->  ( A xe B )  e.  RR )
43 rexr 9651 . . . . . . . . . 10  |-  ( ( A xe B )  e.  RR  ->  ( A xe B )  e.  RR* )
44 renemnf 9654 . . . . . . . . . 10  |-  ( ( A xe B )  e.  RR  ->  ( A xe B )  =/= -oo )
45 xaddpnf1 11437 . . . . . . . . . 10  |-  ( ( ( A xe B )  e.  RR*  /\  ( A xe B )  =/= -oo )  ->  ( ( A xe B ) +e +oo )  = +oo )
4643, 44, 45syl2anc 661 . . . . . . . . 9  |-  ( ( A xe B )  e.  RR  ->  ( ( A xe B ) +e +oo )  = +oo )
4742, 46syl 16 . . . . . . . 8  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  e.  RR )  ->  (
( A xe B ) +e +oo )  = +oo )
4840, 47eqtr4d 2511 . . . . . . 7  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  e.  RR )  ->  ( A xe +oo )  =  ( ( A xe B ) +e +oo )
)
4948adantr 465 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = +oo )  ->  ( A xe +oo )  =  ( ( A xe B ) +e +oo )
)
50 oveq2 6303 . . . . . . . 8  |-  ( C  = +oo  ->  ( B +e C )  =  ( B +e +oo ) )
51 rexr 9651 . . . . . . . . . 10  |-  ( B  e.  RR  ->  B  e.  RR* )
52 renemnf 9654 . . . . . . . . . 10  |-  ( B  e.  RR  ->  B  =/= -oo )
53 xaddpnf1 11437 . . . . . . . . . 10  |-  ( ( B  e.  RR*  /\  B  =/= -oo )  ->  ( B +e +oo )  = +oo )
5451, 52, 53syl2anc 661 . . . . . . . . 9  |-  ( B  e.  RR  ->  ( B +e +oo )  = +oo )
5554adantl 466 . . . . . . . 8  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  e.  RR )  ->  ( B +e +oo )  = +oo )
5650, 55sylan9eqr 2530 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = +oo )  ->  ( B +e C )  = +oo )
5756oveq2d 6311 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = +oo )  ->  ( A xe ( B +e C ) )  =  ( A xe +oo )
)
58 oveq2 6303 . . . . . . . 8  |-  ( C  = +oo  ->  ( A xe C )  =  ( A xe +oo ) )
5958, 40sylan9eqr 2530 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = +oo )  ->  ( A xe C )  = +oo )
6059oveq2d 6311 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = +oo )  ->  (
( A xe B ) +e
( A xe C ) )  =  ( ( A xe B ) +e +oo ) )
6149, 57, 603eqtr4d 2518 . . . . 5  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = +oo )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
62 xmulmnf1 11480 . . . . . . . . . 10  |-  ( ( A  e.  RR*  /\  0  <  A )  ->  ( A xe -oo )  = -oo )
6337, 62sylan 471 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  ( A xe -oo )  = -oo )
6463adantr 465 . . . . . . . 8  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  e.  RR )  ->  ( A xe -oo )  = -oo )
6564adantr 465 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = -oo )  ->  ( A xe -oo )  = -oo )
6642adantr 465 . . . . . . . 8  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = -oo )  ->  ( A xe B )  e.  RR )
67 renepnf 9653 . . . . . . . . 9  |-  ( ( A xe B )  e.  RR  ->  ( A xe B )  =/= +oo )
68 xaddmnf1 11439 . . . . . . . . 9  |-  ( ( ( A xe B )  e.  RR*  /\  ( A xe B )  =/= +oo )  ->  ( ( A xe B ) +e -oo )  = -oo )
6943, 67, 68syl2anc 661 . . . . . . . 8  |-  ( ( A xe B )  e.  RR  ->  ( ( A xe B ) +e -oo )  = -oo )
7066, 69syl 16 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = -oo )  ->  (
( A xe B ) +e -oo )  = -oo )
7165, 70eqtr4d 2511 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = -oo )  ->  ( A xe -oo )  =  ( ( A xe B ) +e -oo )
)
72 oveq2 6303 . . . . . . . 8  |-  ( C  = -oo  ->  ( B +e C )  =  ( B +e -oo ) )
73 renepnf 9653 . . . . . . . . . 10  |-  ( B  e.  RR  ->  B  =/= +oo )
74 xaddmnf1 11439 . . . . . . . . . 10  |-  ( ( B  e.  RR*  /\  B  =/= +oo )  ->  ( B +e -oo )  = -oo )
7551, 73, 74syl2anc 661 . . . . . . . . 9  |-  ( B  e.  RR  ->  ( B +e -oo )  = -oo )
7675adantl 466 . . . . . . . 8  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  e.  RR )  ->  ( B +e -oo )  = -oo )
7772, 76sylan9eqr 2530 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = -oo )  ->  ( B +e C )  = -oo )
7877oveq2d 6311 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = -oo )  ->  ( A xe ( B +e C ) )  =  ( A xe -oo )
)
79 oveq2 6303 . . . . . . . 8  |-  ( C  = -oo  ->  ( A xe C )  =  ( A xe -oo ) )
8079, 64sylan9eqr 2530 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = -oo )  ->  ( A xe C )  = -oo )
8180oveq2d 6311 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = -oo )  ->  (
( A xe B ) +e
( A xe C ) )  =  ( ( A xe B ) +e -oo ) )
8271, 78, 813eqtr4d 2518 . . . . 5  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  C  = -oo )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
8335, 61, 823jaodan 1294 . . . 4  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  e.  RR )  /\  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )  -> 
( A xe ( B +e
C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
847, 83mpdan 668 . . 3  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  e.  RR )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
856adantr 465 . . . 4  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = +oo )  ->  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )
8639ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  e.  RR )  ->  ( A xe +oo )  = +oo )
878adantr 465 . . . . . . . . 9  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = +oo )  ->  A  e.  RR )
8831, 21eqeltrd 2555 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( A xe C )  e.  RR )
8987, 88sylan 471 . . . . . . . 8  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  e.  RR )  ->  ( A xe C )  e.  RR )
90 rexr 9651 . . . . . . . . 9  |-  ( ( A xe C )  e.  RR  ->  ( A xe C )  e.  RR* )
91 renemnf 9654 . . . . . . . . 9  |-  ( ( A xe C )  e.  RR  ->  ( A xe C )  =/= -oo )
92 xaddpnf2 11438 . . . . . . . . 9  |-  ( ( ( A xe C )  e.  RR*  /\  ( A xe C )  =/= -oo )  ->  ( +oo +e ( A xe C ) )  = +oo )
9390, 91, 92syl2anc 661 . . . . . . . 8  |-  ( ( A xe C )  e.  RR  ->  ( +oo +e ( A xe C ) )  = +oo )
9489, 93syl 16 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  e.  RR )  ->  ( +oo +e ( A xe C ) )  = +oo )
9586, 94eqtr4d 2511 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  e.  RR )  ->  ( A xe +oo )  =  ( +oo +e
( A xe C ) ) )
96 simpr 461 . . . . . . . . 9  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = +oo )  ->  B  = +oo )
9796oveq1d 6310 . . . . . . . 8  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = +oo )  ->  ( B +e C )  =  ( +oo +e C ) )
98 rexr 9651 . . . . . . . . 9  |-  ( C  e.  RR  ->  C  e.  RR* )
99 renemnf 9654 . . . . . . . . 9  |-  ( C  e.  RR  ->  C  =/= -oo )
100 xaddpnf2 11438 . . . . . . . . 9  |-  ( ( C  e.  RR*  /\  C  =/= -oo )  ->  ( +oo +e C )  = +oo )
10198, 99, 100syl2anc 661 . . . . . . . 8  |-  ( C  e.  RR  ->  ( +oo +e C )  = +oo )
10297, 101sylan9eq 2528 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  e.  RR )  ->  ( B +e C )  = +oo )
103102oveq2d 6311 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  e.  RR )  ->  ( A xe ( B +e C ) )  =  ( A xe +oo )
)
104 oveq2 6303 . . . . . . . . 9  |-  ( B  = +oo  ->  ( A xe B )  =  ( A xe +oo ) )
105104, 39sylan9eqr 2530 . . . . . . . 8  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = +oo )  ->  ( A xe B )  = +oo )
106105adantr 465 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  e.  RR )  ->  ( A xe B )  = +oo )
107106oveq1d 6310 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  e.  RR )  ->  (
( A xe B ) +e
( A xe C ) )  =  ( +oo +e
( A xe C ) ) )
10895, 103, 1073eqtr4d 2518 . . . . 5  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  e.  RR )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
109 pnfxr 11333 . . . . . . . . 9  |- +oo  e.  RR*
110 pnfnemnf 11338 . . . . . . . . 9  |- +oo  =/= -oo
111 xaddpnf1 11437 . . . . . . . . 9  |-  ( ( +oo  e.  RR*  /\ +oo  =/= -oo )  ->  ( +oo +e +oo )  = +oo )
112109, 110, 111mp2an 672 . . . . . . . 8  |-  ( +oo +e +oo )  = +oo
11339, 39oveq12d 6313 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  (
( A xe +oo ) +e
( A xe +oo ) )  =  ( +oo +e +oo ) )
114112, 113, 393eqtr4a 2534 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  (
( A xe +oo ) +e
( A xe +oo ) )  =  ( A xe +oo ) )
115114ad2antrr 725 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  = +oo )  ->  (
( A xe +oo ) +e
( A xe +oo ) )  =  ( A xe +oo ) )
116104, 58oveqan12d 6314 . . . . . . 7  |-  ( ( B  = +oo  /\  C  = +oo )  ->  ( ( A xe B ) +e ( A xe C ) )  =  ( ( A xe +oo ) +e ( A xe +oo )
) )
117116adantll 713 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  = +oo )  ->  (
( A xe B ) +e
( A xe C ) )  =  ( ( A xe +oo ) +e ( A xe +oo ) ) )
118 oveq12 6304 . . . . . . . . 9  |-  ( ( B  = +oo  /\  C  = +oo )  ->  ( B +e
C )  =  ( +oo +e +oo ) )
119118, 112syl6eq 2524 . . . . . . . 8  |-  ( ( B  = +oo  /\  C  = +oo )  ->  ( B +e
C )  = +oo )
120119oveq2d 6311 . . . . . . 7  |-  ( ( B  = +oo  /\  C  = +oo )  ->  ( A xe ( B +e
C ) )  =  ( A xe +oo ) )
121120adantll 713 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  = +oo )  ->  ( A xe ( B +e C ) )  =  ( A xe +oo )
)
122115, 117, 1213eqtr4rd 2519 . . . . 5  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  = +oo )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
123 pnfaddmnf 11441 . . . . . . . 8  |-  ( +oo +e -oo )  =  0
12439, 63oveq12d 6313 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  (
( A xe +oo ) +e
( A xe -oo ) )  =  ( +oo +e -oo ) )
125 xmul01 11471 . . . . . . . . 9  |-  ( A  e.  RR*  ->  ( A xe 0 )  =  0 )
1268, 36, 1253syl 20 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  ( A xe 0 )  =  0 )
127123, 124, 1263eqtr4a 2534 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  (
( A xe +oo ) +e
( A xe -oo ) )  =  ( A xe 0 ) )
128127ad2antrr 725 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  = -oo )  ->  (
( A xe +oo ) +e
( A xe -oo ) )  =  ( A xe 0 ) )
129104, 79oveqan12d 6314 . . . . . . 7  |-  ( ( B  = +oo  /\  C  = -oo )  ->  ( ( A xe B ) +e ( A xe C ) )  =  ( ( A xe +oo ) +e ( A xe -oo )
) )
130129adantll 713 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  = -oo )  ->  (
( A xe B ) +e
( A xe C ) )  =  ( ( A xe +oo ) +e ( A xe -oo ) ) )
131 oveq12 6304 . . . . . . . . 9  |-  ( ( B  = +oo  /\  C  = -oo )  ->  ( B +e
C )  =  ( +oo +e -oo ) )
132131, 123syl6eq 2524 . . . . . . . 8  |-  ( ( B  = +oo  /\  C  = -oo )  ->  ( B +e
C )  =  0 )
133132oveq2d 6311 . . . . . . 7  |-  ( ( B  = +oo  /\  C  = -oo )  ->  ( A xe ( B +e
C ) )  =  ( A xe 0 ) )
134133adantll 713 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  = -oo )  ->  ( A xe ( B +e C ) )  =  ( A xe 0 ) )
135128, 130, 1343eqtr4rd 2519 . . . . 5  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  C  = -oo )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
136108, 122, 1353jaodan 1294 . . . 4  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = +oo )  /\  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )  -> 
( A xe ( B +e
C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
13785, 136mpdan 668 . . 3  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = +oo )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
1386adantr 465 . . . 4  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = -oo )  ->  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )
13963ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  e.  RR )  ->  ( A xe -oo )  = -oo )
1408adantr 465 . . . . . . . . 9  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = -oo )  ->  A  e.  RR )
141140, 88sylan 471 . . . . . . . 8  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  e.  RR )  ->  ( A xe C )  e.  RR )
142 renepnf 9653 . . . . . . . . 9  |-  ( ( A xe C )  e.  RR  ->  ( A xe C )  =/= +oo )
143 xaddmnf2 11440 . . . . . . . . 9  |-  ( ( ( A xe C )  e.  RR*  /\  ( A xe C )  =/= +oo )  ->  ( -oo +e ( A xe C ) )  = -oo )
14490, 142, 143syl2anc 661 . . . . . . . 8  |-  ( ( A xe C )  e.  RR  ->  ( -oo +e ( A xe C ) )  = -oo )
145141, 144syl 16 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  e.  RR )  ->  ( -oo +e ( A xe C ) )  = -oo )
146139, 145eqtr4d 2511 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  e.  RR )  ->  ( A xe -oo )  =  ( -oo +e
( A xe C ) ) )
147 simpr 461 . . . . . . . . 9  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = -oo )  ->  B  = -oo )
148147oveq1d 6310 . . . . . . . 8  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = -oo )  ->  ( B +e C )  =  ( -oo +e C ) )
149 renepnf 9653 . . . . . . . . 9  |-  ( C  e.  RR  ->  C  =/= +oo )
150 xaddmnf2 11440 . . . . . . . . 9  |-  ( ( C  e.  RR*  /\  C  =/= +oo )  ->  ( -oo +e C )  = -oo )
15198, 149, 150syl2anc 661 . . . . . . . 8  |-  ( C  e.  RR  ->  ( -oo +e C )  = -oo )
152148, 151sylan9eq 2528 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  e.  RR )  ->  ( B +e C )  = -oo )
153152oveq2d 6311 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  e.  RR )  ->  ( A xe ( B +e C ) )  =  ( A xe -oo )
)
154 oveq2 6303 . . . . . . . . 9  |-  ( B  = -oo  ->  ( A xe B )  =  ( A xe -oo ) )
155154, 63sylan9eqr 2530 . . . . . . . 8  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = -oo )  ->  ( A xe B )  = -oo )
156155adantr 465 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  e.  RR )  ->  ( A xe B )  = -oo )
157156oveq1d 6310 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  e.  RR )  ->  (
( A xe B ) +e
( A xe C ) )  =  ( -oo +e
( A xe C ) ) )
158146, 153, 1573eqtr4d 2518 . . . . 5  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  e.  RR )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
15963, 39oveq12d 6313 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  (
( A xe -oo ) +e
( A xe +oo ) )  =  ( -oo +e +oo ) )
160 mnfaddpnf 11442 . . . . . . . . 9  |-  ( -oo +e +oo )  =  0
161159, 160syl6eq 2524 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  (
( A xe -oo ) +e
( A xe +oo ) )  =  0 )
162126, 161eqtr4d 2511 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  ( A xe 0 )  =  ( ( A xe -oo ) +e ( A xe +oo )
) )
163162ad2antrr 725 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  = +oo )  ->  ( A xe 0 )  =  ( ( A xe -oo ) +e ( A xe +oo )
) )
164 oveq12 6304 . . . . . . . . 9  |-  ( ( B  = -oo  /\  C  = +oo )  ->  ( B +e
C )  =  ( -oo +e +oo ) )
165164, 160syl6eq 2524 . . . . . . . 8  |-  ( ( B  = -oo  /\  C  = +oo )  ->  ( B +e
C )  =  0 )
166165oveq2d 6311 . . . . . . 7  |-  ( ( B  = -oo  /\  C  = +oo )  ->  ( A xe ( B +e
C ) )  =  ( A xe 0 ) )
167166adantll 713 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  = +oo )  ->  ( A xe ( B +e C ) )  =  ( A xe 0 ) )
168154, 58oveqan12d 6314 . . . . . . 7  |-  ( ( B  = -oo  /\  C  = +oo )  ->  ( ( A xe B ) +e ( A xe C ) )  =  ( ( A xe -oo ) +e ( A xe +oo )
) )
169168adantll 713 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  = +oo )  ->  (
( A xe B ) +e
( A xe C ) )  =  ( ( A xe -oo ) +e ( A xe +oo ) ) )
170163, 167, 1693eqtr4d 2518 . . . . 5  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  = +oo )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
171 mnfxr 11335 . . . . . . . . 9  |- -oo  e.  RR*
172 mnfnepnf 11339 . . . . . . . . 9  |- -oo  =/= +oo
173 xaddmnf1 11439 . . . . . . . . 9  |-  ( ( -oo  e.  RR*  /\ -oo  =/= +oo )  ->  ( -oo +e -oo )  = -oo )
174171, 172, 173mp2an 672 . . . . . . . 8  |-  ( -oo +e -oo )  = -oo
17563, 63oveq12d 6313 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  (
( A xe -oo ) +e
( A xe -oo ) )  =  ( -oo +e -oo ) )
176174, 175, 633eqtr4a 2534 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  (
( A xe -oo ) +e
( A xe -oo ) )  =  ( A xe -oo ) )
177176ad2antrr 725 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  = -oo )  ->  (
( A xe -oo ) +e
( A xe -oo ) )  =  ( A xe -oo ) )
178154, 79oveqan12d 6314 . . . . . . 7  |-  ( ( B  = -oo  /\  C  = -oo )  ->  ( ( A xe B ) +e ( A xe C ) )  =  ( ( A xe -oo ) +e ( A xe -oo )
) )
179178adantll 713 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  = -oo )  ->  (
( A xe B ) +e
( A xe C ) )  =  ( ( A xe -oo ) +e ( A xe -oo ) ) )
180 oveq12 6304 . . . . . . . . 9  |-  ( ( B  = -oo  /\  C  = -oo )  ->  ( B +e
C )  =  ( -oo +e -oo ) )
181180, 174syl6eq 2524 . . . . . . . 8  |-  ( ( B  = -oo  /\  C  = -oo )  ->  ( B +e
C )  = -oo )
182181oveq2d 6311 . . . . . . 7  |-  ( ( B  = -oo  /\  C  = -oo )  ->  ( A xe ( B +e
C ) )  =  ( A xe -oo ) )
183182adantll 713 . . . . . 6  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  = -oo )  ->  ( A xe ( B +e C ) )  =  ( A xe -oo )
)
184177, 179, 1833eqtr4rd 2519 . . . . 5  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  C  = -oo )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
185158, 170, 1843jaodan 1294 . . . 4  |-  ( ( ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e. 
RR* )  /\  0  <  A )  /\  B  = -oo )  /\  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )  -> 
( A xe ( B +e
C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
186138, 185mpdan 668 . . 3  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  B  = -oo )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
18784, 137, 1863jaodan 1294 . 2  |-  ( ( ( ( A  e.  RR  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  0  < 
A )  /\  ( B  e.  RR  \/  B  = +oo  \/  B  = -oo ) )  -> 
( A xe ( B +e
C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
1883, 187mpdan 668 1  |-  ( ( ( A  e.  RR  /\  B  e.  RR*  /\  C  e.  RR* )  /\  0  <  A )  ->  ( A xe ( B +e C ) )  =  ( ( A xe B ) +e ( A xe C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    \/ w3o 972    /\ w3a 973    = wceq 1379    e. wcel 1767    =/= wne 2662   class class class wbr 4453  (class class class)co 6295   CCcc 9502   RRcr 9503   0cc0 9504    + caddc 9507    x. cmul 9509   +oocpnf 9637   -oocmnf 9638   RR*cxr 9639    < clt 9640   +ecxad 11328   xecxmu 11329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-po 4806  df-so 4807  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-er 7323  df-en 7529  df-dom 7530  df-sdom 7531  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-xneg 11330  df-xadd 11331  df-xmul 11332
This theorem is referenced by:  xadddi  11499
  Copyright terms: Public domain W3C validator