Archimedean property in the reals

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I want to prove the following theorem:

theorem Real_archimedean' (x y : ℝ) : (0 < x) → (0 < y) → ∃ (n : ℕ), y < n * x

To do that, I've used the theorem in mathlib named "Archimedean.arch", but the problem is that in that theorem the product with the naturals is not the usual real product, but the product by an scalar. So, this is what I've done:

theorem Real_archimedean' (x y : ℝ) : (0 < x) → (0 < y) → ∃ (n : ℕ), y < n * x := by
  intro x_pos y_pos
  have : ∃ (n : ℕ), y ≤ n • x := by
    apply Archimedean.arch y x_pos
  rcases this with ⟨n, n_eq⟩
  have : n • x = ↑n * x := by
    sorry
  use (n + 1)
  rw [this] at n_eq
  apply lt_of_le_of_lt n_eq
  apply mul_lt_mul
  · norm_cast
    linarith
  · rfl
  · exact x_pos
  · norm_cast
    linarith

How Can I prove the "sorry" part? How can one relate the product by a scalar with the usual real product?

Thanks in advance.

[Patrick Massot]

theorem Real_archimedean' (x y : ℝ) : (0 < x) → (0 < y) → ∃ (n : ℕ), y < n * x := by
  intro x_pos _
  simpa using exists_lt_nsmul x_pos y

Note the positivity assumption on y is useless.

[Etienne Marion]

And for your particular sorry, you can use docs#nsmul_eq_mul.

[Esteban Martínez Vañó]

Thanks to both!

[Patrick Massot]

Sorry I didn’t pay attention to your proof start. The most useful answer about that particular sorry is that you should always try apply? in such situations.

[Esteban Martínez Vañó]

Patrick Massot ha dicho:

Sorry I didn’t pay attention to your proof start. The most useful answer about that particular sorry is that you should always try apply? in such situations.

I'll have it in mind. I've also learned that the simplifier has a lot of information contained in it :sweat_smile:

[Patrick Massot]

Sure, this is all useful information that is not so obvious. This is a normal part of the learning process.