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

Proof

Step	Hyp	Ref	Expression
1		0elright.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		0elright.2	⊢ ( 𝜑 → 𝐴 <s 0s )
3		ltsne	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 <s 0s ) → 0s ≠ 𝐴 )
4	1 2 3	syl2anc	⊢ ( 𝜑 → 0s ≠ 𝐴 )
5	4	necomd	⊢ ( 𝜑 → 𝐴 ≠ 0s )
6	1 5	0elold	⊢ ( 𝜑 → 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
7		elright	⊢ ( 0s ∈ ( R ‘ 𝐴 ) ↔ ( 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 0s ) )
8	6 2 7	sylanbrc	⊢ ( 𝜑 → 0s ∈ ( R ‘ 𝐴 ) )