rpnnen1lem4

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 13-Aug-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	rpnnen1lem.1	⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
	rpnnen1lem.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
	rpnnen1lem.n	⊢ ℕ ∈ V
	rpnnen1lem.q	⊢ ℚ ∈ V
Assertion	rpnnen1lem4	⊢ ( 𝑥 ∈ ℝ → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		rpnnen1lem.1	⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
2		rpnnen1lem.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
3		rpnnen1lem.n	⊢ ℕ ∈ V
4		rpnnen1lem.q	⊢ ℚ ∈ V
5	1 2 3 4	rpnnen1lem1	⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑_m ℕ ) )
6	4 3	elmap	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑_m ℕ ) ↔ ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ )
7	5 6	sylib	⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ )
8		frn	⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ran ( 𝐹 ‘ 𝑥 ) ⊆ ℚ )
9		qssre	⊢ ℚ ⊆ ℝ
10	8 9	sstrdi	⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ )
11	7 10	syl	⊢ ( 𝑥 ∈ ℝ → ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ )
12		1nn	⊢ 1 ∈ ℕ
13	12	ne0ii	⊢ ℕ ≠ ∅
14		fdm	⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → dom ( 𝐹 ‘ 𝑥 ) = ℕ )
15	14	neeq1d	⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ( dom ( 𝐹 ‘ 𝑥 ) ≠ ∅ ↔ ℕ ≠ ∅ ) )
16	13 15	mpbiri	⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → dom ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
17		dm0rn0	⊢ ( dom ( 𝐹 ‘ 𝑥 ) = ∅ ↔ ran ( 𝐹 ‘ 𝑥 ) = ∅ )
18	17	necon3bii	⊢ ( dom ( 𝐹 ‘ 𝑥 ) ≠ ∅ ↔ ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
19	16 18	sylib	⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
20	7 19	syl	⊢ ( 𝑥 ∈ ℝ → ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
21	1 2 3 4	rpnnen1lem3	⊢ ( 𝑥 ∈ ℝ → ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 )
22		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝑛 ≤ 𝑦 ↔ 𝑛 ≤ 𝑥 ) )
23	22	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 ↔ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ) )
24	23	rspcev	⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 )
25	21 24	mpdan	⊢ ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 )
26		suprcl	⊢ ( ( ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ ∧ ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 ) → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ )
27	11 20 25 26	syl3anc	⊢ ( 𝑥 ∈ ℝ → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ )

Metamath Proof Explorer

Theorem rpnnen1lem4

Proof