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	syl5eq	⊢ ( 𝑦 = 𝑥 → ( 𝑗 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑗 ) < 𝑦 } , ℝ , < ) / 𝑗 ) ) = ( 𝑘 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑥 } , ℝ , < ) / 𝑘 ) ) )
19	18	cbvmptv	⊢ ( 𝑦 ∈ ℝ ↦ ( 𝑗 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑗 ) < 𝑦 } , ℝ , < ) / 𝑗 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( { 𝑚 ∈ ℤ ∣ ( 𝑚 / 𝑘 ) < 𝑥 } , ℝ , < ) / 𝑘 ) ) )
20	5 19 1 2	rpnnen1lem6	⊢ ℝ ≼ ( ℚ ↑m ℕ )