rexmul2

Description: If the result A of an extended real multiplication is real, then its first factor B is also real. See also rexmul . (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	rexmul2.a	$⊢ φ \to A \in ℝ$
	rexmul2.b	$⊢ φ \to B \in ℝ^{*}$
	rexmul2.c	$⊢ φ \to C \in ℝ^{*}$
	rexmul2.1	$⊢ φ \to 0 < C$
	rexmul2.2	$⊢ φ \to A = B \cdot_{𝑒} C$
Assertion	rexmul2	$⊢ φ \to B \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		rexmul2.a	$⊢ φ \to A \in ℝ$
2		rexmul2.b	$⊢ φ \to B \in ℝ^{*}$
3		rexmul2.c	$⊢ φ \to C \in ℝ^{*}$
4		rexmul2.1	$⊢ φ \to 0 < C$
5		rexmul2.2	$⊢ φ \to A = B \cdot_{𝑒} C$
6	5	adantr	$⊢ (φ \land B = +∞) \to A = B \cdot_{𝑒} C$
7		simpr	$⊢ (φ \land B = +∞) \to B = +∞$
8	7	oveq1d	$⊢ (φ \land B = +∞) \to B \cdot_{𝑒} C = +∞ \cdot_{𝑒} C$
9		xmulpnf2	$⊢ (C \in ℝ^{*} \land 0 < C) \to +∞ \cdot_{𝑒} C = +∞$
10	3 4 9	syl2anc	$⊢ φ \to +∞ \cdot_{𝑒} C = +∞$
11	10	adantr	$⊢ (φ \land B = +∞) \to +∞ \cdot_{𝑒} C = +∞$
12	6 8 11	3eqtrd	$⊢ (φ \land B = +∞) \to A = +∞$
13	1	renepnfd	$⊢ φ \to A \neq +∞$
14	13	adantr	$⊢ (φ \land B = +∞) \to A \neq +∞$
15	14	neneqd	$⊢ (φ \land B = +∞) \to \neg A = +∞$
16	12 15	pm2.65da	$⊢ φ \to \neg B = +∞$
17	5	adantr	$⊢ (φ \land B = −∞) \to A = B \cdot_{𝑒} C$
18		simpr	$⊢ (φ \land B = −∞) \to B = −∞$
19	18	oveq1d	$⊢ (φ \land B = −∞) \to B \cdot_{𝑒} C = −∞ \cdot_{𝑒} C$
20		xmulmnf2	$⊢ (C \in ℝ^{*} \land 0 < C) \to −∞ \cdot_{𝑒} C = −∞$
21	3 4 20	syl2anc	$⊢ φ \to −∞ \cdot_{𝑒} C = −∞$
22	21	adantr	$⊢ (φ \land B = −∞) \to −∞ \cdot_{𝑒} C = −∞$
23	17 19 22	3eqtrd	$⊢ (φ \land B = −∞) \to A = −∞$
24	1	renemnfd	$⊢ φ \to A \neq −∞$
25	24	adantr	$⊢ (φ \land B = −∞) \to A \neq −∞$
26	25	neneqd	$⊢ (φ \land B = −∞) \to \neg A = −∞$
27	23 26	pm2.65da	$⊢ φ \to \neg B = −∞$
28		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
29	2 28	sylib	$⊢ φ \to (B \in ℝ \lor B = +∞ \lor B = −∞)$
30	16 27 29	ecase23d	$⊢ φ \to B \in ℝ$

Metamath Proof Explorer

Theorem rexmul2

Proof