Metamath Proof Explorer


Theorem 0elleft

Description: Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025)

Ref Expression
Hypotheses 0elleft.1 φ A No
0elleft.2 φ 0 s < s A
Assertion 0elleft φ 0 s L A

Proof

Step Hyp Ref Expression
1 0elleft.1 φ A No
2 0elleft.2 φ 0 s < s A
3 2 sgt0ne0d φ A 0 s
4 1 3 0elold φ 0 s Old bday A
5 breq1 x = 0 s x < s A 0 s < s A
6 leftval L A = x Old bday A | x < s A
7 5 6 elrab2 0 s L A 0 s Old bday A 0 s < s A
8 4 2 7 sylanbrc φ 0 s L A