Metamath Proof Explorer

Theorem xmulasslem3

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

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

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 recn 
 |-  ( B e. RR -> B e. CC )
3 recn 
 |-  ( C e. RR -> C e. CC )
4 mulass 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
5 1 2 3 4 syl3an 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
6 5 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
7 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
8 rexmul 
 |-  ( ( ( A x. B ) e. RR /\ C e. RR ) -> ( ( A x. B ) *e C ) = ( ( A x. B ) x. C ) )
9 7 8 sylan 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A x. B ) *e C ) = ( ( A x. B ) x. C ) )
10 remulcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B x. C ) e. RR )
11 rexmul 
 |-  ( ( A e. RR /\ ( B x. C ) e. RR ) -> ( A *e ( B x. C ) ) = ( A x. ( B x. C ) ) )
12 10 11 sylan2 
 |-  ( ( A e. RR /\ ( B e. RR /\ C e. RR ) ) -> ( A *e ( B x. C ) ) = ( A x. ( B x. C ) ) )
13 12 anassrs 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A *e ( B x. C ) ) = ( A x. ( B x. C ) ) )
14 6 9 13 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A x. B ) *e C ) = ( A *e ( B x. C ) ) )
15 rexmul 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A *e B ) = ( A x. B ) )
16 15 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A *e B ) = ( A x. B ) )
17 16 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A *e B ) *e C ) = ( ( A x. B ) *e C ) )
18 rexmul 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B *e C ) = ( B x. C ) )
19 18 adantll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( B *e C ) = ( B x. C ) )
20 19 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A *e ( B *e C ) ) = ( A *e ( B x. C ) ) )
21 14 17 20 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
22 21 adantll 
 |-  ( ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ ( A e. RR /\ B e. RR ) ) /\ C e. RR ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
23 oveq2 
 |-  ( C = +oo -> ( ( A *e B ) *e C ) = ( ( A *e B ) *e +oo ) )
24 simp1l 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> A e. RR* )
25 simp2l 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> B e. RR* )
26 xmulcl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) e. RR* )
27 24 25 26 syl2anc 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( A *e B ) e. RR* )
28 xmulgt0 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> 0 < ( A *e B ) )
29 28 3adant3 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> 0 < ( A *e B ) )
30 xmulpnf1 
 |-  ( ( ( A *e B ) e. RR* /\ 0 < ( A *e B ) ) -> ( ( A *e B ) *e +oo ) = +oo )
31 27 29 30 syl2anc 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( ( A *e B ) *e +oo ) = +oo )
32 23 31 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ C = +oo ) -> ( ( A *e B ) *e C ) = +oo )
33 simpl1 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ C = +oo ) -> ( A e. RR* /\ 0 < A ) )
34 xmulpnf1 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo )
35 33 34 syl 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ C = +oo ) -> ( A *e +oo ) = +oo )
36 32 35 eqtr4d 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ C = +oo ) -> ( ( A *e B ) *e C ) = ( A *e +oo ) )
37 oveq2 
 |-  ( C = +oo -> ( B *e C ) = ( B *e +oo ) )
38 xmulpnf1 
 |-  ( ( B e. RR* /\ 0 < B ) -> ( B *e +oo ) = +oo )
39 38 3ad2ant2 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( B *e +oo ) = +oo )
40 37 39 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ C = +oo ) -> ( B *e C ) = +oo )
41 40 oveq2d 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ C = +oo ) -> ( A *e ( B *e C ) ) = ( A *e +oo ) )
42 36 41 eqtr4d 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ C = +oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
43 42 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ ( A e. RR /\ B e. RR ) ) /\ C = +oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
44 simpl3r 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ ( A e. RR /\ B e. RR ) ) -> 0 < C )
45 xmulasslem2 
 |-  ( ( 0 < C /\ C = -oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
46 44 45 sylan 
 |-  ( ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ ( A e. RR /\ B e. RR ) ) /\ C = -oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
47 simp3l 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> C e. RR* )
48 elxr 
 |-  ( C e. RR* <-> ( C e. RR \/ C = +oo \/ C = -oo ) )
49 47 48 sylib 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( C e. RR \/ C = +oo \/ C = -oo ) )
50 49 adantr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( C e. RR \/ C = +oo \/ C = -oo ) )
51 22 43 46 50 mpjao3dan 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
52 51 anassrs 
 |-  ( ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A e. RR ) /\ B e. RR ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
