Theorem nn0archi

Description: The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018)

	Ref	Expression
Assertion	nn0archi	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Archi}$$

Proof

Step	Hyp	Ref	Expression
1		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
2	1	oveq1i	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0=\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
3		resubdrg	$$⊢\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$$
4	3	simpli	$$⊢ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
5		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
6		ressabs	$$⊢\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {\mathbb{N}}_0\subseteq ℝ\right)\to \left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
7	4 5 6	mp2an	$$⊢\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
8	2 7	eqtri	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
9		retos	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Toset}$$
10		rearchi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Archi}$$
11	9 10	pm3.2i	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{Toset}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{Archi}\right)$$
12		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
13		subrgsubg	$$⊢ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
14		subgsubm	$$⊢ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to ℝ\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
15	4 13 14	mp2b	$$⊢ℝ\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
16	1	subsubm	$$⊢ℝ\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to \left({\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℝ}_{\mathrm{fld}}\right)\leftrightarrow \left({\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\wedge {\mathbb{N}}_0\subseteq ℝ\right)\right)$$
17	15 16	ax-mp	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℝ}_{\mathrm{fld}}\right)\leftrightarrow \left({\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\wedge {\mathbb{N}}_0\subseteq ℝ\right)$$
18	12 5 17	mpbir2an	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℝ}_{\mathrm{fld}}\right)$$
19		submarchi	$$⊢\left(\left({ℝ}_{\mathrm{fld}}\in \mathrm{Toset}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{Archi}\right)\wedge {\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℝ}_{\mathrm{fld}}\right)\right)\to {ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Archi}$$
20	11 18 19	mp2an	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Archi}$$
21	8 20	eqeltrri	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Archi}$$