This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpnnen1

Description: One half of rpnnen , where we show an injection from the real numbers to sequences of rational numbers. Specifically, we map a real number x to the sequence ( Fx ) : NN --> QQ (see rpnnen1lem6 ) such that ( ( Fx )k ) is the largest rational number with denominator k that is strictly less than x . In this manner, we get a monotonically increasing sequence that converges to x , and since each sequence converges to a unique real number, this mapping from reals to sequences of rational numbers is injective. Note: The NN and QQ existence hypotheses provide for use with either nnex and qex , or nnexALT and qexALT . The proof should not be modified to use any of those 4 theorems. (Contributed by Mario Carneiro, 13-May-2013) (Revised by Mario Carneiro, 16-Jun-2013) (Revised by NM, 15-Aug-2021) (Proof modification is discouraged.)

Ref Expression
Hypotheses rpnnen1.n ⊢ ℕ ∈ V
rpnnen1.q ⊢ ℚ ∈ V
Assertion rpnnen1 ⊢ ℝ ≼ ℚ ℕ

Proof

Step Hyp Ref Expression
1 rpnnen1.n ⊢ ℕ ∈ V
2 rpnnen1.q ⊢ ℚ ∈ V
3 oveq1 ⊢ m = n → m k = n k
4 3 breq1d ⊢ m = n → m k < x ↔ n k < x
5 4 cbvrabv ⊢ m ∈ ℤ | m k < x = n ∈ ℤ | n k < x
6 oveq2 ⊢ j = k → m j = m k
7 6 breq1d ⊢ j = k → m j < y ↔ m k < y
8 7 rabbidv ⊢ j = k → m ∈ ℤ | m j < y = m ∈ ℤ | m k < y
9 8 supeq1d ⊢ j = k → sup m ∈ ℤ | m j < y ℝ < = sup m ∈ ℤ | m k < y ℝ <
10 id ⊢ j = k → j = k
11 9 10 oveq12d ⊢ j = k → sup m ∈ ℤ | m j < y ℝ < j = sup m ∈ ℤ | m k < y ℝ < k
12 11 cbvmptv ⊢ j ∈ ℕ ⟼ sup m ∈ ℤ | m j < y ℝ < j = k ∈ ℕ ⟼ sup m ∈ ℤ | m k < y ℝ < k
13 breq2 ⊢ y = x → m k < y ↔ m k < x
14 13 rabbidv ⊢ y = x → m ∈ ℤ | m k < y = m ∈ ℤ | m k < x
15 14 supeq1d ⊢ y = x → sup m ∈ ℤ | m k < y ℝ < = sup m ∈ ℤ | m k < x ℝ <
16 15 oveq1d ⊢ y = x → sup m ∈ ℤ | m k < y ℝ < k = sup m ∈ ℤ | m k < x ℝ < k
17 16 mpteq2dv ⊢ y = x → k ∈ ℕ ⟼ sup m ∈ ℤ | m k < y ℝ < k = k ∈ ℕ ⟼ sup m ∈ ℤ | m k < x ℝ < k
18 12 17 eqtrid ⊢ y = x → j ∈ ℕ ⟼ sup m ∈ ℤ | m j < y ℝ < j = k ∈ ℕ ⟼ sup m ∈ ℤ | m k < x ℝ < k
19 18 cbvmptv ⊢ y ∈ ℝ ⟼ j ∈ ℕ ⟼ sup m ∈ ℤ | m j < y ℝ < j = x ∈ ℝ ⟼ k ∈ ℕ ⟼ sup m ∈ ℤ | m k < x ℝ < k
20 5 19 1 2 rpnnen1lem6 ⊢ ℝ ≼ ℚ ℕ