Theorem xmulasslem3

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

	Ref	Expression
Assertion	xmulasslem3	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 < 𝐶 ) ) → ( ( 𝐴 ·e 𝐵 ) ·e 𝐶 ) = ( 𝐴 ·e ( 𝐵 ·e 𝐶 ) ) )

Proof

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