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		sltne	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 <s 0s ) → 0s ≠ 𝐴 )
4	1 2 3	syl2anc	⊢ ( 𝜑 → 0s ≠ 𝐴 )
5	4	necomd	⊢ ( 𝜑 → 𝐴 ≠ 0s )
6	1 5	0elold	⊢ ( 𝜑 → 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
7		breq2	⊢ ( 𝑥 = 0s → ( 𝐴 <s 𝑥 ↔ 𝐴 <s 0s ) )
8		rightval	⊢ ( R ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 }
9	7 8	elrab2	⊢ ( 0s ∈ ( R ‘ 𝐴 ) ↔ ( 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 0s ) )
10	6 2 9	sylanbrc	⊢ ( 𝜑 → 0s ∈ ( R ‘ 𝐴 ) )