Theorem mulsne0bd

Description: The product of two non-zero surreals is non-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	mulsne0bd	$$⊢\phi \to \left(A{\cdot }_{s}B\ne 0_s\leftrightarrow \left(A\ne 0_s\wedge B\ne 0_s\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		muls0ord.1	$$⊢\phi \to A\in \mathrm{No}$$
2		muls0ord.2	$$⊢\phi \to B\in \mathrm{No}$$
3	1 2	muls0ord	$$⊢\phi \to \left(A{\cdot }_{s}B=0_s\leftrightarrow \left(A=0_s\vee B=0_s\right)\right)$$
4	3	necon3abid	$$⊢\phi \to \left(A{\cdot }_{s}B\ne 0_s\leftrightarrow \neg \left(A=0_s\vee B=0_s\right)\right)$$
5		neanior	$$⊢\left(A\ne 0_s\wedge B\ne 0_s\right)\leftrightarrow \neg \left(A=0_s\vee B=0_s\right)$$
6	4 5	bitr4di	$$⊢\phi \to \left(A{\cdot }_{s}B\ne 0_s\leftrightarrow \left(A\ne 0_s\wedge B\ne 0_s\right)\right)$$