Theorem opnlen0

Description: An element not less than another is nonzero. TODO: Look for uses of necon3bd and op0le to see if this is useful elsewhere. (Contributed by NM, 5-May-2013)

	Ref	Expression
Hypotheses	op0le.b	$$⊢B={\mathrm{Base}}_K$$
	op0le.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	op0le.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
Assertion	opnlen0	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\wedge \neg X\underset{\dot{}}{\le }Y\right)\to X\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		op0le.b	$$⊢B={\mathrm{Base}}_K$$
2		op0le.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		op0le.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4	1 2 3	op0le	$$⊢\left(K\in \mathrm{OP}\wedge Y\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }Y$$
5	4	3adant2	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }Y$$
6		breq1	$$⊢X=\underset{\dot{}}{0}\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)$$
7	5 6	syl5ibrcom	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \left(X=\underset{\dot{}}{0}\to X\underset{\dot{}}{\le }Y\right)$$
8	7	necon3bd	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \left(\neg X\underset{\dot{}}{\le }Y\to X\ne \underset{\dot{}}{0}\right)$$
9	8	imp	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\wedge \neg X\underset{\dot{}}{\le }Y\right)\to X\ne \underset{\dot{}}{0}$$