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 ) )