Theorem muls0ord

Description: If a surreal product is zero, one of its factors must be zero. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Hypotheses	muls0ord.1	$$⊢\phi \to A\in \mathrm{No}$$
	muls0ord.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	muls0ord	Could not format assertion : No typesetting found for |- ( ph -> ( ( A x.s B ) = 0s <-> ( A = 0s \/ B = 0s ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		muls0ord.1	$$⊢\phi \to A\in \mathrm{No}$$
2		muls0ord.2	$$⊢\phi \to B\in \mathrm{No}$$
3		muls02	Could not format ( B e. No -> ( 0s x.s B ) = 0s ) : No typesetting found for |- ( B e. No -> ( 0s x.s B ) = 0s ) with typecode |-
4	2 3	syl	Could not format ( ph -> ( 0s x.s B ) = 0s ) : No typesetting found for |- ( ph -> ( 0s x.s B ) = 0s ) with typecode |-
5	4	adantr	Could not format ( ( ph /\ B =/= 0s ) -> ( 0s x.s B ) = 0s ) : No typesetting found for |- ( ( ph /\ B =/= 0s ) -> ( 0s x.s B ) = 0s ) with typecode |-
6	5	eqeq2d	Could not format ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = ( 0s x.s B ) <-> ( A x.s B ) = 0s ) ) : No typesetting found for |- ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = ( 0s x.s B ) <-> ( A x.s B ) = 0s ) ) with typecode |-
7	1	adantr	Could not format ( ( ph /\ B =/= 0s ) -> A e. No ) : No typesetting found for |- ( ( ph /\ B =/= 0s ) -> A e. No ) with typecode |-
8		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
9	8	a1i	Could not format ( ( ph /\ B =/= 0s ) -> 0s e. No ) : No typesetting found for |- ( ( ph /\ B =/= 0s ) -> 0s e. No ) with typecode |-
10	2	adantr	Could not format ( ( ph /\ B =/= 0s ) -> B e. No ) : No typesetting found for |- ( ( ph /\ B =/= 0s ) -> B e. No ) with typecode |-
11		simpr	Could not format ( ( ph /\ B =/= 0s ) -> B =/= 0s ) : No typesetting found for |- ( ( ph /\ B =/= 0s ) -> B =/= 0s ) with typecode |-
12	7 9 10 11	mulscan2d	Could not format ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = ( 0s x.s B ) <-> A = 0s ) ) : No typesetting found for |- ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = ( 0s x.s B ) <-> A = 0s ) ) with typecode |-
13	6 12	bitr3d	Could not format ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = 0s <-> A = 0s ) ) : No typesetting found for |- ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = 0s <-> A = 0s ) ) with typecode |-
14	13	biimpd	Could not format ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = 0s -> A = 0s ) ) : No typesetting found for |- ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = 0s -> A = 0s ) ) with typecode |-
15	14	impancom	Could not format ( ( ph /\ ( A x.s B ) = 0s ) -> ( B =/= 0s -> A = 0s ) ) : No typesetting found for |- ( ( ph /\ ( A x.s B ) = 0s ) -> ( B =/= 0s -> A = 0s ) ) with typecode |-
16	15	necon1bd	Could not format ( ( ph /\ ( A x.s B ) = 0s ) -> ( -. A = 0s -> B = 0s ) ) : No typesetting found for |- ( ( ph /\ ( A x.s B ) = 0s ) -> ( -. A = 0s -> B = 0s ) ) with typecode |-
17	16	orrd	Could not format ( ( ph /\ ( A x.s B ) = 0s ) -> ( A = 0s \/ B = 0s ) ) : No typesetting found for |- ( ( ph /\ ( A x.s B ) = 0s ) -> ( A = 0s \/ B = 0s ) ) with typecode |-
18	17	ex	Could not format ( ph -> ( ( A x.s B ) = 0s -> ( A = 0s \/ B = 0s ) ) ) : No typesetting found for |- ( ph -> ( ( A x.s B ) = 0s -> ( A = 0s \/ B = 0s ) ) ) with typecode |-
19		oveq1	Could not format ( A = 0s -> ( A x.s B ) = ( 0s x.s B ) ) : No typesetting found for |- ( A = 0s -> ( A x.s B ) = ( 0s x.s B ) ) with typecode |-
20	19	eqeq1d	Could not format ( A = 0s -> ( ( A x.s B ) = 0s <-> ( 0s x.s B ) = 0s ) ) : No typesetting found for |- ( A = 0s -> ( ( A x.s B ) = 0s <-> ( 0s x.s B ) = 0s ) ) with typecode |-
21	4 20	syl5ibrcom	Could not format ( ph -> ( A = 0s -> ( A x.s B ) = 0s ) ) : No typesetting found for |- ( ph -> ( A = 0s -> ( A x.s B ) = 0s ) ) with typecode |-
22		muls01	Could not format ( A e. No -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( A e. No -> ( A x.s 0s ) = 0s ) with typecode |-
23	1 22	syl	Could not format ( ph -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( ph -> ( A x.s 0s ) = 0s ) with typecode |-
24		oveq2	Could not format ( B = 0s -> ( A x.s B ) = ( A x.s 0s ) ) : No typesetting found for |- ( B = 0s -> ( A x.s B ) = ( A x.s 0s ) ) with typecode |-
25	24	eqeq1d	Could not format ( B = 0s -> ( ( A x.s B ) = 0s <-> ( A x.s 0s ) = 0s ) ) : No typesetting found for |- ( B = 0s -> ( ( A x.s B ) = 0s <-> ( A x.s 0s ) = 0s ) ) with typecode |-
26	23 25	syl5ibrcom	Could not format ( ph -> ( B = 0s -> ( A x.s B ) = 0s ) ) : No typesetting found for |- ( ph -> ( B = 0s -> ( A x.s B ) = 0s ) ) with typecode |-
27	21 26	jaod	Could not format ( ph -> ( ( A = 0s \/ B = 0s ) -> ( A x.s B ) = 0s ) ) : No typesetting found for |- ( ph -> ( ( A = 0s \/ B = 0s ) -> ( A x.s B ) = 0s ) ) with typecode |-
28	18 27	impbid	Could not format ( ph -> ( ( A x.s B ) = 0s <-> ( A = 0s \/ B = 0s ) ) ) : No typesetting found for |- ( ph -> ( ( A x.s B ) = 0s <-> ( A = 0s \/ B = 0s ) ) ) with typecode |-