Metamath Proof Explorer


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 φ A No
0elright.2 φ A < s 0 s
Assertion 0elright φ 0 s R A

Proof

Step Hyp Ref Expression
1 0elright.1 φ A No
2 0elright.2 φ A < s 0 s
3 sltne A No A < s 0 s 0 s A
4 1 2 3 syl2anc φ 0 s A
5 4 necomd φ A 0 s
6 1 5 0elold φ 0 s Old bday A
7 breq2 x = 0 s A < s x A < s 0 s
8 rightval R A = x Old bday A | A < s x
9 7 8 elrab2 0 s R A 0 s Old bday A A < s 0 s
10 6 2 9 sylanbrc φ 0 s R A