Theorem 0elright

Description: Zero is in the right set of any negative number. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Hypotheses	0elright.1	$$⊢\phi \to A\in \mathrm{No}$$
	0elright.2	$$⊢\phi \to A{<}_s{0}_s$$
Assertion	0elright	$$⊢\phi \to 0_s\in R\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		0elright.1	$$⊢\phi \to A\in \mathrm{No}$$
2		0elright.2	$$⊢\phi \to A{<}_s{0}_s$$
3		sltne	$$⊢\left(A\in \mathrm{No}\wedge A{<}_s{0}_s\right)\to 0_s\ne A$$
4	1 2 3	syl2anc	$$⊢\phi \to 0_s\ne A$$
5	4	necomd	$$⊢\phi \to A\ne 0_s$$
6	1 5	0elold	$$⊢\phi \to 0_s\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
7		breq2	$$⊢x=0_s\to \left(A{<}_{s}x\leftrightarrow A{<}_s{0}_s\right)$$
8		rightval	$$⊢R\left(A\right)=\left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)|A{<}_{s}x\right\}$$
9	7 8	elrab2	$$⊢0_s\in R\left(A\right)\leftrightarrow \left(0_s\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\wedge A{<}_s{0}_s\right)$$
10	6 2 9	sylanbrc	$$⊢\phi \to 0_s\in R\left(A\right)$$