53 xmulpnf2 
 |-  ( ( C e. RR* /\ 0 < C ) -> ( +oo *e C ) = +oo )
54 53 3ad2ant3 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( +oo *e C ) = +oo )
55 34 3ad2ant1 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( A *e +oo ) = +oo )
56 54 55 eqtr4d 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( +oo *e C ) = ( A *e +oo ) )
57 56 adantr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ B = +oo ) -> ( +oo *e C ) = ( A *e +oo ) )
58 oveq2 
 |-  ( B = +oo -> ( A *e B ) = ( A *e +oo ) )
59 58 55 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ B = +oo ) -> ( A *e B ) = +oo )
60 59 oveq1d 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ B = +oo ) -> ( ( A *e B ) *e C ) = ( +oo *e C ) )
61 oveq1 
 |-  ( B = +oo -> ( B *e C ) = ( +oo *e C ) )
62 61 54 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ B = +oo ) -> ( B *e C ) = +oo )
63 62 oveq2d 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ B = +oo ) -> ( A *e ( B *e C ) ) = ( A *e +oo ) )
64 57 60 63 3eqtr4d 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ B = +oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
65 64 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A e. RR ) /\ B = +oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
66 simpl2r 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A e. RR ) -> 0 < B )
67 xmulasslem2 
 |-  ( ( 0 < B /\ B = -oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
68 66 67 sylan 
 |-  ( ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A e. RR ) /\ B = -oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
69 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
70 25 69 sylib 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( B e. RR \/ B = +oo \/ B = -oo ) )
71 70 adantr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A e. RR ) -> ( B e. RR \/ B = +oo \/ B = -oo ) )
72 52 65 68 71 mpjao3dan 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A e. RR ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
73 simpl3 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A = +oo ) -> ( C e. RR* /\ 0 < C ) )
74 73 53 syl 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A = +oo ) -> ( +oo *e C ) = +oo )
75 oveq1 
 |-  ( A = +oo -> ( A *e B ) = ( +oo *e B ) )
76 xmulpnf2 
 |-  ( ( B e. RR* /\ 0 < B ) -> ( +oo *e B ) = +oo )
77 76 3ad2ant2 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( +oo *e B ) = +oo )
78 75 77 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A = +oo ) -> ( A *e B ) = +oo )
79 78 oveq1d 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A = +oo ) -> ( ( A *e B ) *e C ) = ( +oo *e C ) )
80 oveq1 
 |-  ( A = +oo -> ( A *e ( B *e C ) ) = ( +oo *e ( B *e C ) ) )
81 xmulcl 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B *e C ) e. RR* )
82 25 47 81 syl2anc 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( B *e C ) e. RR* )
83 xmulgt0 
 |-  ( ( ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> 0 < ( B *e C ) )
84 83 3adant1 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> 0 < ( B *e C ) )
85 xmulpnf2 
 |-  ( ( ( B *e C ) e. RR* /\ 0 < ( B *e C ) ) -> ( +oo *e ( B *e C ) ) = +oo )
86 82 84 85 syl2anc 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( +oo *e ( B *e C ) ) = +oo )
87 80 86 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A = +oo ) -> ( A *e ( B *e C ) ) = +oo )
88 74 79 87 3eqtr4d 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A = +oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
89 simp1r 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> 0 < A )
90 xmulasslem2 
 |-  ( ( 0 < A /\ A = -oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
91 89 90 sylan 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) /\ A = -oo ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )
92 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
93 24 92 sylib 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( A e. RR \/ A = +oo \/ A = -oo ) )
94 72 88 91 93 mpjao3dan 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) /\ ( C e. RR* /\ 0 < C ) ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )