Theorem nnamecl

Description: Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of Schloeder p. 6. See nnacl , nnmcl , nnecl . (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	nnamecl	|- ( ( A e. _om /\ B e. _om ) -> ( ( A +o B ) e. _om /\ ( A .o B ) e. _om /\ ( A ^o B ) e. _om ) )

Proof

Step	Hyp	Ref	Expression
1		nnacl	|- ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )
2		nnmcl	|- ( ( A e. _om /\ B e. _om ) -> ( A .o B ) e. _om )
3		nnecl	|- ( ( A e. _om /\ B e. _om ) -> ( A ^o B ) e. _om )
4	1 2 3	3jca	|- ( ( A e. _om /\ B e. _om ) -> ( ( A +o B ) e. _om /\ ( A .o B ) e. _om /\ ( A ^o B ) e. _om ) )