Metamath Proof Explorer


Theorem 0elold

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

Ref Expression
Hypotheses 0elold.1 φ A No
0elold.2 φ A 0 s
Assertion 0elold φ 0 s Old bday A

Proof

Step Hyp Ref Expression
1 0elold.1 φ A No
2 0elold.2 φ A 0 s
3 bday0s bday 0 s =
4 2 neneqd φ ¬ A = 0 s
5 bday0b A No bday A = A = 0 s
6 1 5 syl φ bday A = A = 0 s
7 4 6 mtbird φ ¬ bday A =
8 bdayelon bday A On
9 on0eqel bday A On bday A = bday A
10 8 9 ax-mp bday A = bday A
11 orel1 ¬ bday A = bday A = bday A bday A
12 7 10 11 mpisyl φ bday A
13 3 12 eqeltrid φ bday 0 s bday A
14 0sno 0 s No
15 oldbday bday A On 0 s No 0 s Old bday A bday 0 s bday A
16 8 14 15 mp2an 0 s Old bday A bday 0 s bday A
17 13 16 sylibr φ 0 s Old bday A