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