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	|- ( ph -> A e. RR )
	rexmul2.b	|- ( ph -> B e. RR* )
	rexmul2.c	|- ( ph -> C e. RR* )
	rexmul2.1	|- ( ph -> 0 < C )
	rexmul2.2	|- ( ph -> A = ( B *e C ) )
Assertion	rexmul2	|- ( ph -> B e. RR )

Proof

Step	Hyp	Ref	Expression
1		rexmul2.a	|- ( ph -> A e. RR )
2		rexmul2.b	|- ( ph -> B e. RR* )
3		rexmul2.c	|- ( ph -> C e. RR* )
4		rexmul2.1	|- ( ph -> 0 < C )
5		rexmul2.2	|- ( ph -> A = ( B *e C ) )
6	5	adantr	|- ( ( ph /\ B = +oo ) -> A = ( B *e C ) )
7		simpr	|- ( ( ph /\ B = +oo ) -> B = +oo )
8	7	oveq1d	|- ( ( ph /\ B = +oo ) -> ( B *e C ) = ( +oo *e C ) )
9		xmulpnf2	|- ( ( C e. RR* /\ 0 < C ) -> ( +oo *e C ) = +oo )
10	3 4 9	syl2anc	|- ( ph -> ( +oo *e C ) = +oo )
11	10	adantr	|- ( ( ph /\ B = +oo ) -> ( +oo *e C ) = +oo )
12	6 8 11	3eqtrd	|- ( ( ph /\ B = +oo ) -> A = +oo )
13	1	renepnfd	|- ( ph -> A =/= +oo )
14	13	adantr	|- ( ( ph /\ B = +oo ) -> A =/= +oo )
15	14	neneqd	|- ( ( ph /\ B = +oo ) -> -. A = +oo )
16	12 15	pm2.65da	|- ( ph -> -. B = +oo )
17	5	adantr	|- ( ( ph /\ B = -oo ) -> A = ( B *e C ) )
18		simpr	|- ( ( ph /\ B = -oo ) -> B = -oo )
19	18	oveq1d	|- ( ( ph /\ B = -oo ) -> ( B *e C ) = ( -oo *e C ) )
20		xmulmnf2	|- ( ( C e. RR* /\ 0 < C ) -> ( -oo *e C ) = -oo )
21	3 4 20	syl2anc	|- ( ph -> ( -oo *e C ) = -oo )
22	21	adantr	|- ( ( ph /\ B = -oo ) -> ( -oo *e C ) = -oo )
23	17 19 22	3eqtrd	|- ( ( ph /\ B = -oo ) -> A = -oo )
24	1	renemnfd	|- ( ph -> A =/= -oo )
25	24	adantr	|- ( ( ph /\ B = -oo ) -> A =/= -oo )
26	25	neneqd	|- ( ( ph /\ B = -oo ) -> -. A = -oo )
27	23 26	pm2.65da	|- ( ph -> -. B = -oo )
28		elxr	|- ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
29	2 28	sylib	|- ( ph -> ( B e. RR \/ B = +oo \/ B = -oo ) )
30	16 27 29	ecase23d	|- ( ph -> B e. RR )