Metamath Proof Explorer

Theorem naddlid

Description: Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 20-Feb-2025)

Ref Expression
Assertion naddlid 
|- ( A e. On -> ( (/) +no A ) = A )

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 naddcom 
 |-  ( ( A e. On /\ (/) e. On ) -> ( A +no (/) ) = ( (/) +no A ) )
3 1 2 mpan2 
 |-  ( A e. On -> ( A +no (/) ) = ( (/) +no A ) )
4 naddrid 
 |-  ( A e. On -> ( A +no (/) ) = A )
5 3 4 eqtr3d 
 |-  ( A e. On -> ( (/) +no A ) = A )