Axiom ax-pre-mulext 7892

Description: Strong extensionality of multiplication (expressed in terms of <RR). Axiom for real and complex numbers, justified by Theorem axpre-mulext 7850

(Contributed by Jim Kingdon, 18-Feb-2020.)

Assertion

Ref	Expression
ax-pre-mulext	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )

Detailed syntax breakdown of Axiom ax-pre-mulext

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cr 7773	. . . 4 class RR
3	1, 2	wcel 2141	. . 3 wff A e. RR
4		cB	. . . 4 class B
5	4, 2	wcel 2141	. . 3 wff B e. RR
6		cC	. . . 4 class C
7	6, 2	wcel 2141	. . 3 wff C e. RR
8	3, 5, 7	w3a 973	. 2 wff ( A e. RR /\ B e. RR /\ C e. RR )
9		cmul 7779	. . . . 5 class x.
10	1, 6, 9	co 5853	. . . 4 class ( A x. C )
11	4, 6, 9	co 5853	. . . 4 class ( B x. C )
12		cltrr 7778	. . . 4 class <RR
13	10, 11, 12	wbr 3989	. . 3 wff ( A x. C ) <RR ( B x. C )
14	1, 4, 12	wbr 3989	. . . 4 wff A <RR B
15	4, 1, 12	wbr 3989	. . . 4 wff B <RR A
16	14, 15	wo 703	. . 3 wff ( A <RR B \/ B <RR A )
17	13, 16	wi 4	. 2 wff ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) )
18	8, 17	wi 4	1 wff ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )

This axiom is referenced by:  remulext1  8518