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	|- ( ph -> A e. No )
	0elleft.2	|- ( ph -> 0s
Assertion	0elleft	|- ( ph -> 0s e. ( _Left ` A ) )

Proof

Step	Hyp	Ref	Expression
1		0elleft.1	|- ( ph -> A e. No )
2		0elleft.2	|- ( ph -> 0s
3	2	sgt0ne0d	|- ( ph -> A =/= 0s )
4	1 3	0elold	|- ( ph -> 0s e. ( _Old ` ( bday ` A ) ) )
5		elleft	|- ( 0s e. ( _Left ` A ) <-> ( 0s e. ( _Old ` ( bday ` A ) ) /\ 0s
6	4 2 5	sylanbrc	|- ( ph -> 0s e. ( _Left ` A ) )