Metamath Proof Explorer

Theorem xmulcom

Description: Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 xmullem 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> A e. RR )
2 1 recnd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> A e. CC )
3 ancom 
 |-  ( ( A e. RR* /\ B e. RR* ) <-> ( B e. RR* /\ A e. RR* ) )
4 orcom 
 |-  ( ( A = 0 \/ B = 0 ) <-> ( B = 0 \/ A = 0 ) )
5 4 notbii 
 |-  ( -. ( A = 0 \/ B = 0 ) <-> -. ( B = 0 \/ A = 0 ) )
6 3 5 anbi12i 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) <-> ( ( B e. RR* /\ A e. RR* ) /\ -. ( B = 0 \/ A = 0 ) ) )
7 orcom 
 |-  ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) <-> ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) )
8 7 notbii 
 |-  ( -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) <-> -. ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) )
9 6 8 anbi12i 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) <-> ( ( ( B e. RR* /\ A e. RR* ) /\ -. ( B = 0 \/ A = 0 ) ) /\ -. ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) ) )
10 orcom 
 |-  ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) <-> ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) )
11 10 notbii 
 |-  ( -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) <-> -. ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) )
12 xmullem 
 |-  ( ( ( ( ( B e. RR* /\ A e. RR* ) /\ -. ( B = 0 \/ A = 0 ) ) /\ -. ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) ) /\ -. ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) ) -> B e. RR )
13 9 11 12 syl2anb 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> B e. RR )
14 13 recnd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> B e. CC )
15 2 14 mulcomd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> ( A x. B ) = ( B x. A ) )
16 15 ifeq2da 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -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 , ( B x. A ) ) )
17 10 a1i 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) <-> ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) ) )
18 17 ifbid 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( B x. A ) ) = if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) )
19 16 18 eqtrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) = if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) )
20 19 ifeq2da 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 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 ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) )
21 7 a1i 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) <-> ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) ) )
22 21 ifbid 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) = if ( ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) )
23 20 22 eqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 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 ( ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) )
24 23 ifeq2da 
 |-  ( ( 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 , if ( ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) ) )
25 4 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A = 0 \/ B = 0 ) <-> ( B = 0 \/ A = 0 ) ) )
26 25 ifbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) ) = if ( ( B = 0 \/ A = 0 ) , 0 , if ( ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) ) )
27 24 26 eqtrd 
 |-  ( ( 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 ( ( B = 0 \/ A = 0 ) , 0 , if ( ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) ) )
28 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 ) ) ) ) )
29 xmulval 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( B *e A ) = if ( ( B = 0 \/ A = 0 ) , 0 , if ( ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) ) )
30 29 ancoms 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( B *e A ) = if ( ( B = 0 \/ A = 0 ) , 0 , if ( ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) , +oo , if ( ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) , -oo , ( B x. A ) ) ) ) )
31 27 28 30 3eqtr4d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) = ( B *e A ) )