Theorem 0elleft

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

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

Proof

Step	Hyp	Ref	Expression
1		0elleft.1	$$⊢\phi \to A\in \mathrm{No}$$
2		0elleft.2	$$⊢\phi \to 0_s{<}_{s}A$$
3	2	sgt0ne0d	$$⊢\phi \to A\ne 0_s$$
4	1 3	0elold	$$⊢\phi \to 0_s\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
5		elleft	$$⊢0_s\in L\left(A\right)\leftrightarrow \left(0_s\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\wedge 0_s{<}_{s}A\right)$$
6	4 2 5	sylanbrc	$$⊢\phi \to 0_s\in L\left(A\right)$$