Metamath Proof Explorer


Theorem negsbday

Description: Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Assertion negsbday A No bday + s A = bday A

Proof

Step Hyp Ref Expression
1 negsbdaylem A No bday + s A bday A
2 negnegs A No + s + s A = A
3 2 fveq2d A No bday + s + s A = bday A
4 negscl A No + s A No
5 negsbdaylem + s A No bday + s + s A bday + s A
6 4 5 syl A No bday + s + s A bday + s A
7 3 6 eqsstrrd A No bday A bday + s A
8 1 7 eqssd A No bday + s A = bday A