This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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