Theorem signswn0

Description: The zero-skipping operation propagates nonzeros. (Contributed by Thierry Arnoux, 11-Oct-2018)

	Ref	Expression
Hypotheses	signsw.p	$$⊢\underset{\dot{}}{⨣}=\left(a\in \left\{-1,0,1\right\},b\in \left\{-1,0,1\right\}⟼if\left(b=0,a,b\right)\right)$$
	signsw.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{-1,0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
Assertion	signswn0	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge X\ne 0\right)\to X\underset{\dot{}}{⨣}Y\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		signsw.p	$$⊢\underset{\dot{}}{⨣}=\left(a\in \left\{-1,0,1\right\},b\in \left\{-1,0,1\right\}⟼if\left(b=0,a,b\right)\right)$$
2		signsw.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{-1,0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
3	1	signspval	$$⊢\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\to X\underset{\dot{}}{⨣}Y=if\left(Y=0,X,Y\right)$$
4	3	adantr	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge X\ne 0\right)\to X\underset{\dot{}}{⨣}Y=if\left(Y=0,X,Y\right)$$
5		neeq1	$$⊢X=if\left(Y=0,X,Y\right)\to \left(X\ne 0\leftrightarrow if\left(Y=0,X,Y\right)\ne 0\right)$$
6		neeq1	$$⊢Y=if\left(Y=0,X,Y\right)\to \left(Y\ne 0\leftrightarrow if\left(Y=0,X,Y\right)\ne 0\right)$$
7		simplr	$$⊢\left(\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge X\ne 0\right)\wedge Y=0\right)\to X\ne 0$$
8		simpr	$$⊢\left(\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge X\ne 0\right)\wedge \neg Y=0\right)\to \neg Y=0$$
9	8	neqned	$$⊢\left(\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge X\ne 0\right)\wedge \neg Y=0\right)\to Y\ne 0$$
10	5 6 7 9	ifbothda	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge X\ne 0\right)\to if\left(Y=0,X,Y\right)\ne 0$$
11	4 10	eqnetrd	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge X\ne 0\right)\to X\underset{\dot{}}{⨣}Y\ne 0$$