Metamath Proof Explorer


Theorem rexmul

Description: The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion rexmul
|- ( ( A e. RR /\ B e. RR ) -> ( A *e B ) = ( A x. B ) )

Proof

Step Hyp Ref Expression
1 renepnf
 |-  ( A e. RR -> A =/= +oo )
2 1 adantr
 |-  ( ( A e. RR /\ B e. RR ) -> A =/= +oo )
3 2 necon2bi
 |-  ( A = +oo -> -. ( A e. RR /\ B e. RR ) )
4 3 adantl
 |-  ( ( 0 < B /\ A = +oo ) -> -. ( A e. RR /\ B e. RR ) )
5 renemnf
 |-  ( A e. RR -> A =/= -oo )
6 5 adantr
 |-  ( ( A e. RR /\ B e. RR ) -> A =/= -oo )
7 6 necon2bi
 |-  ( A = -oo -> -. ( A e. RR /\ B e. RR ) )
8 7 adantl
 |-  ( ( B < 0 /\ A = -oo ) -> -. ( A e. RR /\ B e. RR ) )
9 4 8 jaoi
 |-  ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) -> -. ( A e. RR /\ B e. RR ) )
10 renepnf
 |-  ( B e. RR -> B =/= +oo )
11 10 adantl
 |-  ( ( A e. RR /\ B e. RR ) -> B =/= +oo )
12 11 necon2bi
 |-  ( B = +oo -> -. ( A e. RR /\ B e. RR ) )
13 12 adantl
 |-  ( ( 0 < A /\ B = +oo ) -> -. ( A e. RR /\ B e. RR ) )
14 renemnf
 |-  ( B e. RR -> B =/= -oo )
15 14 adantl
 |-  ( ( A e. RR /\ B e. RR ) -> B =/= -oo )
16 15 necon2bi
 |-  ( B = -oo -> -. ( A e. RR /\ B e. RR ) )
17 16 adantl
 |-  ( ( A < 0 /\ B = -oo ) -> -. ( A e. RR /\ B e. RR ) )
18 13 17 jaoi
 |-  ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) -> -. ( A e. RR /\ B e. RR ) )
19 9 18 jaoi
 |-  ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( A e. RR /\ B e. RR ) )
20 19 con2i
 |-  ( ( A e. RR /\ B e. RR ) -> -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) )
21 20 iffalsed
 |-  ( ( A e. RR /\ B e. RR ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) )
22 7 adantl
 |-  ( ( 0 < B /\ A = -oo ) -> -. ( A e. RR /\ B e. RR ) )
23 3 adantl
 |-  ( ( B < 0 /\ A = +oo ) -> -. ( A e. RR /\ B e. RR ) )
24 22 23 jaoi
 |-  ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) -> -. ( A e. RR /\ B e. RR ) )
25 16 adantl
 |-  ( ( 0 < A /\ B = -oo ) -> -. ( A e. RR /\ B e. RR ) )
26 12 adantl
 |-  ( ( A < 0 /\ B = +oo ) -> -. ( A e. RR /\ B e. RR ) )
27 25 26 jaoi
 |-  ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) -> -. ( A e. RR /\ B e. RR ) )
28 24 27 jaoi
 |-  ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) -> -. ( A e. RR /\ B e. RR ) )
29 28 con2i
 |-  ( ( A e. RR /\ B e. RR ) -> -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) )
30 29 iffalsed
 |-  ( ( A e. RR /\ B e. RR ) -> if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) = ( A x. B ) )
31 21 30 eqtrd
 |-  ( ( A e. RR /\ B e. RR ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = ( A x. B ) )
32 31 ifeq2d
 |-  ( ( A e. RR /\ B e. RR ) -> if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) = if ( ( A = 0 \/ B = 0 ) , 0 , ( A x. B ) ) )
33 rexr
 |-  ( A e. RR -> A e. RR* )
34 rexr
 |-  ( B e. RR -> B e. RR* )
35 xmulval
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )
36 33 34 35 syl2an
 |-  ( ( A e. RR /\ B e. RR ) -> ( A *e B ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )
37 ifid
 |-  if ( ( A = 0 \/ B = 0 ) , ( A x. B ) , ( A x. B ) ) = ( A x. B )
38 oveq1
 |-  ( A = 0 -> ( A x. B ) = ( 0 x. B ) )
39 mul02lem2
 |-  ( B e. RR -> ( 0 x. B ) = 0 )
40 39 adantl
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 x. B ) = 0 )
41 38 40 sylan9eqr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A = 0 ) -> ( A x. B ) = 0 )
42 oveq2
 |-  ( B = 0 -> ( A x. B ) = ( A x. 0 ) )
43 recn
 |-  ( A e. RR -> A e. CC )
44 43 mul01d
 |-  ( A e. RR -> ( A x. 0 ) = 0 )
45 44 adantr
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. 0 ) = 0 )
46 42 45 sylan9eqr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B = 0 ) -> ( A x. B ) = 0 )
47 41 46 jaodan
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A = 0 \/ B = 0 ) ) -> ( A x. B ) = 0 )
48 47 ifeq1da
 |-  ( ( A e. RR /\ B e. RR ) -> if ( ( A = 0 \/ B = 0 ) , ( A x. B ) , ( A x. B ) ) = if ( ( A = 0 \/ B = 0 ) , 0 , ( A x. B ) ) )
49 37 48 eqtr3id
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) = if ( ( A = 0 \/ B = 0 ) , 0 , ( A x. B ) ) )
50 32 36 49 3eqtr4d
 |-  ( ( A e. RR /\ B e. RR ) -> ( A *e B ) = ( A x. B ) )