Theorem nn0archi

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

	Ref	Expression
Assertion	nn0archi	⊢ ( ℂfld ↾s ℕ0 ) ∈ Archi

Proof

Step	Hyp	Ref	Expression
1		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
2	1	oveq1i	⊢ ( ℝfld ↾s ℕ0 ) = ( ( ℂfld ↾s ℝ ) ↾s ℕ0 )
3		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
4	3	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
5		nn0ssre	⊢ ℕ0 ⊆ ℝ
6		ressabs	⊢ ( ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℕ0 ⊆ ℝ ) → ( ( ℂfld ↾s ℝ ) ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 ) )
7	4 5 6	mp2an	⊢ ( ( ℂfld ↾s ℝ ) ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
8	2 7	eqtri	⊢ ( ℝfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
9		retos	⊢ ℝfld ∈ Toset
10		rearchi	⊢ ℝfld ∈ Archi
11	9 10	pm3.2i	⊢ ( ℝfld ∈ Toset ∧ ℝfld ∈ Archi )
12		nn0subm	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
13		subrgsubg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝ ∈ ( SubGrp ‘ ℂfld ) )
14		subgsubm	⊢ ( ℝ ∈ ( SubGrp ‘ ℂfld ) → ℝ ∈ ( SubMnd ‘ ℂfld ) )
15	4 13 14	mp2b	⊢ ℝ ∈ ( SubMnd ‘ ℂfld )
16	1	subsubm	⊢ ( ℝ ∈ ( SubMnd ‘ ℂfld ) → ( ℕ0 ∈ ( SubMnd ‘ ℝfld ) ↔ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) ∧ ℕ0 ⊆ ℝ ) ) )
17	15 16	ax-mp	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℝfld ) ↔ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) ∧ ℕ0 ⊆ ℝ ) )
18	12 5 17	mpbir2an	⊢ ℕ0 ∈ ( SubMnd ‘ ℝfld )
19		submarchi	⊢ ( ( ( ℝfld ∈ Toset ∧ ℝfld ∈ Archi ) ∧ ℕ0 ∈ ( SubMnd ‘ ℝfld ) ) → ( ℝfld ↾s ℕ0 ) ∈ Archi )
20	11 18 19	mp2an	⊢ ( ℝfld ↾s ℕ0 ) ∈ Archi
21	8 20	eqeltrri	⊢ ( ℂfld ↾s ℕ0 ) ∈ Archi