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	⊢ ( 𝜑 → 𝐴 ∈ No )
	0elleft.2	⊢ ( 𝜑 → 0s <s 𝐴 )
Assertion	0elleft	⊢ ( 𝜑 → 0s ∈ ( L ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		0elleft.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		0elleft.2	⊢ ( 𝜑 → 0s <s 𝐴 )
3	2	sgt0ne0d	⊢ ( 𝜑 → 𝐴 ≠ 0s )
4	1 3	0elold	⊢ ( 𝜑 → 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
5		elleft	⊢ ( 0s ∈ ( L ‘ 𝐴 ) ↔ ( 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 0s <s 𝐴 ) )
6	4 2 5	sylanbrc	⊢ ( 𝜑 → 0s ∈ ( L ‘ 𝐴 ) )