Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	rexmul2.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	rexmul2.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
	rexmul2.1	⊢ ( 𝜑 → 0 < 𝐶 )
	rexmul2.2	⊢ ( 𝜑 → 𝐴 = ( 𝐵 ·e 𝐶 ) )
Assertion	rexmul2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		rexmul2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		rexmul2.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		rexmul2.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4		rexmul2.1	⊢ ( 𝜑 → 0 < 𝐶 )
5		rexmul2.2	⊢ ( 𝜑 → 𝐴 = ( 𝐵 ·e 𝐶 ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → 𝐴 = ( 𝐵 ·e 𝐶 ) )
7		simpr	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → 𝐵 = +∞ )
8	7	oveq1d	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → ( 𝐵 ·e 𝐶 ) = ( +∞ ·e 𝐶 ) )
9		xmulpnf2	⊢ ( ( 𝐶 ∈ ℝ* ∧ 0 < 𝐶 ) → ( +∞ ·e 𝐶 ) = +∞ )
10	3 4 9	syl2anc	⊢ ( 𝜑 → ( +∞ ·e 𝐶 ) = +∞ )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → ( +∞ ·e 𝐶 ) = +∞ )
12	6 8 11	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → 𝐴 = +∞ )
13	1	renepnfd	⊢ ( 𝜑 → 𝐴 ≠ +∞ )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → 𝐴 ≠ +∞ )
15	14	neneqd	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → ¬ 𝐴 = +∞ )
16	12 15	pm2.65da	⊢ ( 𝜑 → ¬ 𝐵 = +∞ )
17	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = -∞ ) → 𝐴 = ( 𝐵 ·e 𝐶 ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝐵 = -∞ ) → 𝐵 = -∞ )
19	18	oveq1d	⊢ ( ( 𝜑 ∧ 𝐵 = -∞ ) → ( 𝐵 ·e 𝐶 ) = ( -∞ ·e 𝐶 ) )
20		xmulmnf2	⊢ ( ( 𝐶 ∈ ℝ* ∧ 0 < 𝐶 ) → ( -∞ ·e 𝐶 ) = -∞ )
21	3 4 20	syl2anc	⊢ ( 𝜑 → ( -∞ ·e 𝐶 ) = -∞ )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = -∞ ) → ( -∞ ·e 𝐶 ) = -∞ )
23	17 19 22	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = -∞ ) → 𝐴 = -∞ )
24	1	renemnfd	⊢ ( 𝜑 → 𝐴 ≠ -∞ )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = -∞ ) → 𝐴 ≠ -∞ )
26	25	neneqd	⊢ ( ( 𝜑 ∧ 𝐵 = -∞ ) → ¬ 𝐴 = -∞ )
27	23 26	pm2.65da	⊢ ( 𝜑 → ¬ 𝐵 = -∞ )
28		elxr	⊢ ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
29	2 28	sylib	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
30	16 27 29	ecase23d	⊢ ( 𝜑 → 𝐵 ∈ ℝ )