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 ℝ ≼ ( ℚ ↑m ℕ )

Proof

Step Hyp Ref Expression
1 rpnnen1.n ⊢ ℕ ∈ V
2 rpnnen1.q ⊢ ℚ ∈ V
3 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 / 𝑘 ) = ( 𝑛 / 𝑘 ) )
4 3 breq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 / 𝑘 ) < 𝑥 ↔ ( 𝑛 / 𝑘 ) < 𝑥 ) )
5 4 cbvrabv ⊢ { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑥 } = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
6 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑚 / 𝑗 ) = ( 𝑚 / 𝑘 ) )
7 6 breq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑚 / 𝑗 ) < 𝑦 ↔ ( 𝑚 / 𝑘 ) < 𝑦 ) )
8 7 rabbidv ⊢ ( 𝑗 = 𝑘 → { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑗 ) < 𝑦 } = { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑦 } )
9 8 supeq1d ⊢ ( 𝑗 = 𝑘 → sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑗 ) < 𝑦 } , ℝ , < ) = sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑦 } , ℝ , < ) )
10 id ⊢ ( 𝑗 = 𝑘 → 𝑗 = 𝑘 )
11 9 10 oveq12d ⊢ ( 𝑗 = 𝑘 → ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑗 ) < 𝑦 } , ℝ , < ) / 𝑗 ) = ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑦 } , ℝ , < ) / 𝑘 ) )
12 11 cbvmptv ⊢ ( 𝑗 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑗 ) < 𝑦 } , ℝ , < ) / 𝑗 ) ) = ( 𝑘 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑦 } , ℝ , < ) / 𝑘 ) )
13 breq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑚 / 𝑘 ) < 𝑦 ↔ ( 𝑚 / 𝑘 ) < 𝑥 ) )
14 13 rabbidv ⊢ ( 𝑦 = 𝑥 → { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑦 } = { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑥 } )
15 14 supeq1d ⊢ ( 𝑦 = 𝑥 → sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑦 } , ℝ , < ) = sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑥 } , ℝ , < ) )
16 15 oveq1d ⊢ ( 𝑦 = 𝑥 → ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑦 } , ℝ , < ) / 𝑘 ) = ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑥 } , ℝ , < ) / 𝑘 ) )
17 16 mpteq2dv ⊢ ( 𝑦 = 𝑥 → ( 𝑘 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑦 } , ℝ , < ) / 𝑘 ) ) = ( 𝑘 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑥 } , ℝ , < ) / 𝑘 ) ) )
18 12 17 eqtrid ⊢ ( 𝑦 = 𝑥 → ( 𝑗 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑗 ) < 𝑦 } , ℝ , < ) / 𝑗 ) ) = ( 𝑘 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑥 } , ℝ , < ) / 𝑘 ) ) )
19 18 cbvmptv ⊢ ( 𝑦 ∈ ℝ ↦ ( 𝑗 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑗 ) < 𝑦 } , ℝ , < ) / 𝑗 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑥 } , ℝ , < ) / 𝑘 ) ) )
20 5 19 1 2 rpnnen1lem6 ⊢ ℝ ≼ ( ℚ ↑m ℕ )