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 )

Metamath Proof Explorer

Theorem rexmul2

Proof