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	$$⊢\phi \to A\in \mathrm{No}$$
	0elright.2	No typesetting found for |- ( ph -> A
Assertion	0elright	Could not format assertion : No typesetting found for |- ( ph -> 0s e. ( _Right ` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0elright.1	$$⊢\phi \to A\in \mathrm{No}$$
2		0elright.2	Could not format ( ph -> A A
3		sltne	Could not format ( ( A e. No /\ A 0s =/= A ) : No typesetting found for |- ( ( A e. No /\ A 0s =/= A ) with typecode |-
4	1 2 3	syl2anc	Could not format ( ph -> 0s =/= A ) : No typesetting found for |- ( ph -> 0s =/= A ) with typecode |-
5	4	necomd	Could not format ( ph -> A =/= 0s ) : No typesetting found for |- ( ph -> A =/= 0s ) with typecode |-
6	1 5	0elold	Could not format ( ph -> 0s e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ph -> 0s e. ( _Old ` ( bday ` A ) ) ) with typecode |-
7		breq2	Could not format ( x = 0s -> ( A A ( A A
8		rightval	Could not format ( _Right ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A
9	7 8	elrab2	Could not format ( 0s e. ( _Right ` A ) <-> ( 0s e. ( _Old ` ( bday ` A ) ) /\ A ( 0s e. ( _Old ` ( bday ` A ) ) /\ A
10	6 2 9	sylanbrc	Could not format ( ph -> 0s e. ( _Right ` A ) ) : No typesetting found for |- ( ph -> 0s e. ( _Right ` A ) ) with typecode |-