Metamath Proof Explorer

Theorem naddoa

Description: Natural addition of a natural is the same as regular addition. (Contributed by Scott Fenton, 20-Aug-2025)

Ref Expression
Assertion naddoa 
|- ( ( A e. On /\ B e. _om ) -> ( A +no B ) = ( A +o B ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( y = (/) -> ( A +no y ) = ( A +no (/) ) )
2 oveq2 
 |-  ( y = (/) -> ( A +o y ) = ( A +o (/) ) )
3 1 2 eqeq12d 
 |-  ( y = (/) -> ( ( A +no y ) = ( A +o y ) <-> ( A +no (/) ) = ( A +o (/) ) ) )
4 3 imbi2d 
 |-  ( y = (/) -> ( ( A e. On -> ( A +no y ) = ( A +o y ) ) <-> ( A e. On -> ( A +no (/) ) = ( A +o (/) ) ) ) )
5 oveq2 
 |-  ( y = x -> ( A +no y ) = ( A +no x ) )
6 oveq2 
 |-  ( y = x -> ( A +o y ) = ( A +o x ) )
7 5 6 eqeq12d 
 |-  ( y = x -> ( ( A +no y ) = ( A +o y ) <-> ( A +no x ) = ( A +o x ) ) )
8 7 imbi2d 
 |-  ( y = x -> ( ( A e. On -> ( A +no y ) = ( A +o y ) ) <-> ( A e. On -> ( A +no x ) = ( A +o x ) ) ) )
9 oveq2 
 |-  ( y = suc x -> ( A +no y ) = ( A +no suc x ) )
10 oveq2 
 |-  ( y = suc x -> ( A +o y ) = ( A +o suc x ) )
11 9 10 eqeq12d 
 |-  ( y = suc x -> ( ( A +no y ) = ( A +o y ) <-> ( A +no suc x ) = ( A +o suc x ) ) )
12 11 imbi2d 
 |-  ( y = suc x -> ( ( A e. On -> ( A +no y ) = ( A +o y ) ) <-> ( A e. On -> ( A +no suc x ) = ( A +o suc x ) ) ) )
13 oveq2 
 |-  ( y = B -> ( A +no y ) = ( A +no B ) )
14 oveq2 
 |-  ( y = B -> ( A +o y ) = ( A +o B ) )
15 13 14 eqeq12d 
 |-  ( y = B -> ( ( A +no y ) = ( A +o y ) <-> ( A +no B ) = ( A +o B ) ) )
16 15 imbi2d 
 |-  ( y = B -> ( ( A e. On -> ( A +no y ) = ( A +o y ) ) <-> ( A e. On -> ( A +no B ) = ( A +o B ) ) ) )
17 naddrid 
 |-  ( A e. On -> ( A +no (/) ) = A )
18 oa0 
 |-  ( A e. On -> ( A +o (/) ) = A )
19 17 18 eqtr4d 
 |-  ( A e. On -> ( A +no (/) ) = ( A +o (/) ) )
20 suceq 
 |-  ( ( A +no x ) = ( A +o x ) -> suc ( A +no x ) = suc ( A +o x ) )
21 20 3ad2ant3 
 |-  ( ( x e. _om /\ A e. On /\ ( A +no x ) = ( A +o x ) ) -> suc ( A +no x ) = suc ( A +o x ) )
22 nnon 
 |-  ( x e. _om -> x e. On )
23 naddsuc2 
 |-  ( ( A e. On /\ x e. On ) -> ( A +no suc x ) = suc ( A +no x ) )
24 22 23 sylan2 
 |-  ( ( A e. On /\ x e. _om ) -> ( A +no suc x ) = suc ( A +no x ) )
25 24 ancoms 
 |-  ( ( x e. _om /\ A e. On ) -> ( A +no suc x ) = suc ( A +no x ) )
26 25 3adant3 
 |-  ( ( x e. _om /\ A e. On /\ ( A +no x ) = ( A +o x ) ) -> ( A +no suc x ) = suc ( A +no x ) )
27 onasuc 
 |-  ( ( A e. On /\ x e. _om ) -> ( A +o suc x ) = suc ( A +o x ) )
28 27 ancoms 
 |-  ( ( x e. _om /\ A e. On ) -> ( A +o suc x ) = suc ( A +o x ) )
29 28 3adant3 
 |-  ( ( x e. _om /\ A e. On /\ ( A +no x ) = ( A +o x ) ) -> ( A +o suc x ) = suc ( A +o x ) )
30 21 26 29 3eqtr4d 
 |-  ( ( x e. _om /\ A e. On /\ ( A +no x ) = ( A +o x ) ) -> ( A +no suc x ) = ( A +o suc x ) )
31 30 3exp 
 |-  ( x e. _om -> ( A e. On -> ( ( A +no x ) = ( A +o x ) -> ( A +no suc x ) = ( A +o suc x ) ) ) )
32 31 a2d 
 |-  ( x e. _om -> ( ( A e. On -> ( A +no x ) = ( A +o x ) ) -> ( A e. On -> ( A +no suc x ) = ( A +o suc x ) ) ) )
33 4 8 12 16 19 32 finds 
 |-  ( B e. _om -> ( A e. On -> ( A +no B ) = ( A +o B ) ) )
34 33 impcom 
 |-  ( ( A e. On /\ B e. _om ) -> ( A +no B ) = ( A +o B ) )