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

Proof

Step	Hyp	Ref	Expression
1		0elright.1	|- ( ph -> A e. No )
2		0elright.2	|- ( ph -> A
3		sltne	|- ( ( A e. No /\ A 0s =/= A )
4	1 2 3	syl2anc	|- ( ph -> 0s =/= A )
5	4	necomd	|- ( ph -> A =/= 0s )
6	1 5	0elold	|- ( ph -> 0s e. ( _Old ` ( bday ` A ) ) )
7		breq2	|- ( x = 0s -> ( A A
8		rightval	|- ( _Right ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A
9	7 8	elrab2	|- ( 0s e. ( _Right ` A ) <-> ( 0s e. ( _Old ` ( bday ` A ) ) /\ A
10	6 2 9	sylanbrc	|- ( ph -> 0s e. ( _Right ` A ) )