Theorem rearchi

Description: The field of the real numbers is Archimedean. See also arch . (Contributed by Thierry Arnoux, 9-Apr-2018)

	Ref	Expression
Assertion	rearchi	⊢ ℝfld ∈ Archi

Proof

Step	Hyp	Ref	Expression
1		reofld	⊢ ℝfld ∈ oField
2		rebase	⊢ ℝ = ( Base ‘ ℝfld )
3		eqid	⊢ ( ℤRHom ‘ ℝfld ) = ( ℤRHom ‘ ℝfld )
4		relt	⊢ < = ( lt ‘ ℝfld )
5	2 3 4	isarchiofld	⊢ ( ℝfld ∈ oField → ( ℝfld ∈ Archi ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) ) )
6	1 5	ax-mp	⊢ ( ℝfld ∈ Archi ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) )
7		arch	⊢ ( 𝑥 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 )
8		nnz	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
9		refld	⊢ ℝfld ∈ Field
10		isfld	⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) )
11	10	simplbi	⊢ ( ℝfld ∈ Field → ℝfld ∈ DivRing )
12		drngring	⊢ ( ℝfld ∈ DivRing → ℝfld ∈ Ring )
13	9 11 12	mp2b	⊢ ℝfld ∈ Ring
14		eqid	⊢ ( .g ‘ ℝfld ) = ( .g ‘ ℝfld )
15		re1r	⊢ 1 = ( 1r ‘ ℝfld )
16	3 14 15	zrhmulg	⊢ ( ( ℝfld ∈ Ring ∧ 𝑛 ∈ ℤ ) → ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) = ( 𝑛 ( .g ‘ ℝfld ) 1 ) )
17	13 16	mpan	⊢ ( 𝑛 ∈ ℤ → ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) = ( 𝑛 ( .g ‘ ℝfld ) 1 ) )
18		1re	⊢ 1 ∈ ℝ
19		remulg	⊢ ( ( 𝑛 ∈ ℤ ∧ 1 ∈ ℝ ) → ( 𝑛 ( .g ‘ ℝfld ) 1 ) = ( 𝑛 · 1 ) )
20	18 19	mpan2	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ( .g ‘ ℝfld ) 1 ) = ( 𝑛 · 1 ) )
21		zcn	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
22	21	mulid1d	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · 1 ) = 𝑛 )
23	17 20 22	3eqtrd	⊢ ( 𝑛 ∈ ℤ → ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) = 𝑛 )
24	23	breq2d	⊢ ( 𝑛 ∈ ℤ → ( 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) ↔ 𝑥 < 𝑛 ) )
25	8 24	syl	⊢ ( 𝑛 ∈ ℕ → ( 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) ↔ 𝑥 < 𝑛 ) )
26	25	rexbiia	⊢ ( ∃ 𝑛 ∈ ℕ 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 )
27	7 26	sylibr	⊢ ( 𝑥 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) )
28	6 27	mprgbir	⊢ ℝfld ∈ Archi