xmulasslem3

		Ref	Expression
	Assertion	xmulasslem3	$⊢ ((A \in ℝ^{} \land 0 < A) \land (B \in ℝ^{} \land 0 < B) \land (C \in ℝ^{*} \land 0 < C)) \to (A \cdot_{𝑒} B) \cdot_{𝑒} C = A \cdot_{𝑒} (B \cdot_{𝑒} C)$

Proof

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

Metamath Proof Explorer

Theorem xmulasslem3

Proof