Theorem arch

Description: Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of Apostol p. 26. (Contributed by NM, 21-Jan-1997)

	Ref	Expression
Assertion	arch	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝐴 < 𝑛 )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 < 𝑛 ↔ 𝐴 < 𝑛 ) )
2	1	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 ↔ ∃ 𝑛 ∈ ℕ 𝐴 < 𝑛 ) )
3		nnunb	⊢ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 )
4		ralnex	⊢ ( ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) ↔ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
5	3 4	mpbir	⊢ ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 )
6		rexnal	⊢ ( ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) ↔ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
7		nnre	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
8		axlttri	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 𝑦 < 𝑛 ↔ ¬ ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ) )
9	7 8	sylan2	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < 𝑛 ↔ ¬ ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ) )
10		equcom	⊢ ( 𝑦 = 𝑛 ↔ 𝑛 = 𝑦 )
11	10	orbi1i	⊢ ( ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ↔ ( 𝑛 = 𝑦 ∨ 𝑛 < 𝑦 ) )
12		orcom	⊢ ( ( 𝑛 = 𝑦 ∨ 𝑛 < 𝑦 ) ↔ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
13	11 12	bitri	⊢ ( ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ↔ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
14	13	notbii	⊢ ( ¬ ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ↔ ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
15	9 14	bitrdi	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < 𝑛 ↔ ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) ) )
16	15	biimprd	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) → 𝑦 < 𝑛 ) )
17	16	reximdva	⊢ ( 𝑦 ∈ ℝ → ( ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 ) )
18	6 17	syl5bir	⊢ ( 𝑦 ∈ ℝ → ( ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 ) )
19	18	ralimia	⊢ ( ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) → ∀ 𝑦 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 )
20	5 19	ax-mp	⊢ ∀ 𝑦 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛
21	2 20	vtoclri	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝐴 < 𝑛 )